File: proof_window.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 (1506 lines) | stat: -rw-r--r-- 54,161 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
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
1324
1325
1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
1361
1362
1363
1364
1365
1366
1367
1368
1369
1370
1371
1372
1373
1374
1375
1376
1377
1378
1379
1380
1381
1382
1383
1384
1385
1386
1387
1388
1389
1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
1400
1401
1402
1403
1404
1405
1406
1407
1408
1409
1410
1411
1412
1413
1414
1415
1416
1417
1418
1419
1420
1421
1422
1423
1424
1425
1426
1427
1428
1429
1430
1431
1432
1433
1434
1435
1436
1437
1438
1439
1440
1441
1442
1443
1444
1445
1446
1447
1448
1449
1450
1451
1452
1453
1454
1455
1456
1457
1458
1459
1460
1461
1462
1463
1464
1465
1466
1467
1468
1469
1470
1471
1472
1473
1474
1475
1476
1477
1478
1479
1480
1481
1482
1483
1484
1485
1486
1487
1488
1489
1490
1491
1492
1493
1494
1495
1496
1497
1498
1499
1500
1501
1502
1503
1504
1505
1506
(* 
 * 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: proof_window.ml,v 1.67 2016/01/23 12:57:15 tews Exp $
 *)


(** Creation, display and drawing of the main proof-tree window *)


(* open Util *)
open Gtk_ext
open Configuration
open Emacs_commands
open Draw_tree
open Tree_layers
open Node_window
open Help_window
open About_window
open Ext_dialog


(** Callback for higher-level modules when the user deletes a proof
    window. During start-up the reference is changed to
    {!Proof_tree.quit_proof}.
*)
let delete_proof_tree_callback = ref (fun (_ : string) -> ())


(** Contains proof window clones. See also
    [Proof_tree.original_proof_trees].
*)
let cloned_proof_windows = ref []

(** Class for managing the main proof-tree window. Contains methods
    for all callbacks and the necessary state. The widget tree the
    binding to singals must be done outside.

    Arguments are
    - top_window              {xref lablgtk class GWindow.window} 
                              of the top-level widget
    - drawing_h_adjustment    {xref lablgtk class GData.adjustment}
                              of the horizontal scroll bar
                              of the drawing area
    - drawing_v_adjustment    {xref lablgtk class GData.adjustment}
                              of the vertical scroll bar
                              of the drawing area
    - drawing_area            {xref lablgtk class GMisc.drawing_area}
                              for the proof tree
    - drawable                {!Gtk_ext.better_drawable} for the actual 
                              drawing operations
    - labeled_sequent_frame   {xref lablgtk class GBin.frame}
                              labelled frame of the sequent area
    - sequent_window          {xref lablgtk class GText.view}
                              of the sequent area
    - sequent_v_adjustment    {xref lablgtk class GData.adjustment}
                              of the vertical scroll bar of the sequent area
    - message_label           {xref lablgtk class GMisc.label}
                              for messages in the bottom line
    - context_menu            {xref lablgtk class GMenu.menu} 
                              of the context menu
    - proof_name              the name of the proof this display is showing
*)
class proof_window (top_window : GWindow.window)
  drawing_h_adjustment drawing_v_adjustment (drawing_area : GMisc.drawing_area)
  (drawable : better_drawable)
  labeled_sequent_frame sequent_window sequent_v_adjustment
  (message_label : GMisc.label) context_menu proof_name
  =
object (self)

  (***************************************************************************
   *
   * Internal state and setters/accessors
   *
   ***************************************************************************)

  (** x-offset of the bounding box of the complete proof tree layer
      stack. This is only non-zero when the width of the complete
      layer stack is smaller than the width of the drawing area. *)
  val mutable top_left = 0

  (** y-offset of the bounding box of the top layer. Constantly 0. *)
  val top_top = 0

  (** [true] if the sequent area should always show the last line.
      This is set to [true] when a sequent is shown and to false when
      a proof command is shown. *)
  val mutable sequent_window_scroll_to_bottom = false

  (** The stack of layers of proof trees *)
  val layer_stack = new tree_layer_stack

  (** The current node of the proof tree, if there is one *)
  val mutable current_node = None

  (** Cache holding the relative bounding box of the current node. If
      not [None], it holds the tuple [(x_low, x_high, y_low, y_high)]
      relative to the top-left corner (i.e., ({!top_left},
      {!top_top})) of the bounding box of the complete proof tree.
  *)
  val mutable current_node_offset_cache = None

  (** Set to [true] when we still have to reposition the drawing area
      to make the current node visible. This is needed because of the
      asynchronous nature of GTK, which does not immediately resize
      the drawing area when I request it. Therefore the positioning
      code has to wait until the drawing area has changed its size and
      all needed scrollbars have been added.
  *)
  val mutable position_to_current_node = true

  (** List of position hints, containing lists of proof tree nodes. If
      possible, the current node will positioned such that some hint
      nodes are also visible. If the list is longer than one, hints
      are tried one after each other. 
  *)
  val mutable position_hints = []

  (** Holds the selected node, if there is one. *)
  val mutable selected_node = None

  (** List of all external non-orphaned node windows that belong to nodes 
      in the current proof tree. This list is stored only for optimization.
  *)
  val mutable node_windows = []

  (** The management object for the dialog for existential
      variables, if present. 
  *)
  val mutable existential_window = None

  (** When we are asked to destroy this proof-tree window (because of
      an undo or because Proof General sent a quit-proof command) then
      the destruction of the top-level GTK window will emit a destroy
      signal that we interpret as a user destroy button click.
      Further, the deletion of this proof from the various list with
      proof_tree structures, might cause a second call of the
      {!delete_proof_window} method. This flag is used to avoid this
      double or triple killing.
  *)
  val mutable destroy_in_progress = false

  (** True when this is a clone. *)
  val mutable is_clone = false

  (** A proof is disconnected if it is not the current proof that is
      currently updated by Proof General. Used for the context menu.
  *)
  val mutable disconnected = false

  (** The stack of layers, containing all proof trees belonging to
      this proof.
  *)
  method layer_stack = layer_stack

  (** Return the selected node or [None] if there is none. *)
  method get_selected_node = selected_node

  (** Delete the external node window from {!node_windows}. *)
  method delete_node_window win =
    node_windows <- List.filter (fun owin -> owin <> win) node_windows

  (** Setter for {!is_clone}. *)
  method set_clone_flag = is_clone <- true

  (** Setter for {!position_hints}. *)
  method set_position_hints hints =
    position_hints <- (hints : proof_tree_element list list)

  (** Clear {!position_hints}. *)
  method clear_position_hints = position_hints <- []

  (***************************************************************************
   *
   * Messages
   *
   ***************************************************************************)

  (** Display text in the message label. *)
  method message text = message_label#set_label text

  (***************************************************************************
   *
   * Sequent window
   *
   ***************************************************************************)

  (** Make the last line visible in the sequent area, if
      {!sequent_window_scroll_to_bottom} is [true].

      This is the callback for the changed signal of the vertical
      adjustment of the scrollbar of the sequent area (emitted when
      the sequent area changes its size but not when the scrollbar is
      moved).
  *)
  method sequent_area_changed () =
    if sequent_window_scroll_to_bottom then
      let a = sequent_v_adjustment in
      a#set_value (max a#lower (a#upper -. a#page_size))

  (** [update_sequent_area label content scroll_to_bottom] updates the
      sequent area to show [content] with label [label] on the frame.
      It further sets {!sequent_window_scroll_to_bottom} to
      [scroll_to_bottom].
  *)
  method private update_sequent_area label content scroll_to_bottom =
    labeled_sequent_frame#set_label (Some label);
    sequent_window#buffer#set_text content;
    sequent_window_scroll_to_bottom <- scroll_to_bottom

  (** Clear the sequent area. *)
  method private clear_sequent_area =
    self#update_sequent_area "no sequent" "" false

  (** Refresh the sequent area. If there is a selected node, show it.
      Otherwise, if there is a current sequent node that has a parent
      sequent, then show the parent sequent. Otherwise clear the sequent
      area.
  *)
  method refresh_sequent_area =
    match selected_node with
      | Some node ->
	let (frame_text, scroll_to_bottom) = match node#node_kind with
	  | Turnstile -> ("Selected sequent", true)
	  | Proof_command -> ("Selected command", false)
	in
	self#update_sequent_area frame_text node#displayed_text scroll_to_bottom
      | None -> 
	match current_node with
	  | None -> self#clear_sequent_area
	  | Some node ->
	    if node#node_kind = Turnstile
	    then
	      match node#parent with
		| None -> self#clear_sequent_area
		| Some p -> match p#parent with
		    | None -> self#clear_sequent_area
		    | Some p ->
		      self#update_sequent_area
			"Previous sequent"
			p#displayed_text
			true
	    else
	      self#clear_sequent_area


  (***************************************************************************
   *
   * Current node
   *
   ***************************************************************************)

  (** Set the current node. *)
  method set_current_node n =
    current_node_offset_cache <- None;
    current_node <- Some (n : proof_tree_element)

  (** Clear the current node. *)
  method clear_current_node =
    current_node_offset_cache <- None;
    current_node <- None;


  (***************************************************************************
   *
   * Unclassified methods
   *
   ***************************************************************************)

  (** Tell whether this proof-tree window should stay alive when the
      user retracted to a point before the start of the proof. If the
      window shows more than just the root sequent, it will stay
      alive.
  *)
  method survive_undo_before_start = 
    layer_stack#survive_undo_before_start_hint

  (** Disconnect the proof tree. Clears all current node and current
      branch indications.
  *)
  method disconnect_proof = 
    disconnected <- true;
    layer_stack#disconnect

  (** Reflect changes in the current configuration. *)
  method configuration_updated =
    sequent_window#misc#modify_font !sequent_font_desc;
    drawable#set_line_attributes 
      ~width:(!current_config.turnstile_line_width) ();
    layer_stack#configuration_updated;
    self#expand_drawing_area;
    ignore(self#position_tree);
    GtkBase.Widget.queue_draw top_window#as_widget;
    self#configuration_updated_ext_dialog
      
  (** Clear this window and the existential variable dialog, if there
      is one, for reuse when the proof it displays is started again.
      Deletes and destroys all non-sticky external node windows.
  *)
  method clear_for_reuse =
    disconnected <- false;
    layer_stack#clear_for_reuse;
    current_node <- None;
    current_node_offset_cache <- None;
    selected_node <- None;
    self#refresh_sequent_area;
    List.iter (fun w -> w#delete_attached_node_window) node_windows;
    assert(node_windows = []);
    self#clear_existential_dialog_for_reuse

  (** Update the existentials info in external sequent displays. *)
  method update_sequent_existentials_info =
    layer_stack#update_sequent_existentials_info

  (** Find the first node in the proof tree satisfying the predicate
      using depth-first search.
  *)
  method find_node p = layer_stack#find_node p


  (***************************************************************************
   *
   * Position to nodes and points
   *
   ***************************************************************************)

  (** Make node visible. *)
  method private clamp_to_node node =
    let (x_l, x_u, y_l, y_u) = node#bounding_box top_left top_top in
    drawing_h_adjustment#clamp_page ~lower:x_l ~upper:x_u;
    drawing_v_adjustment#clamp_page ~lower:y_l ~upper:y_u


  (** Move the drawing area to show point [(x,y)] as centre point. *)
  method private centre_point x y =
    let x_size = drawing_h_adjustment#page_size in
    let adj_x_l = drawing_h_adjustment#lower in
    let adj_x_u = drawing_h_adjustment#upper in
    let x = x -. x_size /. 2.0 in
    let x = if x +. x_size > adj_x_u then adj_x_u -. x_size else x in
    drawing_h_adjustment#set_value (max adj_x_l x);
    let y_size = drawing_v_adjustment#page_size in
    let adj_y_l = drawing_v_adjustment#lower in
    let adj_y_u = drawing_v_adjustment#upper in
    let y = y -. y_size /. 2.0 in
    let y = if y +. y_size > adj_y_u then adj_y_u -. y_size else y in
    drawing_v_adjustment#set_value (max adj_y_l y)

  (** Show the given node in the centre of the drawing area. *)
  method private centre_node node =
    let (x_l, x_u, y_l, y_u) = node#bounding_box top_left top_top in
    self#centre_point ((x_l +. x_u) /. 2.0) ((y_l +. y_u) /. 2.0)

  (** Test if the given node is (partially) visible. *)
  method private is_partially_visible node =
    let (node_x_l, node_x_u, node_y_l, node_y_u) = 
      node#bounding_box top_left top_top in
    let in_x = inside_adj_range drawing_h_adjustment in
    let in_y = inside_adj_range drawing_v_adjustment
    in
    ((in_x node_x_l) || (in_x node_x_u))
    && ((in_y node_y_l) || (in_y node_y_u))

  (** Make the given node visible in a user friendly way. *)
  method show_node node =
    if self#is_partially_visible node 
    then self#clamp_to_node node
    else self#centre_node node

  (** Make the two given nodes visible in a user friendly way. If both
      nodes do not fit together in the drawing area, then only the second
      node is shown.
  *)
  method show_both_nodes n1 n2 =
    let (x1_l, x1_u, y1_l, y1_u) = n1#bounding_box top_left top_top in
    let (x2_l, x2_u, y2_l, y2_u) = n2#bounding_box top_left top_top in
    let x_l = min x1_l x2_l in
    let x_u = max x1_u x2_u in
    let y_l = min y1_l y2_l in
    let y_u = max y1_u y2_u in
    (* 
     * Printf.fprintf (debugc()) 
     *   "SBN n1 x %.0f-%.0f y %.0f-%.0f  "
     *   "n2 x %.0f-%.0f y %.0f-%.0f bb x %.0f-%.0f y %.0f-%.0f\n%!"
     *   x1_l x1_u y1_l y1_u
     *   x2_l x2_u y2_l y2_u
     *   x_l x_u y_l y_u;
     *)
    if x_u -. x_l <= drawing_h_adjustment#page_size
      && y_u -. y_l <= drawing_v_adjustment#page_size
    then
      (* both n1 and n2 fit on the page *)
      if self#is_partially_visible n1 || self#is_partially_visible n2
      then begin
	self#clamp_to_node n1;
	self#clamp_to_node n2
      end
      else
	self#centre_point ((x_l +. x_u) /. 2.0) ((y_l +. y_u) /. 2.0)
    else
      self#show_node n2


  (***************************************************************************
   *
   * Key events
   *
   ***************************************************************************)

  (** Delete and destroy this proof-tree window, including all its
      non-sticky external node windows and the existential variable
      dialog. Delete this window from {!cloned_proof_windows}. Other
      data structures in higher-level modules are not touched.

      The destruction process might cause destroy signals which will
      cause this method to be called again. The flag
      {!destroy_in_progress} is used to protect against such cases.
  *)
  method delete_proof_window =
    if destroy_in_progress = false then begin
      destroy_in_progress <- true;
      List.iter (fun w -> w#delete_attached_node_window) node_windows;
      self#destroy_existential_dialog;
      let self = (self :> proof_window) in
      cloned_proof_windows :=
	List.fold_left 
        (fun res w -> if w = self then res else w :: res)
        [] !cloned_proof_windows;
      top_window#destroy()
    end

  (** Callback for the "Dismiss" button and the destroy signal
      (emitted, for instance, when the window manager kills this
      window). Delete and destroy this window as for
      {!delete_proof_window} and delete it from all data structures in
      the module {!Proof_tree}.
  *)
  method user_delete_proof_window () =
    if destroy_in_progress = false then begin
      if is_clone = false then
	!delete_proof_tree_callback proof_name;
      self#delete_proof_window
    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#user_delete_proof_window (); true
      | ks when ks = GdkKeysyms._Left -> 
	scroll_adjustment drawing_h_adjustment (-1); true
      | ks when ks = GdkKeysyms._Right -> 
	scroll_adjustment drawing_h_adjustment 1; true
      | ks when ks = GdkKeysyms._Up -> 
	scroll_adjustment drawing_v_adjustment (-1); true
      | ks when ks = GdkKeysyms._Down -> 
	scroll_adjustment drawing_v_adjustment 1; true

      | ks when (ks = GdkKeysyms._E || ks = GdkKeysyms._e)  -> 
      	self#show_existential_window (); true

      (* 
       * | ks when (ks = GdkKeysyms._C or ks = GdkKeysyms._c)  -> 
       * 	show_config_window (); true
       *)

      | _ -> false


  (***************************************************************************
   *
   * Window for existential variables
   *
   ***************************************************************************)

  (** Clear {!existential_window}. *)
  method existential_clear () = 
    existential_window <- None

  (** Show a dialog for existential variables. If there is currently
      none, a new one is created and initialized.
  *)
  method show_existential_window () =
    match existential_window with
      | Some w -> w#present
      | None -> 
	let ext = 
	  make_ext_dialog (self :> proof_window) proof_name 
	in
	layer_stack#init_ext_dialog ext;
	ext#finish_table_init;
	existential_window <- Some ext

  (** Destroy the existential variables dialog, if one is present. *)
  method private destroy_existential_dialog =
    match existential_window with
      | None -> ()
      | Some w -> 
	w#destroy ();
	existential_window <- None

  (** Prepare the existential variable dialog for reuse, if there is
      one.
  *)
  method private clear_existential_dialog_for_reuse =
    match existential_window with
      | None -> ()
      | Some w -> w#clear_for_reuse

  (** Schedule some existentials to be added to the existential
      variable dialog, if there is one.
  *)
  method ext_dialog_add new_ext =
    match existential_window with
      | Some w -> w#change_and_add new_ext
      | None -> ()

  (** Schedule some existentials to be removed from the existential
      variable dialog, if there is one.
  *)
  method ext_dialog_undo remove_ext =
    match existential_window with
      | Some w -> w#change_and_delete remove_ext
      | None -> ()

  (** Process all pending requests for the existential variable
      dialog, if there is one.
  *)
  method update_ext_dialog =
    match existential_window with
      | Some w -> w#update_ext_dialog
      | None -> ()

  (** Ask the existential variable dialog to reflect changes in the
      current configuration.
  *)
  method private configuration_updated_ext_dialog =
    match existential_window with
      | Some w -> w#configuration_updated
      | None -> ()

  (***************************************************************************
   *
   * Redraw / expose events
   *
   ***************************************************************************)

  (** Return the relative bounding box of the current node, see
      {!current_node_offset_cache}. If there nothing in the cache, try
      to fill it. Return [None] if there is no current node.
  *)
  method private get_current_offset =
    match current_node_offset_cache with
      | Some _ as res -> res
      | None -> match current_node with
	  | None -> None
	  | Some node ->
	    let res = Some node#bounding_box_offsets in
	    current_node_offset_cache <- res;
	    res

  (** Erase the complete drawing area. *)
  method private erase = 
    (* Printf.fprintf (debugc()) "ERASE\n%!"; *)
    let (x,y) = drawable#size in
    let gc = save_gc drawable in
    let bg = top_window#misc#style#bg `PRELIGHT in
    (* let bg = drawable#get_background in *)
    (* drawable#set_foreground (`NAME("gray85")); *)
    drawable#set_foreground (`COLOR bg);
    drawable#polygon ~filled:true [(0,0); (x,0); (x,y); (0,y)];
    restore_gc drawable gc

  (** Try to change the scrollbars of the drawing area such that the
      current node becomes visible in the bottom part. Do nothing if
      {!position_to_current_node} is [false]. Making the current node
      visible might be impossible, because the resize request for the
      drawing area might not have been processed yet. In this case
      {!position_to_current_node} stays true and this method is called
      again at some later stage.
  *)
  method private try_adjustment = 
    if position_to_current_node = true then
      match self#get_current_offset with
	| None -> 
	  position_to_current_node <- false
	| Some((x_l_off, x_u_off, y_l_off, y_u_off)) ->
	  let x_page_size = int_of_float drawing_h_adjustment#page_size in
	  let y_page_size = int_of_float drawing_v_adjustment#page_size in
	  let x_l_f = float_of_int(top_left + x_l_off) in
	  let x_u_f = float_of_int(top_left + x_u_off) in
	  let y_l_f = float_of_int(top_top + y_l_off) in
	  let y_u_i = top_top + y_u_off in
	  let y_u_f = float_of_int y_u_i in
	  (* 
           * Printf.fprintf (debugc()) 
	   *   "TRY ADJUSTMENT x %.1f-%.1f y %.1f-%.1f\n%!"
	   *   x_l_f x_u_f y_l_f y_u_f;
           *)
	  let success = ref true in
          (* The following code might immediately trigger
	   * expose events, which will call try_adjustment again. To avoid
	   * entering this function a second time before leaving it, I
	   * temporarily switch position_to_current_node off.
	   *)
	  position_to_current_node <- false;

	  if x_page_size >= (x_u_off - x_l_off) && 
	    y_page_size >= (y_u_off - y_l_off)
	  then begin
	    (* current node fits into the viewport, be sophisticated *)
	    let req_width = layer_stack#width in
	    let req_height = layer_stack#height in
	    if (float_of_int req_width) > drawing_h_adjustment#upper ||
	       (float_of_int req_height) > drawing_v_adjustment#upper
	    then begin
	      (* The resize request for the drawing area has not 
	       * been processed yet. It might happen that this resize
	       * request causes the addition of some scrollbars. In
	       * this case the viewport gets smaller and the 
	       * current node would possible (partially) hidden.
	       * Therefore we mimic an adjustment error. Note that 
	       * in this case also clamp_page would not give a proper
	       * adjustment.
	       *)
	      success := false;
	      (* Printf.fprintf (debugc()) "clever forced error %!" *)
	    end else begin
	      let y_val = 
		max drawing_v_adjustment#lower 
		  (float_of_int (y_u_i - y_page_size))
	      in
	      drawing_v_adjustment#set_value y_val;

	      (* make now the _h_adjustment, first try if one of the 
               * hint nodes can be made visible as well
	       *)
	      if 
		List.exists
		  (fun hint_nodes ->
		    let (off_l, off_u) =
		      List.fold_left
			(fun (off_l, off_u) hint_node ->
			  let (h_x_l_off, h_x_u_off, _, _) = 
			    hint_node#bounding_box_offsets 
			  in
			  (min off_l h_x_l_off, max off_u h_x_u_off))
			(x_l_off, x_u_off)
			hint_nodes
		    in
		    if x_page_size >= (off_u - off_l)
		    then begin
		      (* the hints fit *)
		      drawing_h_adjustment#clamp_page
			~lower:(float_of_int (top_left + off_l))
			~upper:(float_of_int (top_top + off_u));
		      true
		    end else 
		      (* the hints don't fit *)
		      false
		  )
		  position_hints
	      then ()
	      else
		drawing_h_adjustment#clamp_page ~lower:x_l_f ~upper:x_u_f;
	      (* 
               * Printf.fprintf (debugc()) "clever y_u_i %d up %d y_val %d %!"
	       * 	y_u_i
	       * 	(int_of_float drawing_v_adjustment#upper)
	       * 	(int_of_float y_val);
               *)
	    end
	  end else begin
	    (* very small viewport, use dump strategy *)
	    (* Printf.fprintf (debugc()) "dump clamp %!"; *)
	    drawing_h_adjustment#clamp_page ~lower:x_l_f ~upper:x_u_f;
	    drawing_v_adjustment#clamp_page ~lower:y_l_f ~upper:y_u_f;
	  end;

	  if !success && 
	    range_inside_adj_range drawing_h_adjustment x_l_f x_u_f &&
	    range_inside_adj_range drawing_v_adjustment y_l_f y_u_f
	  then begin
	    (* Printf.fprintf (debugc()) "SUCCESSFUL\n%!"; *)
	    () (* Do nothing: leave position_to_current_node disabled *)
	  end else begin
	    (* Printf.fprintf (debugc()) "UNSUCCESSFUL %b\n%!" !success; *)
	    (* Schedule the adjustment again, hope that we are more
	     * successful next time.
	     *)
	    position_to_current_node <- true;
	  end;
          (* 
           * (let a = drawing_h_adjustment in
	   *  Printf.fprintf (debugc()) 
	   *    ("TA HADJ low %.1f val %.1f " ^^ 
	   * 	 "up %.1f size %.1f step %.1f page %.1f\n%!")
	   *    a#lower a#value a#upper a#page_size 
	   *    a#step_increment a#page_increment);
           * (let a = drawing_v_adjustment in
	   *  Printf.fprintf (debugc()) 
	   *    ("TA VADJ low %.1f val %.1f " ^^
	   * 	 "up %.1f size %.1f step %.1f page %.1f\n%!")
	   *    a#lower a#value a#upper a#page_size 
	   *    a#step_increment a#page_increment);
           *)
	  ()

  (** Request the drawing are to change its size to the size of the
      current proof tree.
  *)
  method private expand_drawing_area =
    let new_width = layer_stack#width in
    let new_height = layer_stack#height in
    (* 
     * Printf.fprintf (debugc()) "DRAWING AREA SIZE REQUEST %d x %d\n%!" 
     *   new_width new_height;
     *)
    (* 
     * if new_width > current_width || new_height > current_height then
     *   drawing_area#misc#set_size_request
     * 	~width:(max current_width new_width)
     * 	~height:(max current_height new_height) ();
     *)
    drawing_area#misc#set_size_request ~width:new_width ~height:new_height ();

  (** Sets the position of the proof tree in the drawing area by 
      computing [top_left]. Returns true if the position changed. 
      In that case the complete drawing area must be redrawn.
  *)
  method private position_tree =
    let old_top_left = top_left in
    let (width, _) = drawable#size in
    top_left <- max 0 ((width - layer_stack#width) / 2);
    top_left <> old_top_left

  (** Handle expose events. Try to move to the current node, erase and
      redraw the complete drawing area.
  *)
  method private redraw =
    (* 
     * (let a = drawing_v_adjustment in
     *  Printf.fprintf (debugc()) 
     *    "RD %s VADJ low %f val %f up %f size %f step %f page %f\n%!"
     *    (match scheduled_adjustment with | None -> "N" | Some _ -> "S")
     *    a#lower a#value a#upper a#page_size 
     *    a#step_increment a#page_increment);
     *)
    self#try_adjustment;
    self#erase;
    (* Printf.fprintf (debugc()) "REDRAW\n%!"; *)
    layer_stack#draw top_left top_top

  (** Schedule an expose event for the drawing area, thereby causing
      it to get redrawn.
  *)
  method invalidate_drawing_area =
    (* Printf.fprintf (debugc()) "INVALIDATE\n%!"; *)
    GtkBase.Widget.queue_draw drawing_area#as_widget

  (** Method for updating the display after the proof tree has changed.
      Adjusts the tree position in the drawing area, schedules a 
      complete redraw and make the current node (if any) visible.
  *)
  method refresh_and_position =
    (* Printf.fprintf (debugc()) "REFRESH & POSITION\n%!"; *)
    position_to_current_node <- true;
    self#expand_drawing_area;
    ignore(self#position_tree);
    self#try_adjustment;
    self#invalidate_drawing_area;
    (* Printf.fprintf (debugc()) "REFRESH & POSITION END\n%!"; *)
    ()

  (** Position the current node in the bottom part of the drawing
      area.
  *)
  method reposition_current_node () =
    position_to_current_node <- true;
    self#try_adjustment

  (** Make the current node visible in a user friendly way. *)
  method show_current_node () =
    match current_node with
      | None -> ()
      | Some current ->
	if self#is_partially_visible current
	then self#show_node current
	else self#reposition_current_node ()

  (** Make the selected node visible in a user friendly way. *)
  method show_selected_node () =
    match selected_node with
      | None -> ()
      | Some selected -> self#show_node selected

  (** Callback for the size_allocate signal of the drawing area.
      Position the proof tree in the viewport of the drawing area and
      redraw.
  *)
  method draw_scroll_size_allocate_callback (_size : Gtk.rectangle) =
    (* 
     * Printf.fprintf (debugc()) "SCROLLING SIZE ALLOC SIGNAL size %d x %d\n%!"
     *   (int_of_float (drawing_h_adjustment#upper +. 0.5))
     *   (int_of_float (drawing_v_adjustment#upper +. 0.5));
     *)
    let need_redraw = self#position_tree in
    (* 
     * (let a = drawing_v_adjustment in
     *  Printf.fprintf (debugc()) 
     *    "SA %s VADJ low %f val %f up %f size %f step %f page %f\n%!"
     *    (match scheduled_adjustment with | None -> "N" | Some _ -> "S")
     *    a#lower a#value a#upper a#page_size 
     *    a#step_increment a#page_increment);
     *)
    self#try_adjustment;
    if need_redraw 
    then self#invalidate_drawing_area

  (* 
   * method draw_area_size_allocate_callback (_size : Gtk.rectangle) =
   *   Printf.fprintf (debugc()) "AREA SIZE ALLOC SIGNAL size %d x %d\n%!"
   *     (int_of_float (drawing_h_adjustment#upper +. 0.5))
   *     (int_of_float (drawing_v_adjustment#upper +. 0.5));
   *)
  
  (* 
   * method draw_area_configure_callback configure_event =
   *   Printf.fprintf (debugc()) 
   *     "AREA CONFIGURE SIGNAL area size %d x %d scroll size %d x %d\n%!"
   *     (GdkEvent.Configure.width configure_event)
   *     (GdkEvent.Configure.height configure_event)
   *     (int_of_float (drawing_h_adjustment#upper +. 0.5))
   *     (int_of_float (drawing_v_adjustment#upper +. 0.5));
   *   false
   *)

  (** Callback for exposure events. Redraw the complete tree. *)
  method expose_callback (_ev : GdkEvent.Expose.t) =
    (* 
     * let r = GdkEvent.Expose.area ev in
     * Printf.fprintf (debugc()) "EXPOSE count %d %d x %d at %d x %d\n%!"
     *   (GdkEvent.Expose.count ev)
     *   (Gdk.Rectangle.width r) (Gdk.Rectangle.height r)
     *   (Gdk.Rectangle.x r) (Gdk.Rectangle.y r);
     *)
    (* 
     * (let a = drawing_v_adjustment in
     *  Printf.fprintf (debugc())
     * "EX VADJ low %f val %f up %f size %f step %f page %f\n%!"
     *    a#lower a#value a#upper a#page_size 
     *    a#step_increment a#page_increment);
     *)
    (* 
     * (let a = drawing_h_adjustment in
     *  Printf.fprintf (debugc())
     * "HADJ low %f val %f up %f size %f step %f page %f\n"
     *    a#lower a#value a#upper a#page_size a#step_increment a#page_increment);
     * (let a = drawing_v_adjustment in
     *  Printf.fprintf (debugc())
     * "VADJ low %f val %f up %f size %f step %f page %f\n%!"
     *    a#lower a#value a#upper a#page_size a#step_increment a#page_increment);
     *)
    self#redraw;
    (* prerr_endline "END EXPOSE EVENT"; *)
    false


  (***************************************************************************
   *
   * numbers for external node windows
   *
   ***************************************************************************)

  (** Counter for external node windows. *)
  val mutable last_node_number = 0

  (** Return the number for the next external node window. *)
  method private next_node_number =
    last_node_number <- last_node_number + 1;
    last_node_number


  (***************************************************************************
   *
   * Button events
   *
   ***************************************************************************)

  (** The dragging feature has the problem that it changes the
      viewport to the drawing area, which itself generates pointer
      motion events for the drawing area. The approach is therefore to
      remember the mouse position at the start of the dragging (i.e.,
      the button press) in coordinates relative to the complete X
      window.

      X position of the mouse at the last button press relative to
      [top_window]. 
  *)
  val mutable last_button_press_top_x = 0

  (** Y position of the mouse at the last button press relative to
      [top_window]. *)
  val mutable last_button_press_top_y = 0

  (** Value of the vertical scrollbar at the last button press. *)
  val mutable last_button_press_v_adjustment_value = 0.0

  (** Value of the horizontal scrollbar at the last button press. *)
  val mutable last_button_press_h_adjustment_value = 0.0

  (** Fill {!last_button_press_top_x}, {!last_button_press_top_y},
      {!last_button_press_v_adjustment_value} and
      {!last_button_press_h_adjustment_value} in case dragging
      follows.
  *)
  method private remember_for_dragging =
    let (x, y) = Gdk.Window.get_pointer_location top_window#misc#window in
    (* 
     * Printf.fprintf (debugc()) "Button press %d x %d\n%!" 
     *   (fst new_poi_loc) (snd new_poi_loc);
     *)
    last_button_press_top_x <- x;
    last_button_press_top_y <- y;
    last_button_press_v_adjustment_value <- drawing_v_adjustment#value;
    last_button_press_h_adjustment_value <- drawing_h_adjustment#value;


  (** We have different and incompatible actions for single and double
      clicks and for dragging. Because single click events do always occur
      before double clicks and dragging events, we have to undo the
      changes that were done for the single click. A double click is of
      course always preceeded by two single clicks. 

      Remember the selected node state before the last but one
      mouse press. This state needs to get reestablished when we
      detect a double click.
  *)
  val mutable old_old_selected_node = None

  (** Remember the selected node state before the last mouse press.
      This state needs to get reestablished on dragging events.
  *)
  val mutable old_selected_node = None

  (** Remember if we have already restored the selected node state
      since the last button press.
  *)
  val mutable restored_selected_node = false

  (** Reset the selected node state to state [node_opt] and update
      drawing and sequent area.
  *)
  method set_selected_node node_opt =
    (match selected_node with
      | None -> ()
      | Some node -> node#selected false);
    selected_node <- node_opt;
    (match node_opt with
      | None -> ()
      | Some node -> node#selected true);
    self#invalidate_drawing_area;
    self#refresh_sequent_area

  (** Make the root node the selected node or clear the selected node
      if there is no root node
  *)
  method select_root_node =
    self#set_selected_node (layer_stack#get_root_node)

  (** Save the selected node state on a button press and clear
      {!restored_selected_node}. 
  *)
  method private save_selected_node_state =
    old_old_selected_node <- old_selected_node;
    old_selected_node <- selected_node;
    restored_selected_node <- false

  (** Restore the selected node state when we detect mouse dragging
      for the first time. Sets {!restored_selected_node}.
  *)
  method private single_restore_selected_node =
    self#set_selected_node old_selected_node;
    restored_selected_node <- true

  (** Restore the selected node state after we detected a double
      click.
  *)
  method private double_restore_selected_node =
    self#set_selected_node old_old_selected_node;
    restored_selected_node <- true

  (** [locate_button_node x y found notfound] tries to locate a proof
      tree element on position [(x, y)]. If there is one [found] is called
      with this element. If there is nothing [notfound] is called.
  *)
  method private locate_button_node : 
    'a . int -> int -> (#proof_tree_element -> 'a) -> (unit -> 'a) -> 'a =
    fun x y node_click_fun outside_click_fun ->
      match layer_stack#find_node_for_point_in_layer_stack 
	                              top_left top_top x y with
	| None -> outside_click_fun ()
	| Some node -> node_click_fun node

  (** Display an external node window for the argument node. *)
  method private external_node_window (node : proof_tree_element) =
    let n = string_of_int(self#next_node_number) in
    let win = 
      make_node_window (self :> proof_window) proof_name node n 
    in 
    node_windows <- win :: node_windows;
    self#invalidate_drawing_area

  (** Method to handle button one press events. Receives as arguments
      the coordinates, a flag for the shift modifier and a flag to
      indicate a double click.
  *)
  method private button_1_press x y shifted double =
    self#remember_for_dragging;
    if (not double) && (not shifted)
    then self#save_selected_node_state;
    if double && (not shifted)
    then self#double_restore_selected_node;
    if double || shifted 
    then self#locate_button_node x y self#external_node_window (fun () -> ())
    else 
      self#locate_button_node x y 
	(fun node -> self#set_selected_node (Some node))
	(fun () -> self#set_selected_node None)

  (* val mutable last_button_press_time = 0l *)

  (** Generic call back for all button press events. *)
  method button_press ev =
    let x = int_of_float(GdkEvent.Button.x ev +. 0.5) in
    let y = int_of_float(GdkEvent.Button.y ev +. 0.5) in
    let button = GdkEvent.Button.button ev in
    let shifted = Gdk.Convert.test_modifier `SHIFT (GdkEvent.Button.state ev) in
    let double = match GdkEvent.get_type ev with
      | `BUTTON_PRESS -> false
      | `TWO_BUTTON_PRESS -> true
      | `THREE_BUTTON_PRESS -> false
      | `BUTTON_RELEASE -> false
    in
    (* 
     * let state = B.state ev in
     * let mod_list = Gdk.Convert.modifier state in
     * let _ = Gdk.Convert.test_modifier `SHIFT state in
     *)
    (* 
     * let time_diff = 
     * Int32.sub (GdkEvent.Button.time ev) last_button_press_time 
     * in
     * last_button_press_time <- GdkEvent.Button.time ev;
     *)
    (* 
     * (let h = drawing_h_adjustment in
     *  let v = drawing_v_adjustment in
     *  Printf.fprintf (debugc()) 
     *    "%s Button %s%d at %d x %d | x: %1.f - %.1f y: %.1f - %.1f\n%!" 
     *    (match GdkEvent.get_type ev with
     * 	 | `BUTTON_PRESS -> "single"
     * 	 | `TWO_BUTTON_PRESS -> "double"
     * 	 | `THREE_BUTTON_PRESS -> "triple"
     * 	 | `BUTTON_RELEASE -> "release")
     *    (if shifted then "shift " else "")
     *    button x y
     *    h#value (h#value +. h#page_size)
     *    v#value (v#value +. v#page_size));
     *)
    (match button with
      | 1 -> self#button_1_press x y shifted double
      | 3 -> self#context_menu x y button (GdkEvent.Button.time ev)
      | _ -> ());
    true


  (***************************************************************************
   *
   * Pointer motion events
   *
   ***************************************************************************)

  (** Action for a pointer motion event that is part of dragging.
      Moves the viewport to the drawing area relative to the mouse position
      when dragging started.
  *)
  method pointer_motion (_ev : GdkEvent.Motion.t) =
    let (x, y) = Gdk.Window.get_pointer_location top_window#misc#window in
    let new_h_value = 
      last_button_press_h_adjustment_value +.
    	!current_config.button_1_drag_acceleration *.
	(float_of_int (x - last_button_press_top_x))
    in
    let new_v_value = 
      last_button_press_v_adjustment_value +.
    	!current_config.button_1_drag_acceleration *. 
	(float_of_int (y - last_button_press_top_y))
    in
    (* 
     * let hint = GdkEvent.Motion.is_hint _ev in
     * Printf.fprintf (debugc()) 
     * "PM %d %d%s\n%!" x y (if hint then " H" else "");
     *)
    if not restored_selected_node 
    then self#single_restore_selected_node;
    drawing_h_adjustment#set_value 
      (min new_h_value 
    	 (drawing_h_adjustment#upper -. drawing_h_adjustment#page_size));
    drawing_v_adjustment#set_value 
      (min new_v_value
    	 (drawing_v_adjustment#upper -. drawing_v_adjustment#page_size));
    (* 
     * last_button_1_x <- x;
     * last_button_1_y <- y;
     *)
    true

  (** General callback for all pointer motion events.  *)
  method pointer_general_motion (ev : GdkEvent.Motion.t) =
    if Gdk.Convert.test_modifier `BUTTON1 (GdkEvent.Motion.state ev)
    then self#pointer_motion ev
    else false


  (***************************************************************************
   *
   * menu actions
   *
   ***************************************************************************)

  (** Field to store the undo state number. This number is determined
      when the context menu is posted and is needed in the callback for
      the undo menu entry. *)
  val mutable context_menu_undo_state = None

  (** Field to store the proof command under the mouse when the
      context menu is posted. This node is needed for sending proof
      commands and proof scripts. To avoid a memory leak, this field
      is cleared with an idle action, see {!context_menu_deactivated}.
  *)
  val mutable context_menu_node = None

  (** Callback for the undo menu entry. *)
  method undo_to_point () = 
    match context_menu_undo_state with
      | None -> assert false
      | Some state -> emacs_callback_undo state

  (** Callback for inserting one proof command. *)
  method insert_proof_command () = 
    match context_menu_node with
      | None -> assert false
      | Some node -> emacs_send_proof_script node#content

  (** Callback for inserting all proof commands of a subtree. *)
  method insert_subproof () =
    let buf = Buffer.create 4095 in
    let rec collect node indent =
      Buffer.add_string buf (String.make indent ' ');
      Buffer.add_string buf node#content;
      Buffer.add_char buf '\n';
      let sequents = node#children in
      ignore(
	List.fold_left
	  (fun indent sequent ->
	    match sequent#children with
	      | [pc] -> collect pc indent; indent - 2
	      | [] -> indent - 2        (* happens for the current sequent *)
	      | _ -> assert false)
	  (indent + (2 * List.length sequents) - 2)
	  sequents)
    in
    match context_menu_node with
      | None -> assert false
      | Some node -> 
	collect node 0;
	emacs_send_proof_script (Buffer.contents buf)

  (** Post the context menu. Depending on where the mouse button is
      pressed, certain menu entries as disabled. The undo state is
      stored in {!context_menu_undo_state} for use in the callback for
      the undo entry.
  *)
  method context_menu x y button time =
    self#locate_button_node x y
      (fun node -> 
	context_menu_node <- Some node;
	let undo_state = 
	  if disconnected then None
	  else
	    match node#node_kind with
	      | Proof_command -> None
	      | Turnstile -> match node#children with
		  | first :: _ -> Some first#undo_state
		  | _ -> None
	in
	context_menu_undo_state <- undo_state;
	(List.nth context_menu#children 0)#misc#set_sensitive
	  (undo_state <> None);
	(List.nth context_menu#children 1)#misc#set_sensitive
	  (node#node_kind = Proof_command);
	(List.nth context_menu#children 2)#misc#set_sensitive
	  (node#node_kind = Proof_command);
	context_menu#popup ~button ~time;
      )
      (fun () ->
	List.iter
	  (fun n ->
	    (List.nth context_menu#children n)#misc#set_sensitive false)
	  [0; 1; 2];
	context_menu#popup ~button ~time
      )

  (** Callback for the deactivated signal of the context menu.
      Unfortunately, this signal is processed before the callback for
      the selected menu item is processed. Therefore, the
      {!context_menu_node} cannot be cleared directly but only in an
      idle action.
  *)
  method context_menu_deactivated () =
    ignore(GMain.Idle.add (fun () -> context_menu_node <- None; false))


  (***************************************************************************
   *
   * tooltips
   *
   ***************************************************************************)
      
  (** Callback for the query tooltip event. Display a tool-tip if
      there is a sequent node or an abbreviated proof command node.
  *)
  method drawable_tooltip ~x ~y ~kbd:(_kbd : bool) (tooltip : Gtk.tooltip) =
    (* Printf.fprintf (debugc()) "TTS x %d y %d\n%!" x y; *)
    self#locate_button_node x y 
      (fun node -> match node#node_kind with
	| Turnstile -> 
	  if !current_config.display_turnstile_tooltips then begin
	    let contents = GMisc.label ~text:node#displayed_text () in
	    GtkBase.Tooltip.set_custom tooltip contents#as_widget;
	    true
	  end 
	  else false
	| Proof_command ->
	  if !current_config.display_command_tooltips && node#content_shortened
	  then begin
	    let contents = GMisc.label ~text:node#displayed_text () in
	    GtkBase.Tooltip.set_custom tooltip contents#as_widget;
	    true
	  end
	  else false
      )
      (fun () -> false)


  (***************************************************************************
   *
   * Cloning
   *
   ***************************************************************************)

  (** Callback for the clone menu item. Creates and displays a clone
      window.
  *)
  method clone (owin : proof_window) =
    owin#set_clone_flag;
    let old_selected = match current_node with
      | Some _ -> current_node
      | None -> selected_node
    in
    let cloned_selected = ref None in
    let cloned_layers = 
      layer_stack#clone_layers (owin#new_proof_command 0) (owin#new_turnstile 0)
        old_selected cloned_selected in
    owin#layer_stack#set_layers cloned_layers;
    owin#set_selected_node !cloned_selected;
    owin#refresh_and_position;
    cloned_proof_windows := owin :: !cloned_proof_windows


  (***************************************************************************
   *
   * Proof element creation
   *
   ***************************************************************************)

  (** Create a new turnstile node for sequents. *)
  method new_turnstile undo_state sequent_id sequent_text_option =
    new turnstile drawable undo_state sequent_id sequent_text_option

  (** Create a new proof command node. *)
  method new_proof_command undo_state command 
                           inst_existentials new_existentials =
    new proof_command drawable undo_state command command 
      (inst_existentials : existential_variable list)
      (new_existentials : existential_variable list)
end



(*****************************************************************************
 *
 * proof window creation
 *
 *****************************************************************************)

(** Create a new proof tree window. Creates the widget hierarchy, the
    menu, initializes the management object and registers all
    callbacks.
*)
let rec make_proof_window name geometry_string =
  let top_window = GWindow.window () in
  top_window#set_default_size 
    ~width:!current_config.default_width_proof_tree_window
    ~height:!current_config.default_height_proof_tree_window;
  (* top_v_box for the pane and the button hbox *)
  let top_v_box = GPack.vbox ~packing:top_window#add () in
      (* top_paned for the drawing area and the sequent *)
  let top_paned = GPack.paned `VERTICAL 
    ~packing:(top_v_box#pack ~expand:true) ()
  in
  let drawing_scrolling = GBin.scrolled_window (* ~border_width:1 *)
    ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC 
    ~packing:(top_paned#pack1 ~resize:true ~shrink:false) () 
  in
  let drawing_h_adjustment = drawing_scrolling#hadjustment in
  let drawing_v_adjustment = drawing_scrolling#vadjustment in
  let drawing_area = GMisc.drawing_area 
    ~packing:drawing_scrolling#add_with_viewport () 
  in
  let _ = drawing_area#misc#realize () in
  let drawable = 
    new better_drawable drawing_area#misc#window 
      drawing_area#misc#create_pango_context
  in
  let outer_sequent_frame = GBin.frame ~shadow_type:`IN 
    ~packing:(top_paned#pack2 ~resize:false ~shrink:true) () 
  in
  let labeled_sequent_frame = GBin.frame ~label:"no sequent" ~shadow_type:`NONE
    ~packing:outer_sequent_frame#add ()
  in
  let sequent_scrolling = GBin.scrolled_window 
    ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC 
    ~packing:labeled_sequent_frame#add () 
  in
  (* 
   * let sequent_h_adjustment = sequent_scrolling#hadjustment in
   *)
  let sequent_v_adjustment = sequent_scrolling#vadjustment in
  sequent_scrolling#misc#modify_font !sequent_font_desc;
  let context = sequent_scrolling#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
  let sequent_window = GText.view ~editable:false ~cursor_visible:false
    ~height:(char_height * !current_config.internal_sequent_window_lines)
    ~packing:sequent_scrolling#add () 
  in
  sequent_window#misc#modify_font !sequent_font_desc;

  (* bottom button line with the message in the middle *)
  let button_box_align = GBin.alignment
    ~padding:(1,1,3,3)			(* (top, bottom, left, right)*)
    ~packing:(top_v_box#pack) () in
  let button_h_box = GPack.hbox
    ~packing:button_box_align#add () in
  let dismiss_button = 
    GButton.button ~stock:`CLOSE ~packing:button_h_box#pack ()
  in
  let message_label =
    GMisc.label ~selectable:true ~ellipsize:`END 
      ~packing:(button_h_box#pack ~expand:true ~fill:true) ()
  in
  message_label#set_use_markup true;
  let menu_button = 
    GButton.button ~label:"Menu" ~packing:(button_h_box#pack) ()
  in

  let main_menu = GMenu.menu () in

  let context_menu = GMenu.menu () in

  let proof_window = 
    new proof_window top_window 
      drawing_h_adjustment drawing_v_adjustment drawing_area
      drawable labeled_sequent_frame sequent_window sequent_v_adjustment
      message_label context_menu name
  in
  let clone_fun () =
    let owin = make_proof_window name geometry_string in
    proof_window#clone owin
  in

  let main_menu_entries = 
    [`I("Clone", clone_fun);
     `I("Show current", proof_window#reposition_current_node);
     `I("Show selected", proof_window#show_selected_node);
     `I("Existentials", proof_window#show_existential_window);
     `I("Configuration", show_config_window);
     `I("Help", show_help_window);
     `I("About", show_about_window);
     `I("Exit", (fun _ -> exit 0));
    ] in
  let context_menu_entries =
    [`I("Undo to point", proof_window#undo_to_point);
     `I("Insert command", proof_window#insert_proof_command);
     `I("Insert subproof", proof_window#insert_subproof);
     `S
    ] @ main_menu_entries
  in
  GToolbox.build_menu main_menu ~entries:main_menu_entries;
  GToolbox.build_menu context_menu ~entries:context_menu_entries;
  ignore(context_menu#connect#deactivate 
           ~callback:(proof_window#context_menu_deactivated));

  top_window#set_title (name ^ " proof tree");
  drawable#set_line_attributes 
    ~width:(!current_config.turnstile_line_width) ();
  drawing_area#misc#set_has_tooltip true;
  ignore(drawing_area#misc#connect#query_tooltip
   	   ~callback:proof_window#drawable_tooltip);
  ignore(drawing_scrolling#misc#connect#size_allocate
	   ~callback:proof_window#draw_scroll_size_allocate_callback);
  (* 
   * ignore(drawing_area#misc#connect#size_allocate
   * 	   ~callback:proof_window#draw_area_size_allocate_callback);
   *)
  (* 
   * ignore(drawing_area#event#connect#configure
   * 	   ~callback:proof_window#draw_area_configure_callback);
   *)

  ignore(top_window#connect#destroy 
	   ~callback:proof_window#user_delete_proof_window);

  (* the delete event yields a destroy signal if not handled *)
  (* ignore(top_window#event#connect#delete 
     ~callback:proof_window#delete_proof_window); *)

    (* 
     * ignore(drawing_area#misc#set_can_focus true);
     * ignore(drawing_area#event#connect#key_press 
     *                  proof_window#key_pressed_callback);
     *)
  ignore(top_window#event#connect#key_press 
	   ~callback:proof_window#key_pressed_callback);
  ignore(drawing_area#event#connect#expose 
	   ~callback:proof_window#expose_callback);
  (* ignore(drawing_area#misc#connect#size_allocate ~callback:resize); *)

  (* events to receive: 
   *  - all button presses, 
   *  - pointer motion when button 1 is pressed
   *  - reduced number of pointer motion events
   *)
  ignore(drawing_area#event#add 
	   [`BUTTON_PRESS; `BUTTON1_MOTION; `POINTER_MOTION_HINT]);
  ignore(drawing_area#event#connect#button_press 
	   ~callback:proof_window#button_press);
  ignore(drawing_area#event#connect#motion_notify
	   ~callback:proof_window#pointer_general_motion);

  ignore(sequent_v_adjustment#connect#changed 
	   ~callback:proof_window#sequent_area_changed);

  ignore(dismiss_button#connect#clicked 
	   ~callback:proof_window#user_delete_proof_window);
  ignore(menu_button#connect#clicked 
	   ~callback:(fun () -> 
	     main_menu#popup ~button:0 
	       ~time:(GtkMain.Main.get_current_event_time ())));

  top_window#show ();
  if geometry_string <> "" then
    ignore(top_window#parse_geometry geometry_string);
  if !current_config.internal_sequent_window_lines = 0 then
    top_paned#set_position (top_paned#max_position);

  proof_window