/
coqide.ml
2245 lines (2091 loc) · 86.2 KB
/
coqide.ml
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
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Preferences
open Gtk_parsing
open Ideutils
type flag = [ `COMMENT | `UNSAFE ]
type ide_info = {
start : GText.mark;
stop : GText.mark;
flags : flag list;
}
class type _analyzed_view =
object
method filename : string option
method stats : Unix.stats option
method update_stats : unit
method revert : unit
method auto_save : unit
method save : string -> bool
method save_as : string -> bool
method get_insert : GText.iter
method get_start_of_input : GText.iter
method go_to_insert : Coq.handle -> unit
method go_to_next_occ_of_cur_word : unit
method go_to_prev_occ_of_cur_word : unit
method tactic_wizard : Coq.handle -> string list -> unit
method insert_message : string -> unit
method process_next_phrase : Coq.handle -> bool -> unit
method process_until_end_or_error : Coq.handle -> unit
method recenter_insert : unit
method erroneous_reset_initial : Coq.handle -> unit
method requested_reset_initial : Coq.handle -> unit
method set_message : string -> unit
method raw_coq_query : Coq.handle -> string -> unit
method show_goals : Coq.handle -> unit
method backtrack_last_phrase : Coq.handle -> unit
method help_for_keyword : unit -> unit
end
type viewable_script = {
script : Wg_ScriptView.script_view;
tab_label : GMisc.label;
proof_view : Wg_ProofView.proof_view;
message_view : Wg_MessageView.message_view;
analyzed_view : _analyzed_view;
toplvl : Coq.coqtop;
command : Wg_Command.command_window;
finder : Wg_Find.finder;
}
let kill_session s =
(* To close the detached views of this script, we call manually
[destroy] on it, triggering some callbacks in [detach_view].
In a more modern lablgtk, rather use the page-removed signal ? *)
s.script#destroy ();
Coq.close_coqtop s.toplvl
let build_session s =
let session_paned = GPack.paned `VERTICAL () in
let session_box =
GPack.vbox ~packing:(session_paned#pack1 ~shrink:false ~resize:true) ()
in
let eval_paned = GPack.paned `HORIZONTAL ~border_width:5
~packing:(session_box#pack ~expand:true) () in
let script_frame = GBin.frame ~shadow_type:`IN
~packing:eval_paned#add1 () in
let script_scroll = GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC
~packing:script_frame#add () in
let state_paned = GPack.paned `VERTICAL
~packing:eval_paned#add2 () in
let proof_frame = GBin.frame ~shadow_type:`IN
~packing:state_paned#add1 () in
let proof_scroll = GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC
~packing:proof_frame#add () in
let message_frame = GBin.frame ~shadow_type:`IN
~packing:state_paned#add2 () in
let message_scroll = GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC
~packing:message_frame#add () in
let session_tab = GPack.hbox ~homogeneous:false () in
let img = GMisc.image ~icon_size:`SMALL_TOOLBAR
~packing:session_tab#pack () in
let _ =
s.script#buffer#connect#modified_changed
~callback:(fun () -> if s.script#buffer#modified
then img#set_stock `SAVE
else img#set_stock `YES) in
let _ =
eval_paned#misc#connect#size_allocate
~callback:
(let old_paned_width = ref 2 in
let old_paned_height = ref 2 in
(fun {Gtk.width=paned_width;Gtk.height=paned_height} ->
if !old_paned_width <> paned_width || !old_paned_height <> paned_height then (
eval_paned#set_position (eval_paned#position * paned_width / !old_paned_width);
state_paned#set_position (state_paned#position * paned_height / !old_paned_height);
old_paned_width := paned_width;
old_paned_height := paned_height;
)))
in
session_box#pack s.finder#coerce;
session_paned#pack2 ~shrink:false ~resize:false (s.command#frame#coerce);
script_scroll#add s.script#coerce;
proof_scroll#add s.proof_view#coerce;
message_scroll#add s.message_view#coerce;
session_tab#pack s.tab_label#coerce;
img#set_stock `YES;
eval_paned#set_position 1;
state_paned#set_position 1;
(Some session_tab#coerce,None,session_paned#coerce)
let session_notebook =
Wg_Notebook.create build_session kill_session
~border_width:2 ~show_border:false ~scrollable:true ()
let cb = GData.clipboard Gdk.Atom.primary
let update_notebook_pos () =
let pos =
match current.vertical_tabs, current.opposite_tabs with
| false, false -> `TOP
| false, true -> `BOTTOM
| true , false -> `LEFT
| true , true -> `RIGHT
in
session_notebook#set_tab_pos pos
(** * Coqide's handling of signals *)
(** We ignore Ctrl-C, and for most of the other catchable signals
we launch an emergency save of opened files and then exit *)
let signals_to_crash = [Sys.sigabrt; Sys.sigalrm; Sys.sigfpe; Sys.sighup;
Sys.sigill; Sys.sigpipe; Sys.sigquit;
(* Sys.sigsegv; Sys.sigterm;*) Sys.sigusr2]
let crash_save i =
(* ignore (Unix.sigprocmask Unix.SIG_BLOCK signals_to_crash);*)
Minilib.log "Trying to save all buffers in .crashcoqide files";
let count = ref 0 in
List.iter
(function {script=view; analyzed_view = av } ->
(let filename = match av#filename with
| None ->
incr count;
"Unnamed_coqscript_"^(string_of_int !count)^".crashcoqide"
| Some f -> f^".crashcoqide"
in
try
if try_export filename (view#buffer#get_text ()) then
Minilib.log ("Saved "^filename)
else Minilib.log ("Could not save "^filename)
with _ -> Minilib.log ("Could not save "^filename))
)
session_notebook#pages;
Minilib.log "Done. Please report.";
if i <> 127 then exit i
let ignore_break () =
List.iter
(fun i ->
try Sys.set_signal i (Sys.Signal_handle crash_save)
with _ -> Minilib.log "Signal ignored (normal if Win32)")
signals_to_crash;
Sys.set_signal Sys.sigint Sys.Signal_ignore
exception Unsuccessful
let force_reset_initial () =
Minilib.log "Reset Initial";
let term = session_notebook#current_term in
Coq.reset_coqtop term.toplvl term.analyzed_view#requested_reset_initial
let break () =
Minilib.log "User break received";
Coq.break_coqtop session_notebook#current_term.toplvl
let do_if_not_computing term text f =
let threaded_task () =
let info () = Minilib.log ("Discarded query:" ^ text) in
try Coq.try_grab term.toplvl f info
with
| e ->
let msg = "Unknown error, please report:\n" ^ (Printexc.to_string e) in
term.analyzed_view#set_message msg
in
Minilib.log ("Launching thread " ^ text);
ignore (Thread.create threaded_task ())
let warning msg =
GToolbox.message_box ~title:"Warning"
~icon:(let img = GMisc.image () in
img#set_stock `DIALOG_WARNING;
img#set_icon_size `DIALOG;
img#coerce)
msg
let remove_current_view_page () =
let do_remove () =
let c = session_notebook#current_page in
session_notebook#remove_page c
in
let current = session_notebook#current_term in
if not current.script#buffer#modified then do_remove ()
else
match GToolbox.question_box ~title:"Close"
~buttons:["Save Buffer and Close";
"Close without Saving";
"Don't Close"]
~default:0
~icon:(let img = GMisc.image () in
img#set_stock `DIALOG_WARNING;
img#set_icon_size `DIALOG;
img#coerce)
"This buffer has unsaved modifications"
with
| 1 ->
begin match current.analyzed_view#filename with
| None ->
begin match select_file_for_save ~title:"Save file" () with
| None -> ()
| Some f ->
if current.analyzed_view#save_as f then begin
flash_info ("File " ^ f ^ " saved") ;
do_remove ()
end else
warning ("Save Failed (check if " ^ f ^ " is writable)")
end
| Some f ->
if current.analyzed_view#save f then begin
flash_info ("File " ^ f ^ " saved") ;
do_remove ()
end else
warning ("Save Failed (check if " ^ f ^ " is writable)")
end
| 2 -> do_remove ()
| _ -> ()
module Opt = Coq.PrintOpt
let print_items = [
([Opt.implicit],"Display implicit arguments","Display _implicit arguments",
"i",false);
([Opt.coercions],"Display coercions","Display _coercions","c",false);
([Opt.raw_matching],"Display raw matching expressions",
"Display raw _matching expressions","m",true);
([Opt.notations],"Display notations","Display _notations","n",true);
([Opt.all_basic],"Display all basic low-level contents",
"Display _all basic low-level contents","a",false);
([Opt.existential],"Display existential variable instances",
"Display _existential variable instances","e",false);
([Opt.universes],"Display universe levels","Display _universe levels",
"u",false);
([Opt.all_basic;Opt.existential;Opt.universes], "Display all low-level contents",
"Display all _low-level contents","l",false)
]
let setopts ct opts v =
let opts = List.map (fun o -> (o, v)) opts in
Coq.PrintOpt.set ct opts
let get_current_word () =
match session_notebook#current_term,cb#text with
| {script=script; analyzed_view=av;},None ->
Minilib.log "None selected";
let it = av#get_insert in
let start = find_word_start it in
let stop = find_word_end start in
script#buffer#move_mark `SEL_BOUND ~where:start;
script#buffer#move_mark `INSERT ~where:stop;
script#buffer#get_text ~slice:true ~start ~stop ()
| _,Some t ->
Minilib.log "Some selected";
Minilib.log t;
t
let input_channel b ic =
let buf = String.create 1024 and len = ref 0 in
while len := input ic buf 0 1024; !len > 0 do
Buffer.add_substring b buf 0 !len
done
let with_file handler name ~f =
try
let ic = open_in_gen [Open_rdonly;Open_creat] 0o644 name in
try f ic; close_in ic with e -> close_in ic; raise e
with Sys_error s -> handler s
(** Cut a part of the buffer in sentences and tag them.
May raise [Coq_lex.Unterminated] when the zone ends with
an unterminated sentence. *)
let split_slice_lax (buffer: GText.buffer) from upto =
buffer#remove_tag ~start:from ~stop:upto Tags.Script.comment_sentence;
buffer#remove_tag ~start:from ~stop:upto Tags.Script.sentence;
let slice = buffer#get_text ~start:from ~stop:upto () in
let rec split_substring str =
let off_conv = byte_offset_to_char_offset str in
let slice_len = String.length str in
let is_comment,end_off = Coq_lex.delimit_sentence str
in
let start = from#forward_chars (off_conv end_off) in
let stop = start#forward_char in
buffer#apply_tag ~start ~stop
(if is_comment then Tags.Script.comment_sentence else Tags.Script.sentence);
let next = end_off + 1 in
if next < slice_len then begin
ignore (from#nocopy#forward_chars (off_conv next));
split_substring (String.sub str next (slice_len - next))
end
in
split_substring slice
(** Searching forward and backward a position fulfilling some condition *)
let rec forward_search cond (iter:GText.iter) =
if iter#is_end || cond iter then iter
else forward_search cond iter#forward_char
let rec backward_search cond (iter:GText.iter) =
if iter#is_start || cond iter then iter
else backward_search cond iter#backward_char
let is_sentence_end s = s#has_tag Tags.Script.sentence || s#has_tag Tags.Script.comment_sentence
let is_char s c = s#char = Char.code c
(** Search backward the first character of a sentence, starting at [iter]
and going at most up to [soi] (meant to be the end of the locked zone).
Raise [Not_found] when no proper sentence start has been found,
in particular when the final "." of the locked zone is followed
by a non-blank character outside the locked zone. This non-blank
character will be signaled as erroneous in [tag_on_insert] below. *)
let grab_sentence_start (iter:GText.iter) soi =
let cond iter =
if iter#compare soi < 0 then raise Not_found;
let prev = iter#backward_char in
is_sentence_end prev &&
(not (is_char prev '.') ||
List.exists (is_char iter) [' ';'\n';'\r';'\t'])
in
backward_search cond iter
(** Search forward the first character immediately after a sentence end *)
let rec grab_sentence_stop (start:GText.iter) =
(forward_search is_sentence_end start)#forward_char
(** Search forward the first character immediately after a "." sentence end
(and not just a "{" or "}" or comment end *)
let rec grab_ending_dot (start:GText.iter) =
let is_ending_dot s = is_sentence_end s && s#char = Char.code '.' in
(forward_search is_ending_dot start)#forward_char
(** Retag a zone that has been edited *)
let tag_on_insert buffer =
try
(* the start of the non-locked zone *)
let soi = buffer#get_iter_at_mark (`NAME "start_of_input") in
(* the inserted zone is between [prev_insert] and [insert] *)
let insert = buffer#get_iter_at_mark `INSERT in
let prev_insert = buffer#get_iter_at_mark (`NAME "prev_insert") in
(* [prev_insert] is normally always before [insert] even when deleting.
Let's check this nonetheless *)
let prev_insert =
if insert#compare prev_insert < 0 then insert else prev_insert
in
let start = grab_sentence_start prev_insert soi in
(** The status of "{" "}" as sentence delimiters is too fragile.
We retag up to the next "." instead. *)
let stop = grab_ending_dot insert in
try split_slice_lax buffer start stop
with Coq_lex.Unterminated ->
try split_slice_lax buffer start buffer#end_iter
with Coq_lex.Unterminated -> ()
with Not_found ->
(* This is raised by [grab_sentence_start] *)
let err_pos = buffer#get_iter_at_mark (`NAME "start_of_input") in
buffer#apply_tag Tags.Script.error ~start:err_pos ~stop:err_pos#forward_char
let force_retag buffer =
try split_slice_lax buffer buffer#start_iter buffer#end_iter
with Coq_lex.Unterminated -> ()
(* GtkSource view should handle that one day !!!
let toggle_proof_visibility (buffer:GText.buffer) (cursor:GText.iter) =
(* move back twice if not into proof_decl,
* once if into proof_decl and back_char into_proof_decl,
* don't move if into proof_decl and back_char not into proof_decl *)
if not (cursor#has_tag Tags.Script.proof_decl) then
ignore (cursor#nocopy#backward_to_tag_toggle (Some Tags.Script.proof_decl));
if cursor#backward_char#has_tag Tags.Script.proof_decl then
ignore (cursor#nocopy#backward_to_tag_toggle (Some Tags.Script.proof_decl));
let decl_start = cursor in
let prf_end = decl_start#forward_to_tag_toggle (Some Tags.Script.qed) in
let decl_end = grab_ending_dot decl_start in
let prf_end = grab_ending_dot prf_end in
let prf_end = prf_end#forward_char in
if decl_start#has_tag Tags.Script.folded then (
buffer#remove_tag ~start:decl_start ~stop:decl_end Tags.Script.folded;
buffer#remove_tag ~start:decl_end ~stop:prf_end Tags.Script.hidden)
else (
buffer#apply_tag ~start:decl_start ~stop:decl_end Tags.Script.folded;
buffer#apply_tag ~start:decl_end ~stop:prf_end Tags.Script.hidden)
*)
(** The arguments that will be passed to coqtop. No quoting here, since
no /bin/sh when using create_process instead of open_process. *)
let custom_project_files = ref []
let sup_args = ref []
class analyzed_view (_script:Wg_ScriptView.script_view)
(_pv:Wg_ProofView.proof_view) (_mv:Wg_MessageView.message_view) _ct _fn =
object(self)
val input_view = _script
val input_buffer = _script#source_buffer
val proof_view = _pv
val message_view = _mv
val cmd_stack = Stack.create ()
val mycoqtop = _ct
val mutable filename = _fn
val mutable stats = None
val mutable last_modification_time = 0.
val mutable last_auto_save_time = 0.
val hidden_proofs = Hashtbl.create 32
method filename = filename
method stats = stats
method update_stats =
match filename with
| Some f -> stats <- my_stat f
| _ -> ()
method revert =
match filename with
| Some f -> begin
let do_revert () = begin
push_info "Reverting buffer";
try
Coq.reset_coqtop mycoqtop self#requested_reset_initial;
let b = Buffer.create 1024 in
with_file flash_info f ~f:(input_channel b);
let s = try_convert (Buffer.contents b) in
input_buffer#set_text s;
self#update_stats;
input_buffer#place_cursor ~where:input_buffer#start_iter;
input_buffer#set_modified false;
pop_info ();
flash_info "Buffer reverted";
force_retag (input_buffer :> GText.buffer);
with _ ->
pop_info ();
flash_info "Warning: could not revert buffer";
end
in
if input_buffer#modified then
match (GToolbox.question_box
~title:"Modified buffer changed on disk"
~buttons:["Revert from File";
"Overwrite File";
"Disable Auto Revert"]
~default:0
~icon:(stock_to_widget `DIALOG_WARNING)
"Some unsaved buffers changed on disk"
)
with 1 -> do_revert ()
| 2 -> if self#save f then flash_info "Overwritten" else
flash_info "Could not overwrite file"
| _ ->
Minilib.log "Auto revert set to false";
current.global_auto_revert <- false;
disconnect_revert_timer ()
else do_revert ()
end
| None -> ()
method save f =
if try_export f (input_buffer#get_text ()) then begin
filename <- Some f;
input_buffer#set_modified false;
stats <- my_stat f;
(match self#auto_save_name with
| None -> ()
| Some fn -> try Sys.remove fn with _ -> ());
true
end
else false
method private auto_save_name =
match filename with
| None -> None
| Some f ->
let dir = Filename.dirname f in
let base = (fst current.auto_save_name) ^
(Filename.basename f) ^
(snd current.auto_save_name)
in Some (Filename.concat dir base)
method private need_auto_save =
input_buffer#modified &&
last_modification_time > last_auto_save_time
method auto_save =
if self#need_auto_save then begin
match self#auto_save_name with
| None -> ()
| Some fn ->
try
last_auto_save_time <- Unix.time();
Minilib.log ("Autosave time: "^(string_of_float (Unix.time())));
if try_export fn (input_buffer#get_text ()) then begin
flash_info ~delay:1000 "Autosaved"
end
else warning
("Autosave failed (check if " ^ fn ^ " is writable)")
with _ ->
warning ("Autosave: unexpected error while writing "^fn)
end
method save_as f =
if Sys.file_exists f then
match (GToolbox.question_box ~title:"File exists on disk"
~buttons:["Overwrite";
"Cancel";]
~default:1
~icon:
(let img = GMisc.image () in
img#set_stock `DIALOG_WARNING;
img#set_icon_size `DIALOG;
img#coerce)
("File "^f^" already exists")
)
with 1 -> self#save f
| _ -> false
else self#save f
method insert_message s =
message_view#push Interface.Notice s
method set_message s =
message_view#clear ();
message_view#push Interface.Notice s
method private push_message level content =
message_view#push level content
method get_start_of_input = input_buffer#get_iter_at_mark (`NAME "start_of_input")
method get_insert = get_insert input_buffer
method recenter_insert =
(* BUG : to investigate further:
FIXED : Never call GMain.* in thread !
PLUS : GTK BUG ??? Cannot be called from a thread...
ADDITION: using sync instead of async causes deadlock...*)
ignore (GtkThread.async (
input_view#scroll_to_mark
~use_align:false
~yalign:0.75
~within_margin:0.25)
`INSERT)
method go_to_next_occ_of_cur_word =
let cv = session_notebook#current_term in
let av = cv.analyzed_view in
let b = (cv.script)#buffer in
let start = find_word_start (av#get_insert) in
let stop = find_word_end start in
let text = b#get_text ~start ~stop () in
match stop#forward_search text with
| None -> ()
| Some(start, _) ->
(b#place_cursor start;
self#recenter_insert)
method go_to_prev_occ_of_cur_word =
let cv = session_notebook#current_term in
let av = cv.analyzed_view in
let b = (cv.script)#buffer in
let start = find_word_start (av#get_insert) in
let stop = find_word_end start in
let text = b#get_text ~start ~stop () in
match start#backward_search text with
| None -> ()
| Some(start, _) ->
(b#place_cursor start;
self#recenter_insert)
method show_goals handle =
Coq.PrintOpt.set_printing_width proof_view#width;
match Coq.goals handle with
| Interface.Fail (l, str) ->
self#set_message ("Error in coqtop:\n"^str)
| Interface.Good goals | Interface.Unsafe goals ->
begin match Coq.evars handle with
| Interface.Fail (l, str)->
self#set_message ("Error in coqtop:\n"^str)
| Interface.Good evs | Interface.Unsafe evs ->
proof_view#set_goals goals;
proof_view#set_evars evs;
proof_view#refresh ()
end
(* This method is intended to perform stateless commands *)
method raw_coq_query handle phrase =
let () = Minilib.log "raw_coq_query starting now" in
let display_error s =
if not (Glib.Utf8.validate s) then
flash_info "This error is so nasty that I can't even display it."
else self#insert_message s;
in
match Coq.interp handle self#push_message ~raw:true ~verbose:false phrase with
| Interface.Fail (_, err) -> sync display_error err
| Interface.Good msg | Interface.Unsafe msg -> sync self#insert_message msg
method private find_phrase_starting_at (start:GText.iter) =
try
let start = grab_sentence_start start self#get_start_of_input in
let stop = grab_sentence_stop start in
(* Is this phrase non-empty and complete ? *)
if stop#compare start > 0 && is_sentence_end stop#backward_char
then Some (start,stop)
else None
with Not_found -> None
(** [fill_command_queue until q] fills a command queue until the [until]
condition returns true; it is fed with the number of phrases read and the
iters enclosing the current sentence. *)
method private fill_command_queue until queue =
let rec loop len iter =
let opt_sentence = self#find_phrase_starting_at iter in
match opt_sentence with
| None -> raise Exit
| Some (start, stop) ->
if until len start stop then raise Exit;
input_buffer#apply_tag Tags.Script.to_process ~start ~stop;
(* Check if this is a comment *)
let is_comment = stop#backward_char#has_tag Tags.Script.comment_sentence in
let flags = if is_comment then [`COMMENT] else [] in
let payload = {
start = `MARK (input_buffer#create_mark start);
stop = `MARK (input_buffer#create_mark stop);
flags = flags;
} in
Queue.push payload queue;
if not stop#is_end then loop (succ len) stop
in
try loop 0 self#get_start_of_input with Exit -> ()
method private process_command_queue ?(verbose = false) queue handle =
let error = ref None in
let info = ref [] in
let current_flags = ref [] in
let push_info level message = info := (level, message) :: !info in
(* First, process until error *)
Minilib.log "Begin command processing";
while not (Queue.is_empty queue) && !error = None do
let sentence = Queue.peek queue in
(* If the line is not a comment, we interpret it. *)
if not (List.mem `COMMENT sentence.flags) then begin
let start = input_buffer#get_iter_at_mark sentence.start in
let stop = input_buffer#get_iter_at_mark sentence.stop in
let phrase = start#get_slice ~stop in
match Coq.interp handle push_info ~verbose phrase with
| Interface.Fail (loc, msg) ->
error := Some (phrase, loc, msg);
| Interface.Good msg ->
push_info Interface.Notice msg;
current_flags := []
| Interface.Unsafe msg ->
current_flags := [`UNSAFE]
end;
(* If there is no error, then we mark it done *)
if !error = None then begin
(* We reget the iters here because Gtk is unable to warranty that they
were not modified meanwhile. Not really necessary but who knows... *)
let start = input_buffer#get_iter_at_mark sentence.start in
let stop = input_buffer#get_iter_at_mark sentence.stop in
let sentence = { sentence with
flags = !current_flags @ sentence.flags
} in
let tag =
if List.mem `UNSAFE !current_flags then Tags.Script.unjustified
else Tags.Script.processed
in
input_buffer#move_mark ~where:stop (`NAME "start_of_input");
input_buffer#apply_tag tag ~start ~stop;
input_buffer#remove_tag Tags.Script.to_process ~start ~stop;
(* Discard the old stack info and put it were it belongs *)
ignore (Queue.pop queue);
Stack.push sentence cmd_stack;
end;
done;
(* Then clear all irrelevant commands *)
while not (Queue.is_empty queue) do
let sentence = Queue.pop queue in
let start = input_buffer#get_iter_at_mark sentence.start in
let stop = input_buffer#get_iter_at_mark sentence.stop in
input_buffer#remove_tag Tags.Script.to_process ~start ~stop;
input_buffer#delete_mark sentence.start;
input_buffer#delete_mark sentence.stop;
done;
(* Return the list of info messages and the error *)
(List.rev !info, !error)
method private show_error phrase loc msg = match loc with
| None ->
message_view#clear ();
message_view#push Interface.Error msg
| Some (start, stop) ->
let soi = self#get_start_of_input in
let start = soi#forward_chars (byte_offset_to_char_offset phrase start) in
let stop = soi#forward_chars (byte_offset_to_char_offset phrase stop) in
input_buffer#apply_tag Tags.Script.error ~start ~stop;
input_buffer#place_cursor ~where:start;
message_view#clear ();
message_view#push Interface.Error msg
(** Compute the phrases until [until] returns [true]. *)
method private process_until until finish handle verbose =
let queue = Queue.create () in
(* Lock everything and fill the waiting queue *)
push_info "Coq is computing";
message_view#clear ();
input_view#set_editable false;
self#fill_command_queue until queue;
(* Now unlock and process asynchronously *)
input_view#set_editable true;
let (msg, error) = self#process_command_queue ~verbose queue handle in
pop_info ();
(* Display the goal and any error *)
self#show_goals handle;
match error with
| None ->
if verbose then
List.iter (fun (lvl, msg) -> self#push_message lvl msg) msg;
finish ();
self#recenter_insert
| Some (phrase, loc, msg) ->
self#show_error phrase loc msg
method process_next_phrase handle verbose =
let until len start stop = 1 <= len in
let finish () = input_buffer#place_cursor self#get_start_of_input in
self#process_until until finish handle verbose
method private process_until_iter handle iter =
let until len start stop =
if current.stop_before then stop#compare iter > 0
else start#compare iter >= 0
in
let finish () = () in
self#process_until until finish handle false
method process_until_end_or_error handle =
self#process_until_iter handle input_buffer#end_iter
(** Clear the command stack until [until] returns [true]. Returns the number
of commands sent to Coqtop to backtrack. *)
method private clear_command_stack until =
let rec loop len real_len =
if Stack.is_empty cmd_stack then real_len
else
let phrase = Stack.top cmd_stack in
let is_comment = List.mem `COMMENT phrase.flags in
let start = input_buffer#get_iter_at_mark phrase.start in
let stop = input_buffer#get_iter_at_mark phrase.stop in
if not (until len real_len start stop) then begin
(* [until] has not been reached, so we clear this command *)
ignore (Stack.pop cmd_stack);
input_buffer#remove_tag Tags.Script.processed ~start ~stop;
input_buffer#remove_tag Tags.Script.unjustified ~start ~stop;
input_buffer#move_mark ~where:start (`NAME "start_of_input");
input_buffer#delete_mark phrase.start;
input_buffer#delete_mark phrase.stop;
loop (succ len) (if is_comment then real_len else succ real_len)
end else
real_len
in
loop 0 0
(** Actually performs the undoing *)
method private undo_command_stack handle n =
match Coq.rewind handle n with
| Interface.Good n | Interface.Unsafe n ->
let until _ len _ _ = n <= len in
(* Coqtop requested [n] more ACTUAL backtrack *)
ignore (self#clear_command_stack until)
| Interface.Fail (l, str) ->
self#set_message
("Error while backtracking: " ^ str ^
"\nCoqIDE and coqtop may be out of sync, you may want to use Restart.")
(** Wrapper around the raw undo command *)
method private backtrack_until until finish handle =
push_info "Coq is undoing";
message_view#clear ();
(* Lock everything *)
input_view#set_editable false;
let to_undo = self#clear_command_stack until in
self#undo_command_stack handle to_undo;
input_view#set_editable true;
pop_info ();
finish ()
method private backtrack_to_iter handle iter =
let until _ _ _ stop = iter#compare stop >= 0 in
let finish () = () in
self#backtrack_until until finish handle;
(* We may have backtracked too much: let's replay *)
self#process_until_iter handle iter
method backtrack_last_phrase handle =
let until len _ _ _ = 1 <= len in
let finish () = input_buffer#place_cursor self#get_start_of_input in
self#backtrack_until until finish handle;
self#show_goals handle
method go_to_insert handle =
let point = self#get_insert in
if point#compare self#get_start_of_input >= 0
then self#process_until_iter handle point
else self#backtrack_to_iter handle point
method private send_to_coq handle phrase =
let display_error (loc, s) =
if not (Glib.Utf8.validate s) then
flash_info "This error is so nasty that I can't even display it."
else self#insert_message s
in
Minilib.log "Send_to_coq starting now";
match Coq.interp handle default_logger ~verbose:false phrase with
| Interface.Fail (l, str) -> sync display_error (l, str); None
| Interface.Good msg -> sync self#insert_message msg; Some []
| Interface.Unsafe msg -> sync self#insert_message msg; Some [`UNSAFE]
method private insert_this_phrase_on_success handle coqphrase insertphrase =
let mark_processed flags =
let stop = self#get_start_of_input in
if stop#starts_line then
input_buffer#insert ~iter:stop insertphrase
else input_buffer#insert ~iter:stop ("\n"^insertphrase);
tag_on_insert (input_buffer :> GText.buffer);
let start = self#get_start_of_input in
input_buffer#move_mark ~where:stop (`NAME "start_of_input");
let tag =
if List.mem `UNSAFE flags then Tags.Script.unjustified
else Tags.Script.processed
in
input_buffer#apply_tag tag ~start ~stop;
if self#get_insert#compare stop <= 0 then
input_buffer#place_cursor ~where:stop;
let ide_payload = {
start = `MARK (input_buffer#create_mark start);
stop = `MARK (input_buffer#create_mark stop);
flags = [];
} in
Stack.push ide_payload cmd_stack;
self#show_goals handle;
in
match self#send_to_coq handle coqphrase with
| Some flags -> sync mark_processed flags; true
| None ->
sync (fun _ -> self#insert_message ("Unsuccessfully tried: "^coqphrase)) ();
false
method private generic_reset_initial handle =
let start = input_buffer#start_iter in
(* clear the stack *)
while not (Stack.is_empty cmd_stack) do
let phrase = Stack.pop cmd_stack in
input_buffer#delete_mark phrase.start;
input_buffer#delete_mark phrase.stop
done;
(* reset the buffer *)
input_buffer#move_mark ~where:start (`NAME "start_of_input");
input_buffer#remove_tag Tags.Script.processed start input_buffer#end_iter;
input_buffer#remove_tag Tags.Script.unjustified start input_buffer#end_iter;
input_buffer#remove_tag Tags.Script.to_process start input_buffer#end_iter;
tag_on_insert (input_buffer :> GText.buffer);
(* clear the views *)
message_view#clear ();
proof_view#clear ();
(* apply the initial commands to coq *)
self#include_file_dir_in_path handle;
method erroneous_reset_initial handle =
self#generic_reset_initial handle;
(* warn the user *)
warning "Coqtop died badly. Resetting."
method requested_reset_initial handle =
self#generic_reset_initial handle
method tactic_wizard handle l =
async message_view#clear ();
ignore
(List.exists
(fun p ->
self#insert_this_phrase_on_success handle
("progress "^p^".") (p^".")) l)
method private include_file_dir_in_path handle =
match filename with
| None -> ()
| Some f ->
let dir = Filename.dirname f in
match Coq.inloadpath handle dir with
| Interface.Fail (_,str) ->
self#set_message
("Could not determine lodpath, this might lead to problems:\n"^str)
| Interface.Good true | Interface.Unsafe true -> ()
| Interface.Good false | Interface.Unsafe false ->
let cmd = Printf.sprintf "Add LoadPath \"%s\". " dir in
match Coq.interp handle default_logger cmd with
| Interface.Fail (l,str) ->
self#set_message ("Couln't add loadpath:\n"^str)
| Interface.Good _ | Interface.Unsafe _ -> ()
method help_for_keyword () =
browse_keyword (self#insert_message) (get_current_word ())
(** NB: Events during text edition:
- [begin_user_action]
- [insert_text] (or [delete_range] when deleting)
- [changed]
- [end_user_action]
When pasting a text containing tags (e.g. the sentence terminators),
there is actually many [insert_text] and [changed]. For instance,
for "a. b.":
- [begin_user_action]
- [insert_text] (for "a")
- [changed]
- [insert_text] (for ".")
- [changed]
- [apply_tag] (for the tag of ".")
- [insert_text] (for " b")
- [changed]
- [insert_text] (for ".")
- [changed]
- [apply_tag] (for the tag of ".")
- [end_user_action]
Since these copy-pasted tags may interact badly with the retag mechanism,
we now don't monitor the "changed" event, but rather the "begin_user_action"
and "end_user_action". We begin by setting a mark at the initial cursor
point. At the end, the zone between the mark and the cursor is to be
untagged and then retagged. *)
initializer
ignore (input_buffer#connect#insert_text
~callback:(fun it s ->
if (it#compare self#get_start_of_input)<0
then GtkSignal.stop_emit ();
if String.length s > 1 then
(Minilib.log "insert_text: Placing cursor";input_buffer#place_cursor ~where:it)));
ignore (input_buffer#connect#after#apply_tag
~callback:(fun tag ~start ~stop ->
if (start#compare self#get_start_of_input)>=0
then
begin
input_buffer#remove_tag
Tags.Script.processed
~start
~stop;
input_buffer#remove_tag
Tags.Script.unjustified
~start
~stop
end
)
);
ignore (input_buffer#connect#begin_user_action
~callback:(fun () ->
let here = input_buffer#get_iter_at_mark `INSERT in
input_buffer#move_mark (`NAME "prev_insert") here
)
);
ignore (input_buffer#connect#end_user_action
~callback:(fun () ->
last_modification_time <- Unix.time ();
let r = input_view#visible_rect in