File: ext_dialog.ml

package info (click to toggle)
prooftree 0.13-1
  • links: PTS, VCS
  • area: main
  • in suites: bullseye, sid, stretch
  • size: 592 kB
  • ctags: 668
  • sloc: ml: 4,462; sh: 117; makefile: 111
file content (622 lines) | stat: -rw-r--r-- 22,708 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
(* 
 * prooftree --- proof tree display for Proof General
 * 
 * Copyright (C) 2011 - 2016 Hendrik Tews
 * 
 * This file is part of "prooftree".
 * 
 * "prooftree" is free software: you can redistribute it and/or
 * modify it under the terms of the GNU General Public License as
 * published by the Free Software Foundation, either version 3 of the
 * License, or (at your option) any later version.
 * 
 * "prooftree" is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
 * General Public License in file COPYING in this or one of the parent
 * directories for more details.
 * 
 * You should have received a copy of the GNU General Public License
 * along with "prooftree". If not, see <http://www.gnu.org/licenses/>.
 * 
 * $Id: ext_dialog.ml,v 1.18 2016/01/23 12:57:14 tews Exp $
 *)

(** The Existential Variable Dialog *)

(* open Util *)
open Gtk_ext
open Configuration
open Draw_tree


(** Record for one line in the table of existential variables. This
    record links the {!Draw_tree.existential_variable} record and the
    necessary GTK widgets in order to update the table line when the
    status of the existential changes. For memory management is makes
    also sense to destroy all widgets when a line gets deleted.

    For easy access, these table line records are stored in the
    {!existential_variable_window.ext_hash} hash table with the name
    of the existential as key.
*)
type ext_table_line = {
  ext_table_ext : existential_variable;     (** The existential record
						with all status information *)
  ext_table_row : int;                      (** The row number in the table *)
  ext_table_status_label : GMisc.label;     (** Label for the status *)
  ext_table_using_label : GMisc.label;      (** Label for using column *)
  ext_table_button : GButton.toggle_button; (** display toggle button *)
  ext_table_other : GObj.widget array;      (** all other widgets in the line *)
}


(** Class for managing dialogs for existential variables. Objects are
    created when the widget tree is completely constructed. Contains
    the necessary state and methods to handle all callbacks. The
    callbacks must be set up by the function that creates objects.

    The existential dialog supports lazy update as the proof-tree
    window. This means that the table is only updated when Prooftree
    is idle because there are currently no commands to process.
    Requests for adding or deleting existentials are accumulated in
    {!to_add} and {!to_delete} until {!update_ext_dialog} is called.
    Actually, the display must be updated add and delete requests
    (which is currently not ensured).

    Arguments are
    - proof_window      {!class: Proof_window.proof_window} to which this 
                        window is associated to
    - top_window	{xref lablgtk class GWindow.window}
                        of the top-level widget
    - ext_table		{xref lablgtk class GPack.table} of the main table
    - table_v_adjustment  {xref lablgtk class GData.adjustment} 
                          for the scrollbar of the table
    - border_vbars      the left and the right vertical bar together 
                        with their column
    - inner_vbars       the other vertical bars together with their column
    - start_row		first row in the table
    - name_col		column for names
    - status_col	column for status
    - button_col	column for buttons
    - last_col		last column
*)
class existential_variable_window
  proof_window
  (top_window : GWindow.window)
  (ext_table : GPack.table)
  (table_v_adjustment : GData.adjustment)
  (border_vbars : (GObj.widget * int) array)
  (inner_vbars : (GObj.widget * int) array)
  start_row name_col status_col using_col button_col last_col
  =
object (self)

  (** "no" label text for the instantiated column. *)
  val uninst_label = "no"

  (** "partially" label text for the instantiated column. Contains
      pango markup for the color.
  *)
  val mutable partially_inst_label = ""

  (** "fully" label text for the instantiated column. Contains pango
      markup for the color.
  *)
  val mutable fully_inst_label = ""

  (** Used to show the bottom of the existential variable table by
      default. If the user scrolls the table, then this flag remembers
      if he scrolled to the bottom, see
      {!scrollbar_value_changed_callback}. When the table size
      changes, the table is automatically scrolled to the bottom, if
      this flag is true.
  *)
  val mutable clamp_to_bottom = true

  (** The next free row in the table. Managed by all methods that add
      or delete rows in the table.
  *)
  val mutable next_row = start_row

  (** Hash mapping existential names to {!ext_table_line} records. The
      hash is used when updating the status and when deleting selected
      existentials from the table.
  *)
  val ext_hash = Hashtbl.create 251

  (** Existentials queued for addition. This is a list of lists to
      avoid list concatenation. If this is non-nil then {!to_delete}
      must be nil. *)
  val mutable to_add = []

  (** Existentials queued for deletion. This is a list of lists to
      avoid list concatenation. If this is non-nil then {!to_add} must
      be nil. *)
  val mutable to_delete = []

  (** This array is non-empty precisely when the "no existential
      variables" line is displayed in the array. Contains the widgets
      of that line if non-empty. 
  *)
  val mutable no_ext_label_widgets = [| |]

  (** Stores the currently pressed "mark" button if there is one. Used
      to ensure that maximal one mark button can be pressed.
  *)
  val mutable pressed_mark_button = None

  (** Create the pango markup text for the "partially" and "fully"
      labels. Called in the initializer and when the configuration has
      been updated.
  *)
  method make_inst_labels =
    partially_inst_label <- 
      pango_markup_color "partially" !proved_partial_gdk_color;
    fully_inst_label <- 
      pango_markup_color "fully" !proved_complete_gdk_color

  (** Schedule the existentials in the argument list to be added to
      the table.
  *)
  method change_and_add new_ext =
    assert(to_delete = []);
    if new_ext <> [] then
      to_add <- new_ext :: to_add

  (** Schedule the existentials in the argument list to be removed
      from the table.
  *)
  method change_and_delete remove_ext =
    assert(to_add = []);
    if remove_ext <> [] then
      to_delete <- remove_ext :: to_delete

  (** Adjust the length of the vertical bars in the table. The border
      bars are always drawn to the bottom of the table. The inner bars
      are only drawn up to row [bottom].
      
      All vertical bars are created in the very beginning and then
      reused all the time by removing and adding them to the table.
  *)
  method private adjust_vbars bottom =
    Array.iter 
      (fun (bar, col) ->
	ext_table#remove bar;
	ext_table#attach ~left:col ~top:0 ~bottom:next_row bar)
      border_vbars;
    Array.iter 
      (fun (bar, col) ->
	ext_table#remove bar;
	ext_table#attach ~left:col ~top:0 ~bottom bar)
      inner_vbars

  (** Put a "no existential variables" line into the table and store
      its widgets in {!no_ext_label_widgets}.
  *)
  method private make_no_ext_label =
    let no_ext_label = GMisc.label 
      ~text:"There are no existential variables" ~ypad:8
      ~packing:(ext_table#attach ~left:name_col ~right:last_col ~top:next_row)
      () in
    next_row <- next_row + 1;
    let hbar = GMisc.separator `HORIZONTAL 
      ~packing:(ext_table#attach ~left:0 ~right:last_col ~top:next_row) () in
    next_row <- next_row + 1;
    self#adjust_vbars (next_row - 2);
    no_ext_label_widgets <- [| hbar#coerce; no_ext_label#coerce |]

  (** Delete the "no existential variables" line from the table. *)
  method private delete_no_ext_label =
    Array.iter (fun w -> w#destroy ()) no_ext_label_widgets;
    no_ext_label_widgets <- [| |];
    next_row <- start_row

  (** Release the currently pressed "mark" button, if there is one. *)
  method release_pressed_button =
    (match pressed_mark_button with
      | None -> ()
      | Some button -> 
	button#set_active false;
	pressed_mark_button <- None
    );

  (** Return the pair of proof-tree nodes that create and instantiate
      the given existential. If the existential is not instantiated
      then the second component is [None].
  *)
  method private get_ext_nodes existential =
    let crea_node = 
      match 
	proof_window#find_node
	  (fun n -> List.memq existential n#fresh_existentials)
      with
	| None -> assert false
	| Some n -> n
    in
    (* 
     * Printf.fprintf (debugc())
     *   "GEN ext %s status %s crea node %s\n%!"
     *   existential.existential_name
     *   (match existential.status with
     * 	| Uninstantiated -> "uninst"
     * 	| Partially_instantiated -> "partial"
     * 	| Fully_instantiated -> "fully")
     *   crea_node#debug_name;
     *)
    if existential.status <> Uninstantiated then
      let inst_node =  
	proof_window#find_node
	  (fun n -> List.memq existential n#inst_existentials)
      in
      assert(inst_node <> None);
      (crea_node, inst_node)
    else
      (crea_node, None)

  (** Callback function for toggling some "mark" button. Marks or
      unmarks the existential, keeps {!pressed_mark_button} up to date,
      schedules the proof tree for redisplay and tries to show the marked
      nodes.
  *)
  method mark_button_toggled button existential () =
    if button#active
    then begin
      self#release_pressed_button;
      pressed_mark_button <- Some button;
      existential.existential_mark <- true;
      (match self#get_ext_nodes existential with
	| (crea, Some inst) ->
	  proof_window#show_both_nodes crea inst
	| (crea, None) -> 
	  proof_window#show_node crea
      );
      proof_window#invalidate_drawing_area;
    end
    else begin
      existential.existential_mark <- false;
      pressed_mark_button <- None;
      proof_window#invalidate_drawing_area;
    end

  (** Update the information in the argument table line. *)
  method private set_ext_line_status tl =
    tl.ext_table_status_label#set_label
      (match tl.ext_table_ext.status with
	| Uninstantiated -> uninst_label
	| Partially_instantiated -> partially_inst_label
	| Fully_instantiated -> fully_inst_label
      );
    let color_ex_name ex =
      match ex.status with
	| Uninstantiated -> ex.existential_name
	| Partially_instantiated -> 
	  pango_markup_color ex.existential_name !proved_partial_gdk_color
	| Fully_instantiated -> 
	  pango_markup_color ex.existential_name !proved_complete_gdk_color
    in
    let colored_dep_names =
      String.concat ", " 
	(List.map color_ex_name tl.ext_table_ext.dependencies) in
    tl.ext_table_using_label#set_label colored_dep_names
      

  (** Update the status of the complete table. *)
  method private update_existential_status =
    Hashtbl.iter 
      (fun _ tl ->
	(* We don't have to update every line. However, the test is
	 * rather complicated, because we have to check whether the
	 * status of any of the dependencies changes. For that one
	 * would have to through ext_hash, in order to find the last
	 * status of the dependencies.
	 *)
	self#set_ext_line_status tl
      )
      ext_hash

  (** Add the existentials in the argument list to the table. Creates
      the necessary widgets and stores them in {!ext_hash}. This method
      must not be called with an empty argument list.
  *)
  method private process_fresh_existentials l =
    assert(l <> []);
    let doit ext =
      assert(Hashtbl.mem ext_hash ext.existential_name = false);
      let ext_row = next_row in
      let name_label = GMisc.label ~text:ext.existential_name
	~packing:(ext_table#attach ~left:name_col ~top:ext_row) () in
      let status_label = GMisc.label (* ~xpad:7 *)
	~packing:(ext_table#attach ~left:status_col ~top:ext_row) () in
      status_label#set_use_markup true;
      let using_label = GMisc.label
	~packing:(ext_table#attach ~left:using_col ~top:ext_row) () in
      using_label#set_use_markup true;
      let button = GButton.toggle_button
	~label:"mark"
	~packing:(ext_table#attach ~fill:`NONE ~left:button_col ~top:ext_row)
	() in
      ignore(button#connect#toggled 
	       ~callback:(self#mark_button_toggled button ext));
      next_row <- next_row + 1;
      let hbar = GMisc.separator `HORIZONTAL 
      	~packing:(ext_table#attach ~left:0 ~right:last_col ~top:next_row) () in
      next_row <- next_row + 1;
      Hashtbl.add ext_hash ext.existential_name 
	{ ext_table_ext = ext;
	  ext_table_row = ext_row;
	  ext_table_status_label = status_label;
	  ext_table_using_label = using_label;
	  ext_table_button = button;
	  ext_table_other = 
	    [| name_label#coerce; hbar#coerce; |]
	};
      ()
    in
    if Array.length no_ext_label_widgets <> 0
    then self#delete_no_ext_label;
    List.iter doit l;
    self#adjust_vbars next_row

  (** Destroy all widgets in a table line. Takes care of releasing the
      "mark" button if necessary.
  *)
  method private destroy_ext_line ext_table_line =
    ext_table_line.ext_table_status_label#destroy ();
    ext_table_line.ext_table_using_label#destroy ();
    ext_table_line.ext_table_button#set_active false;
    ext_table_line.ext_table_button#destroy ();
    Array.iter (fun w -> w#destroy ()) ext_table_line.ext_table_other


  (** Delete an existential from the table. Destroys the widgets,
      releases the "mark" button if necessary and updates {!ext_hash}.
  *)
  method private undo_delete ext =
    let tl = Hashtbl.find ext_hash ext.existential_name in
    self#destroy_ext_line tl;
    Hashtbl.remove ext_hash ext.existential_name;
    if tl.ext_table_row < next_row
    then next_row <- tl.ext_table_row


  (** Process pending addition or deletion requests and make the whole
      table up-to-date. Only one of {!to_add} and {!to_delete} can be
      non-nil.
  *)
  method update_ext_dialog =
    assert(to_add = [] || to_delete = []);
    List.iter (fun l -> self#process_fresh_existentials l) (List.rev to_add);
    to_add <- [];
    List.iter 
      (fun l -> List.iter (fun e -> self#undo_delete e) l)
      to_delete;
    to_delete <- [];
    self#update_existential_status;
    if next_row = start_row 
    then self#make_no_ext_label
      

  (** Fist part of table initialization. Fill the table by processing
      all existentials in the proof tree of the given root node. This
      function can be called several times for different root nodes.
  *)
  method fill_table_lines (nodes : proof_tree_element list) =
    let rec iter node =
      if node#fresh_existentials <> [] then
	self#process_fresh_existentials node#fresh_existentials;
      List.iter iter node#children
    in
    List.iter iter nodes

  (** Second part of table initialization, to be called after all
      proof trees have been processed with {!fill_table_lines}.
  *)
  method finish_table_init =
    self#update_existential_status;
    if next_row = start_row
    then self#make_no_ext_label

  (** Update colors after the configuration has been updated. *)
  method configuration_updated =
    self#make_inst_labels;
    self#update_existential_status

  (** Clear the table for reuse. *)
  method clear_for_reuse =
    if Array.length no_ext_label_widgets = 0 then begin
      Hashtbl.iter (fun _ tl -> self#destroy_ext_line tl) ext_hash;
      Hashtbl.clear ext_hash;
      next_row <- start_row;
    end

  (** Callback for key events. Call the appropriate action for each
      key.
  *)
  method key_pressed_callback ev =
    match GdkEvent.Key.keyval ev with 
      | ks when 
	  (ks = GdkKeysyms._Q || ks = GdkKeysyms._q) 
	  && (List.mem `CONTROL (GdkEvent.Key.state ev))
	  -> 
	exit 0
      | ks when (ks = GdkKeysyms._Q || ks = GdkKeysyms._q)  -> 
	self#destroy (); true
      | ks when ks = GdkKeysyms._Up -> 
	scroll_adjustment table_v_adjustment (-1); true
      | ks when ks = GdkKeysyms._Down -> 
	scroll_adjustment table_v_adjustment 1; true

      | _ -> false

  (** Callback for the [changed] signal of the scrollbar adjustment,
      which is emitted when anything but the [value] changes. This
      callback scrolls the table to the bottom, if {!clamp_to_bottom}
      is [true].
  *)
  method scrollbar_changed_callback () =
    let a = table_v_adjustment in
    (* 
     * Printf.fprintf (debugc()) "scroll changed %.1f - %.1f up %.1f\n%!"
     *   a#value (a#value +. a#page_size) a#upper;
     *)
    if clamp_to_bottom then
      let upper = a#upper in
      a#clamp_page ~lower:upper ~upper:upper

  (** Callback for the [value-changed] signal of the scrollbar
      adjustment, which is emitted when the [value] changes. This
      callback remembers in {!clamp_to_bottom} whether the table was
      scrolled to the bottom.
  *)
  method scrollbar_value_changed_callback () =
    let a = table_v_adjustment in
    (* 
     * Printf.fprintf (debugc()) "scroll value   %.1f - %.1f up %.1f\n%!"
     *   a#value (a#value +. a#page_size) a#upper;
     *)
    if a#value +. a#page_size >= a#upper
    then clamp_to_bottom <- true
    else clamp_to_bottom <- false

  (** Make this configuration dialog visible. *)
  method present = top_window#present()

  (** Action for the Close button and the destroy signal. *)
  method destroy () =
    self#release_pressed_button;
    proof_window#existential_clear ();
    top_window#destroy();

  initializer
    self#make_inst_labels
end



(** Create a new dialog for existential variables. Creates the widget
    hierarchy, initializes the management object and registers all
    callbacks. The initial table fill must be initiated by the caller.
*)
let make_ext_dialog proof_window proof_name =
  let top_window = GWindow.window () in
  let top_v_box = GPack.vbox ~packing:top_window#add () in
  let _ext_title = GMisc.label
    ~line_wrap:true
    ~justify:`CENTER
    ~markup:("<big><b>Existential Variables: " ^ proof_name ^ "</b></big>")
    ~xpad:10 ~ypad:10
    ~packing:top_v_box#pack () in

  (****************************************************************************
   *
   * Scrollbar for table
   *
   ****************************************************************************)
  let scrolling_hbox = GPack.hbox 
    ~packing:(top_v_box#pack ~expand:true) () in
  let table_scrolling = GBin.scrolled_window 
    ~hpolicy:`NEVER ~vpolicy:`ALWAYS
    ~packing:(scrolling_hbox#pack ~expand:true ~fill:false) ()
  in
  let table_v_adjustment = table_scrolling#vadjustment in

  (****************************************************************************
   *
   * table of existentials
   *
   ****************************************************************************)
  let ext_table = GPack.table ~border_width:5
    ~packing:table_scrolling#add_with_viewport () in
  let name_col = 1 in
  let status_col = 3 in
  let using_col = 5 in
  let button_col = 7 in 
  let last_col = button_col + 2 in
  let xpadding = 7 in
  let ypadding = 3 in
  let row = 0 in
  let _hbar = GMisc.separator `HORIZONTAL 
    ~packing:(ext_table#attach ~left:0 ~right:last_col ~top:row) () in
  let row = row + 1 in
  let bar_l = GMisc.separator `VERTICAL
    ~packing:(ext_table#attach ~left:0 ~top:row ~bottom:(row + 1)) () in
  let _name_heading = GMisc.label ~markup:"<b>Name</b>" 
    ~xpad:xpadding ~ypad:ypadding
    ~packing:(ext_table#attach ~left:name_col ~top:row) () in
  let bar_1 = GMisc.separator `VERTICAL
    ~packing:(ext_table#attach ~left:(name_col + 1) ~top:row) () in
  let _status_heading = GMisc.label ~markup:"<b>Instantiated</b>"
    ~xpad:xpadding ~ypad:ypadding
    ~packing:(ext_table#attach ~left:status_col ~top:row) () in
  let bar_2 = GMisc.separator `VERTICAL
    ~packing:(ext_table#attach ~left:(status_col + 1) ~top:row) () in
  let _using_heading = GMisc.label ~markup:"<b>Using</b>"
    ~xpad:xpadding ~ypad:ypadding
    ~packing:(ext_table#attach ~left:using_col ~top:row) () in
  let bar_3 = GMisc.separator `VERTICAL
    ~packing:(ext_table#attach ~left:(using_col + 1) ~top:row) () in
  let _button_heading = GMisc.label ~markup:"<b>Mark Nodes</b>"
    ~xpad:xpadding ~ypad:ypadding
    ~packing:(ext_table#attach ~left:button_col ~top:row) () in
  let bar_r = GMisc.separator `VERTICAL
    ~packing:(ext_table#attach ~left:(button_col + 1) 
		~top:row ~bottom:(row + 1)) () in
  let border_vbars = [| (bar_l#coerce, 0); 
			(bar_r#coerce, button_col + 1) |] in
  let inner_vbars = [| (bar_1#coerce, name_col + 1);
		       (bar_2#coerce, status_col + 1);
		       (bar_3#coerce, using_col + 1); |] in

  let row = row + 1 in
  let _hbar = GMisc.separator `HORIZONTAL 
    ~packing:(ext_table#attach ~left:0 ~right:last_col ~top:row) () in
  let row = row + 1 in

  (****************************************************************************
   *
   * compute size
   *
   ****************************************************************************)
  let context = ext_table#misc#pango_context in
  let layout = context#create_layout in
  Pango.Layout.set_text layout "X";
  let (_, char_height) = Pango.Layout.get_pixel_size layout in
  top_window#set_default_size ~width:0 
    ~height:(8 * char_height + 
	       int_of_float ((float_of_int !current_config.ext_table_lines)
			     *. 1.76 *. (float_of_int char_height)));


  (****************************************************************************
   *
   * bottom button box
   *
   ****************************************************************************)
  let button_box = GPack.hbox 
    ~spacing:5 ~border_width:5 ~packing:top_v_box#pack () in
  let show_current_button = GButton.button
    ~label:"Show current" ~packing:button_box#pack () in
  let close_button = GButton.button
    ~stock:`CLOSE ~packing:(button_box#pack ~from:`END) () in

  let ext_window = 
    new existential_variable_window proof_window top_window 
      ext_table table_v_adjustment border_vbars inner_vbars
      row name_col status_col using_col button_col last_col
  in

  top_window#set_title "Existential Variables";
  ignore(table_v_adjustment#connect#changed 
	   ~callback:ext_window#scrollbar_changed_callback);
  ignore(table_v_adjustment#connect#value_changed 
	   ~callback:ext_window#scrollbar_value_changed_callback);
  ignore(top_window#event#connect#key_press 
	   ~callback:ext_window#key_pressed_callback);
  ignore(top_window#connect#destroy ~callback:ext_window#destroy);
  ignore(show_current_button#connect#clicked 
	   ~callback:proof_window#show_current_node);
  ignore(close_button#connect#clicked ~callback:ext_window#destroy);
  top_window#show ();

  ext_window