2
(************************************************************************)
3
(* v * The Coq Proof Assistant / The Coq Development Team *)
4
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
5
(* \VV/ **************************************************************)
6
(* // * This file is distributed under the terms of the *)
7
(* * GNU Lesser General Public License Version 2.1 *)
8
(************************************************************************)
10
(* $Id: coqide.ml 12104 2009-04-24 18:10:10Z notin $ *)
18
let cb () = ((Option.get !cb_):GData.clipboard)
19
let last_cb_content = ref ""
21
let (message_view:GText.view option ref) = ref None
22
let (proof_view:GText.view option ref) = ref None
24
let (_notebook:GPack.notebook option ref) = ref None
25
let notebook () = Option.get !_notebook
27
let update_notebook_pos () =
29
match !current.vertical_tabs, !current.opposite_tabs with
30
| false, false -> `TOP
31
| false, true -> `BOTTOM
32
| true , false -> `LEFT
33
| true , true -> `RIGHT
35
(notebook ())#set_tab_pos pos
37
(* Tabs contain the name of the edited file and 2 status informations:
38
Saved state + Focused proof buffer *)
40
let vbox = new GPack.box ((Gobject.try_cast w "GtkBox"):Gtk.box Gtk.obj) in
41
let l = vbox#children in
44
let img = new GMisc.image
45
((Gobject.try_cast img#as_widget "GtkImage"):
48
let lbl = GMisc.label_cast lbl in
52
let set_tab_label i n =
53
let nb = notebook () in
54
let _,_,lbl = decompose_tab (nb#get_tab_label(nb#get_nth_page i))#as_widget
56
lbl#set_use_markup true;
57
(* lbl#set_text n *) lbl#set_label n
60
let set_tab_image ~icon i =
61
let nb = notebook () in
62
let _,img,_ = decompose_tab (nb#get_tab_label(nb#get_nth_page i))#as_widget
64
img#set_icon_size `SMALL_TOOLBAR;
67
let set_current_tab_image ~icon = set_tab_image ~icon (notebook())#current_page
69
let set_current_tab_label n = set_tab_label (notebook())#current_page n
72
let nb = notebook () in
73
let _,_,lbl = decompose_tab (nb#get_tab_label(nb#get_nth_page i))#as_widget
77
let get_full_tab_label i =
78
let nb = notebook () in
79
let _,_,lbl = decompose_tab (nb#get_tab_label(nb#get_nth_page i))#as_widget
83
let get_current_tab_label () = get_tab_label (notebook())#current_page
85
let get_current_page () =
86
let i = (notebook())#current_page in
87
(notebook())#get_nth_page i
89
(* This function must remove "focused proof" decoration *)
90
let reset_tab_label i =
91
set_tab_label i (get_tab_label i)
93
let to_do_on_page_switch = ref []
95
module Vector = struct
96
exception Found of int
97
type 'a t = ('a option) array ref
98
let create () = ref [||]
99
let length t = Array.length !t
100
let get t i = Option.get (Array.get !t i)
101
let set t i v = Array.set !t i (Some v)
102
let remove t i = Array.set !t i None
103
let append t e = t := Array.append !t [|Some e|]; (Array.length !t)-1
104
let iter f t = Array.iter (function | None -> () | Some x -> f x) !t
105
let find_or_fail f t =
106
let test i = function | None -> () | Some e -> if f e then raise (Found i) in
110
let l = Array.length !t in
112
(i < l) && (((!t.(i) <> None) && f (Option.get !t.(i))) || test (i+1))
117
type 'a viewable_script =
118
{view : Undo.undoable_view;
119
mutable analyzed_view : 'a option;
123
class type analyzed_views=
125
val mutable act_id : GtkSignal.id option
126
val current_all : 'self viewable_script
127
val mutable deact_id : GtkSignal.id option
128
val input_buffer : GText.buffer
129
val input_view : Undo.undoable_view
130
val last_array : string array
131
val mutable last_index : bool
132
val message_buffer : GText.buffer
133
val message_view : GText.view
134
val proof_buffer : GText.buffer
135
val proof_view : GText.view
136
val mutable is_active : bool
137
val mutable read_only : bool
138
val mutable filename : string option
139
val mutable stats : Unix.stats option
140
val mutable detached_views : GWindow.window list
141
method without_auto_complete : 'a 'b. ('a -> 'b) -> 'a -> 'b
142
method set_auto_complete : bool -> unit
144
method kill_detached_views : unit -> unit
145
method add_detached_view : GWindow.window -> unit
146
method remove_detached_view : GWindow.window -> unit
148
method view : Undo.undoable_view
149
method filename : string option
150
method stats : Unix.stats option
151
method set_filename : string option -> unit
152
method update_stats : unit
154
method auto_save : unit
155
method save : string -> bool
156
method save_as : string -> bool
157
method read_only : bool
158
method set_read_only : bool -> unit
159
method is_active : bool
160
method activate : unit -> unit
161
method active_keypress_handler : GdkEvent.Key.t -> bool
162
method backtrack_to : GText.iter -> unit
163
method backtrack_to_no_lock : GText.iter -> unit
164
method clear_message : unit
165
method deactivate : unit -> unit
166
method disconnected_keypress_handler : GdkEvent.Key.t -> bool
167
method electric_handler : GtkSignal.id
168
method find_phrase_starting_at :
169
GText.iter -> (GText.iter * GText.iter) option
170
method get_insert : GText.iter
171
method get_start_of_input : GText.iter
172
method go_to_insert : unit
173
method indent_current_line : unit
174
method insert_command : string -> string -> unit
175
method tactic_wizard : string list -> unit
176
method insert_message : string -> unit
177
method insert_this_phrase_on_success :
178
bool -> bool -> bool -> string -> string -> bool
179
method process_next_phrase : bool -> bool -> bool -> bool
180
method process_until_iter_or_error : GText.iter -> unit
181
method process_until_end_or_error : unit
182
method recenter_insert : unit
183
method reset_initial : unit
185
bool -> bool -> string ->
186
bool -> bool -> bool ->
187
(bool*(reset_info*(Util.loc * Vernacexpr.vernac_expr))) option
188
method set_message : string -> unit
189
method show_pm_goal : unit
190
method show_goals : unit
191
method show_goals_full : unit
192
method undo_last_step : unit
193
method help_for_keyword : unit -> unit
194
method complete_at_offset : int -> bool
196
method blaster : unit -> unit
199
let (input_views:analyzed_views viewable_script Vector.t) = Vector.create ()
202
let signals_to_crash = [Sys.sigabrt; Sys.sigalrm; Sys.sigfpe; Sys.sighup;
203
Sys.sigill; Sys.sigpipe; Sys.sigquit;
204
(* Sys.sigsegv; Sys.sigterm;*) Sys.sigusr2]
207
(* ignore (Unix.sigprocmask Unix.SIG_BLOCK signals_to_crash);*)
208
Pervasives.prerr_endline "Trying to save all buffers in .crashcoqide files";
211
(function {view=view; analyzed_view = Some av } ->
212
(let filename = match av#filename with
215
"Unnamed_coqscript_"^(string_of_int !count)^".crashcoqide"
216
| Some f -> f^".crashcoqide"
219
if try_export filename (view#buffer#get_text ()) then
220
Pervasives.prerr_endline ("Saved "^filename)
221
else Pervasives.prerr_endline ("Could not save "^filename)
222
with _ -> Pervasives.prerr_endline ("Could not save "^filename))
223
| _ -> Pervasives.prerr_endline "Unanalyzed view found. Please report."
226
Pervasives.prerr_endline "Done. Please report.";
227
if i <> 127 then exit i
229
let ignore_break () =
232
try Sys.set_signal i (Sys.Signal_handle crash_save)
233
with _ -> prerr_endline "Signal ignored (normal if Win32)")
235
Sys.set_signal Sys.sigint Sys.Signal_ignore
237
(* Locking machinery for Coq kernel *)
238
let coq_computing = Mutex.create ()
240
(* To prevent Coq from interrupting during undoing...*)
241
let coq_may_stop = Mutex.create ()
244
prerr_endline "User break received:";
245
if not (Mutex.try_lock coq_computing) then
247
prerr_endline " trying to stop computation:";
248
if Mutex.try_lock coq_may_stop then begin
249
Util.interrupt := true;
250
prerr_endline " interrupt flag set. Computation should stop soon...";
251
Mutex.unlock coq_may_stop
252
end else prerr_endline " interruption refused (may not stop now)";
255
Mutex.unlock coq_computing;
256
prerr_endline " ignored (not computing)"
259
let do_if_not_computing text f x =
260
let threaded_task () =
261
if Mutex.try_lock coq_computing
264
let w = Blaster_window.blaster_window () in
265
if not (Mutex.try_lock w#lock) then
268
let lck = Mutex.create () in
270
prerr_endline "Waiting on blaster...";
271
Condition.wait w#blaster_killed lck;
272
prerr_endline "Waiting on blaster ok";
278
Glib.Timeout.add ~ms:300
279
~callback:(fun () -> async !pulse ();true) in
281
prerr_endline "Getting lock";
284
Glib.Timeout.remove idle;
285
prerr_endline "Releasing lock";
286
Mutex.unlock coq_computing;
288
Glib.Timeout.remove idle;
289
prerr_endline "Releasing lock (on error)";
290
Mutex.unlock coq_computing;
296
"Discarded order (computations are ongoing)"
298
prerr_endline ("Launching thread " ^ text);
299
ignore (Thread.create threaded_task ())
301
let add_input_view tv =
302
Vector.append input_views tv
304
let get_input_view i =
305
if 0 <= i && i < Vector.length input_views
307
Vector.get input_views i
310
let active_view = ref None
312
let get_active_view () = Vector.get input_views (Option.get !active_view)
314
let set_active_view i =
315
(match !active_view with None -> () | Some i ->
317
(notebook ())#goto_page i;
318
let txt = get_current_tab_label () in
319
set_current_tab_label ("<span background=\"light green\">"^txt^"</span>");
320
active_view := Some i
322
let set_current_view i = (notebook ())#goto_page i
324
let kill_input_view i =
325
let v = Vector.get input_views i in
326
(match v.analyzed_view with
327
| Some v -> v#kill_detached_views ()
330
v.analyzed_view <- None;
331
Vector.remove input_views i
333
let get_current_view_page () = (notebook ())#current_page
334
let get_current_view () = Vector.get input_views (notebook ())#current_page
335
let remove_current_view_page () =
336
let c = (notebook ())#current_page in
338
((notebook ())#get_nth_page c)#misc#hide ()
341
(* TODO: avoid num and prime at the head of a word *)
342
Glib.Unichar.isalnum c || c = underscore || c = prime
345
prerr_endline ("Starts word ? '"^(Glib.Utf8.from_unichar it#char)^"'");
346
(not it#copy#nocopy#backward_char ||
347
(let c = it#backward_char#char in
348
not (is_word_char c)))
351
(not it#copy#nocopy#forward_char ||
352
let c = it#forward_char#char in
358
not (starts_word it) &&
359
not (ends_word it) &&
362
let is_on_word_limit it = inside_word it || ends_word it
364
let rec find_word_start it =
365
prerr_endline "Find word start";
366
if not it#nocopy#backward_char then
367
(prerr_endline "find_word_start: cannot backward"; it)
368
else if is_word_char it#char
369
then find_word_start it
370
else (it#nocopy#forward_char;
371
prerr_endline ("Word start at: "^(string_of_int it#offset));it)
372
let find_word_start (it:GText.iter) = find_word_start it#copy
374
let rec find_word_end it =
375
prerr_endline "Find word end";
376
if let c = it#char in c<>0 && is_word_char c
378
ignore (it#nocopy#forward_char);
380
end else (prerr_endline ("Word end at: "^(string_of_int it#offset));it)
381
let find_word_end it = find_word_end it#copy
384
let get_word_around it =
385
let start = find_word_start it in
386
let stop = find_word_end it in
390
let rec complete_backward w (it:GText.iter) =
391
prerr_endline "Complete backward...";
392
match it#backward_search w with
393
| None -> (prerr_endline "backward_search failed";None)
394
| Some (start,stop) ->
395
prerr_endline ("complete_backward got a match:"^(string_of_int start#offset)^(string_of_int stop#offset));
396
if starts_word start then
397
let ne = find_word_end stop in
398
if ne#compare stop = 0
399
then complete_backward w start
400
else Some (start,stop,ne)
401
else complete_backward w start
403
let rec complete_forward w (it:GText.iter) =
404
prerr_endline "Complete forward...";
405
match it#forward_search w with
407
| Some (start,stop) ->
408
if starts_word start then
409
let ne = find_word_end stop in
410
if ne#compare stop = 0 then
411
complete_forward w stop
412
else Some (stop,stop,ne)
413
else complete_forward w stop
415
(* Reset this to None on page change ! *)
416
let (last_completion:(string*int*int*bool) option ref) = ref None
418
let () = to_do_on_page_switch :=
419
(fun i -> last_completion := None)::!to_do_on_page_switch
421
let rec complete input_buffer w (offset:int) =
422
match !last_completion with
423
| Some (lw,loffset,lpos,backward)
424
when lw=w && loffset=offset ->
426
let iter = input_buffer#get_iter (`OFFSET lpos) in
428
match complete_backward w iter with
433
(input_buffer#get_iter (`OFFSET loffset)))#offset ,
436
| Some (ss,start,stop) as result ->
438
Some (w,offset,ss#offset,true);
441
match complete_forward w iter with
443
last_completion := None;
445
| Some (ss,start,stop) as result ->
447
Some (w,offset,ss#offset,false);
451
match complete_backward w (input_buffer#get_iter (`OFFSET offset)) with
454
Some (w,offset,(find_word_end (input_buffer#get_iter
455
(`OFFSET offset)))#offset,false);
456
complete input_buffer w offset
457
| Some (ss,start,stop) as result ->
458
last_completion := Some (w,offset,ss#offset,true);
462
let get_current_word () =
463
let av = Option.get ((get_current_view ()).analyzed_view) in
464
match (cb ())#text with
466
prerr_endline "None selected";
467
let it = av#get_insert in
468
let start = find_word_start it in
469
let stop = find_word_end start in
470
av#view#buffer#move_mark `SEL_BOUND start;
471
av#view#buffer#move_mark `INSERT stop;
472
av#view#buffer#get_text ~slice:true ~start ~stop ()
474
prerr_endline "Some selected";
479
let input_channel b ic =
480
let buf = String.create 1024 and len = ref 0 in
481
while len := input ic buf 0 1024; !len > 0 do
482
Buffer.add_substring b buf 0 !len
485
let with_file handler name ~f =
487
let ic = open_in_gen [Open_rdonly;Open_creat] 0o644 name in
488
try f ic; close_in ic with e -> close_in ic; raise e
489
with Sys_error s -> handler s
491
type info = {start:GText.mark;
493
ast:Util.loc * Vernacexpr.vernac_expr;
494
reset_info:Coq.reset_info
497
exception Size of int
498
let (processed_stack:info Stack.t) = Stack.create ()
499
let push x = Stack.push x processed_stack
500
let pop () = try Stack.pop processed_stack with Stack.Empty -> raise (Size 0)
501
let top () = try Stack.top processed_stack with Stack.Empty -> raise (Size 0)
502
let is_empty () = Stack.is_empty processed_stack
504
(* push a new Coq phrase *)
506
let update_on_end_of_segment id =
507
let lookup_section = function
508
| { reset_info = ResetAtSegmentStart id',_,_ } when id = id' -> raise Exit
509
| { reset_info = _,_,r } -> r := false
511
try Stack.iter lookup_section processed_stack with Exit -> ()
513
let push_phrase reset_info start_of_phrase_mark end_of_phrase_mark ast =
514
let x = {start = start_of_phrase_mark;
515
stop = end_of_phrase_mark;
517
reset_info = reset_info
521
| VernacEndSegment (_,id) ->
522
prerr_endline "Updating on end of segment 1";
523
update_on_end_of_segment id
529
let repush_phrase reset_info x =
530
let x = { x with reset_info = reset_info } in
533
| VernacEndSegment (_,id) ->
534
prerr_endline "Updating on end of segment 2";
535
update_on_end_of_segment id
541
| BacktrackToNextActiveMark
542
| BacktrackToMark of reset_mark
543
| BacktrackToModSec of Names.identifier
546
let add_undo = function (n,a,b,p,l as x) -> if p = 0 then (n+1,a,b,p,l) else x
547
let add_abort = function
548
| (n,a,b,0,l) -> (0,a+1,b,0,l)
549
| (n,a,b,p,l) -> (n,a,b,p-1,l)
550
let add_qed q (n,a,b,p,l as x) =
551
if q = 0 then x else (n,a,BacktrackToNextActiveMark,p+q,l)
552
let add_backtrack (n,a,b,p,l) b' = (n,a,b',p,l)
554
let update_proofs (n,a,b,p,cur_lems) prev_lems =
555
let ncommon = List.length (Util.list_intersect cur_lems prev_lems) in
556
let openproofs = List.length cur_lems - ncommon in
557
let closedproofs = List.length prev_lems - ncommon in
558
let undos = (n,a,b,p,prev_lems) in
559
add_qed closedproofs (Util.iterate add_abort openproofs undos)
561
let pop_command undos t =
562
let (state_info,undo_info,section_info) = t.reset_info in
564
if !section_info then
565
let undos = update_proofs undos undo_info in
566
match state_info with
567
| _ when is_vernac_tactic_command (snd t.ast) ->
568
(* A tactic, active if not below a Qed *)
570
| ResetAtRegisteredObject mark ->
571
add_backtrack undos (BacktrackToMark mark)
572
| ResetAtSegmentStart id ->
573
add_backtrack undos (BacktrackToModSec id)
574
| _ when is_vernac_state_preserving_command (snd t.ast) ->
577
add_backtrack undos BacktrackToNextActiveMark
580
prerr_endline "In section";
581
(* An object inside a closed section *)
582
add_backtrack undos BacktrackToNextActiveMark
588
if a <> 0 then prerr_endline ("Applying "^string_of_int a^" aborts");
589
try Util.repeat a Pfedit.delete_current_proof ()
590
with e -> prerr_endline "WARNING : found a closed environment"; raise e
592
exception UndoStackExhausted
594
let apply_tactic_undo n =
596
(prerr_endline ("Applying "^string_of_int n^" undos");
597
try Pfedit.undo n with _ -> raise UndoStackExhausted)
599
let apply_reset = function
600
| BacktrackToMark mark -> reset_to mark
601
| BacktrackToModSec id -> reset_to_mod id
603
| BacktrackToNextActiveMark -> assert false
605
let rec apply_undos (n,a,b,p,l as undos) =
606
if p = 0 & b <> BacktrackToNextActiveMark then
612
with UndoStackExhausted ->
613
apply_undos (n,0,BacktrackToNextActiveMark,p,l)
616
(* re-synchronize Coq to the current state of the stack *)
622
apply_undos (pop_command undos t);
623
let reset_info = Coq.compute_reset_info (snd t.ast) in
625
repush_phrase reset_info t
628
(* For electric handlers *)
631
(* For find_phrase_starting_at *)
632
exception Stop of int
634
let activate_input i =
635
(match !active_view with
638
let a_v = Option.get (Vector.get input_views n).analyzed_view in
642
let activate_function = (Option.get (Vector.get input_views i).analyzed_view)#activate in
643
activate_function ();
647
GToolbox.message_box ~title:"Warning"
648
~icon:(let img = GMisc.image () in
649
img#set_stock `DIALOG_WARNING;
650
img#set_icon_size `DIALOG;
655
class analyzed_view index =
656
let {view = input_view_} as current_all_ = get_input_view index in
657
let proof_view_ = Option.get !proof_view in
658
let message_view_ = Option.get !message_view in
660
val current_all = current_all_
661
val input_view = current_all_.view
662
val proof_view = Option.get !proof_view
663
val message_view = Option.get !message_view
664
val input_buffer = input_view_#buffer
665
val proof_buffer = proof_view_#buffer
666
val message_buffer = message_view_#buffer
667
val mutable is_active = false
668
val mutable read_only = false
669
val mutable filename = None
670
val mutable stats = None
671
val mutable last_modification_time = 0.
672
val mutable last_auto_save_time = 0.
673
val mutable detached_views = []
675
val mutable auto_complete_on = !current.auto_complete
677
method private toggle_auto_complete =
678
auto_complete_on <- not auto_complete_on
679
method set_auto_complete t = auto_complete_on <- t
680
method without_auto_complete : 'a 'b. ('a -> 'b) -> 'a -> 'b = fun f x ->
681
let old = auto_complete_on in
682
self#set_auto_complete false;
684
self#set_auto_complete old;
686
method add_detached_view (w:GWindow.window) =
687
detached_views <- w::detached_views
688
method remove_detached_view (w:GWindow.window) =
689
detached_views <- List.filter (fun e -> w#misc#get_oid<>e#misc#get_oid) detached_views
691
method kill_detached_views () =
692
List.iter (fun w -> w#destroy ()) detached_views;
695
method view = input_view
696
method filename = filename
698
method set_filename f =
701
| Some f -> stats <- my_stat f
704
method update_stats =
706
| Some f -> stats <- my_stat f
712
let do_revert () = begin
713
!push_info "Reverting buffer";
715
if is_active then self#reset_initial;
716
let b = Buffer.create 1024 in
717
with_file !flash_info f ~f:(input_channel b);
718
let s = try_convert (Buffer.contents b) in
719
input_buffer#set_text s;
721
input_buffer#place_cursor input_buffer#start_iter;
722
input_buffer#set_modified false;
724
!flash_info "Buffer reverted";
725
Highlight.highlight_all input_buffer;
728
!flash_info "Warning: could not revert buffer";
731
if input_buffer#modified then
732
match (GToolbox.question_box
733
~title:"Modified buffer changed on disk"
734
~buttons:["Revert from File";
736
"Disable Auto Revert"]
738
~icon:(stock_to_widget `DIALOG_WARNING)
739
"Some unsaved buffers changed on disk"
741
with 1 -> do_revert ()
742
| 2 -> if self#save f then !flash_info "Overwritten" else
743
!flash_info "Could not overwrite file"
745
prerr_endline "Auto revert set to false";
746
!current.global_auto_revert <- false;
747
disconnect_revert_timer ()
753
if try_export f (input_buffer#get_text ()) then begin
755
input_buffer#set_modified false;
757
(match self#auto_save_name with
759
| Some fn -> try Sys.remove fn with _ -> ());
764
method private auto_save_name =
768
let dir = Filename.dirname f in
769
let base = (fst !current.auto_save_name) ^
770
(Filename.basename f) ^
771
(snd !current.auto_save_name)
772
in Some (Filename.concat dir base)
774
method private need_auto_save =
775
input_buffer#modified &&
776
last_modification_time > last_auto_save_time
779
if self#need_auto_save then begin
780
match self#auto_save_name with
784
last_auto_save_time <- Unix.time();
785
prerr_endline ("Autosave time : "^(string_of_float (Unix.time())));
786
if try_export fn (input_buffer#get_text ()) then begin
787
!flash_info ~delay:1000 "Autosaved"
790
("Autosave failed (check if " ^ fn ^ " is writable)")
792
warning ("Autosave: unexpected error while writing "^fn)
796
if Sys.file_exists f then
797
match (GToolbox.question_box ~title:"File exists on disk"
798
~buttons:["Overwrite";
802
(let img = GMisc.image () in
803
img#set_stock `DIALOG_WARNING;
804
img#set_icon_size `DIALOG;
806
("File "^f^"already exists")
808
with 1 -> self#save f
812
method set_read_only b = read_only<-b
813
method read_only = read_only
814
method is_active = is_active
815
method insert_message s =
816
message_buffer#insert s;
817
message_view#misc#draw None
819
method set_message s =
820
message_buffer#set_text s;
821
message_view#misc#draw None
823
method clear_message = message_buffer#set_text ""
824
val mutable last_index = true
825
val last_array = [|"";""|]
826
method get_start_of_input = input_buffer#get_iter_at_mark (`NAME "start_of_input")
828
method get_insert = get_insert input_buffer
830
method recenter_insert =
831
(* BUG : to investigate further:
832
FIXED : Never call GMain.* in thread !
833
PLUS : GTK BUG ??? Cannot be called from a thread...
834
ADDITION: using sync instead of async causes deadlock...*)
835
ignore (GtkThread.async (
836
input_view#scroll_to_mark
843
method indent_current_line =
844
let get_nb_space it =
846
let nb_sep = ref 0 in
847
let continue = ref true in
849
if it#char = space then begin
851
if not it#nocopy#forward_char then continue := false;
852
end else continue := false
856
let previous_line = self#get_insert in
857
if previous_line#nocopy#backward_line then begin
858
let previous_line_spaces = get_nb_space previous_line in
859
let current_line_start = self#get_insert#set_line_offset 0 in
860
let current_line_spaces = get_nb_space current_line_start in
861
if input_buffer#delete_interactive
862
~start:current_line_start
863
~stop:(current_line_start#forward_chars current_line_spaces)
866
let current_line_start = self#get_insert#set_line_offset 0 in
868
~iter:current_line_start
869
(String.make previous_line_spaces ' ')
872
method show_pm_goal =
874
(Printf.sprintf " *** Declarative Mode ***\n");
876
let (hyps,concl) = get_current_pm_goal () in
878
(fun ((_,_,_,(s,_)) as _hyp) ->
879
proof_buffer#insert (s^"\n"))
882
(String.make 38 '_' ^ "\n");
883
let (_,_,_,s) = concl in
884
proof_buffer#insert ("thesis := \n "^s^"\n");
885
let my_mark = `NAME "end_of_conclusion" in
886
proof_buffer#move_mark
887
~where:((proof_buffer#get_iter_at_mark `INSERT))
889
ignore (proof_view#scroll_to_mark my_mark)
891
match Decl_mode.get_end_command (Pfedit.get_pftreestate ()) with
894
("Subproof completed, now type "^endc^".")
896
proof_buffer#insert "Proof completed."
900
proof_view#buffer#set_text "";
901
match Decl_mode.get_current_mode () with
902
Decl_mode.Mode_none -> proof_buffer#insert (Coq.print_no_goal ())
903
| Decl_mode.Mode_tactic ->
905
let s = Coq.get_current_goals () in
907
| [] -> proof_buffer#insert (Coq.print_no_goal ())
909
let goal_nb = List.length s in
911
(Printf.sprintf "%d subgoal%s\n"
913
(if goal_nb<=1 then "" else "s"));
915
(fun ((_,_,_,(s,_)) as _hyp) ->
916
proof_buffer#insert (s^"\n"))
919
(String.make 38 '_' ^ "(1/"^
920
(string_of_int goal_nb)^
922
let _,_,_,sconcl = concl in
923
proof_buffer#insert sconcl;
924
proof_buffer#insert "\n";
925
let my_mark = `NAME "end_of_conclusion" in
926
proof_buffer#move_mark
927
~where:((proof_buffer#get_iter_at_mark `INSERT))
929
proof_buffer#insert "\n\n";
932
(function (_,(_,_,_,concl)) ->
935
(String.make 38 '_' ^"("^
938
(string_of_int goal_nb)^
940
proof_buffer#insert concl;
941
proof_buffer#insert "\n\n";
944
ignore (proof_view#scroll_to_mark my_mark)
946
| Decl_mode.Mode_proof ->
949
prerr_endline ("Don't worry be happy despite: "^Printexc.to_string e)
952
val mutable full_goal_done = true
954
method show_goals_full =
955
if not full_goal_done then
958
proof_view#buffer#set_text "";
959
match Decl_mode.get_current_mode () with
960
Decl_mode.Mode_none ->
961
proof_buffer#insert (Coq.print_no_goal ())
962
| Decl_mode.Mode_tactic ->
964
match Coq.get_current_goals () with
965
[] -> Util.anomaly "show_goals_full"
966
| ((hyps,concl)::r) as s ->
967
let last_shown_area =
968
proof_buffer#create_tag [`BACKGROUND "light green"]
970
let goal_nb = List.length s in
971
proof_buffer#insert (Printf.sprintf "%d subgoal%s\n"
973
(if goal_nb<=1 then "" else "s"));
974
let coq_menu commands =
975
let tag = proof_buffer#create_tag []
978
(tag#connect#event ~callback:
979
(fun ~origin ev it ->
980
begin match GdkEvent.get_type ev with
982
let ev = (GdkEvent.Button.cast ev) in
983
if (GdkEvent.Button.button ev) = 3
985
let loc_menu = GMenu.menu () in
987
new GMenu.factory loc_menu in
988
let add_coq_command (cp,ip) =
993
(self#insert_this_phrase_on_success
997
("progress "^ip^"\n")
1002
List.iter add_coq_command commands;
1005
~time:(GdkEvent.Button.time ev);
1008
proof_buffer#remove_tag
1009
~start:proof_buffer#start_iter
1010
~stop:proof_buffer#end_iter
1012
prerr_endline "Before find_tag_limits";
1014
let s,e = find_tag_limits tag
1017
prerr_endline "After find_tag_limits";
1018
proof_buffer#apply_tag
1023
prerr_endline "Applied tag";
1032
(fun ((_,_,_,(s,_)) as hyp) ->
1033
let tag = coq_menu (hyp_menu hyp) in
1034
proof_buffer#insert ~tags:[tag] (s^"\n"))
1037
(String.make 38 '_' ^"(1/"^
1038
(string_of_int goal_nb)^
1041
let tag = coq_menu (concl_menu concl) in
1042
let _,_,_,sconcl = concl in
1043
proof_buffer#insert ~tags:[tag] sconcl;
1044
proof_buffer#insert "\n";
1045
let my_mark = `NAME "end_of_conclusion" in
1046
proof_buffer#move_mark
1047
~where:((proof_buffer#get_iter_at_mark `INSERT)) my_mark;
1048
proof_buffer#insert "\n\n";
1051
(function (_,(_,_,_,concl)) ->
1054
(String.make 38 '_' ^"("^
1057
(string_of_int goal_nb)^
1059
proof_buffer#insert concl;
1060
proof_buffer#insert "\n\n";
1063
ignore (proof_view#scroll_to_mark my_mark) ;
1064
full_goal_done <- true
1066
| Decl_mode.Mode_proof ->
1068
with e -> prerr_endline (Printexc.to_string e)
1071
method send_to_coq verbosely replace phrase show_output show_error localize =
1072
let display_output msg =
1073
self#insert_message (if show_output then msg else "") in
1074
let display_error e =
1075
let (s,loc) = Coq.process_exn e in
1076
assert (Glib.Utf8.validate s);
1077
self#insert_message s;
1078
message_view#misc#draw None;
1080
(match Option.map Util.unloc loc with
1082
| Some (start,stop) ->
1083
let convert_pos = byte_offset_to_char_offset phrase in
1084
let start = convert_pos start in
1085
let stop = convert_pos stop in
1086
let i = self#get_start_of_input in
1087
let starti = i#forward_chars start in
1088
let stopi = i#forward_chars stop in
1089
input_buffer#apply_tag_by_name "error"
1092
input_buffer#place_cursor starti) in
1094
full_goal_done <- false;
1095
prerr_endline "Send_to_coq starting now";
1096
Decl_mode.clear_daimon_flag ();
1097
if replace then begin
1098
let r,info = Coq.interp_and_replace ("info " ^ phrase) in
1099
let complete = not (Decl_mode.get_daimon_flag ()) in
1100
let msg = read_stdout () in
1101
sync display_output msg;
1104
let r = Coq.interp verbosely phrase in
1105
let complete = not (Decl_mode.get_daimon_flag ()) in
1106
let msg = read_stdout () in
1107
sync display_output msg;
1111
if show_error then sync display_error e;
1114
method find_phrase_starting_at (start:GText.iter) =
1115
prerr_endline "find_phrase_starting_at starting now";
1116
let trash_bytes = ref "" in
1117
let end_iter = start#copy in
1118
let lexbuf_function s count =
1120
let n_trash = String.length !trash_bytes in
1121
String.blit !trash_bytes 0 s 0 n_trash;
1124
while !i <= count - 1 do
1125
let c = end_iter#char in
1126
if c = 0 then raise (Stop !i);
1127
let c' = Glib.Utf8.from_unichar c in
1128
let n = String.length c' in
1129
if (n<=0) then exit (-2);
1130
if n > count - !i then
1132
let ri = count - !i in
1133
String.blit c' 0 s !i ri;
1134
trash_bytes := String.sub c' ri (n-ri);
1137
String.blit c' 0 s !i n;
1140
if not end_iter#nocopy#forward_char then
1149
let _ = Find_phrase.get (Lexing.from_function lexbuf_function)
1151
end_iter#nocopy#set_offset (start#offset + !Find_phrase.length);
1152
Some (start,end_iter)
1155
| Find_phrase.EOF s ->
1156
(* Phrase is at the end of the buffer*)
1157
let si = start#offset in
1158
let ei = si + !Find_phrase.length in
1159
end_iter#nocopy#set_offset (ei - 1);
1160
input_buffer#insert ~iter:end_iter "\n";
1161
Some (input_buffer#get_iter (`OFFSET si),
1162
input_buffer#get_iter (`OFFSET ei))
1166
method complete_at_offset (offset:int) =
1167
prerr_endline ("Completion at offset : " ^ string_of_int offset);
1168
let it () = input_buffer#get_iter (`OFFSET offset) in
1170
let start = find_word_start iit in
1171
if ends_word iit then
1172
let w = input_buffer#get_text
1177
if String.length w <> 0 then begin
1178
prerr_endline ("Completion of prefix : '" ^ w^"'");
1179
match complete input_buffer w start#offset with
1181
| Some (ss,start,stop) ->
1182
let completion = input_buffer#get_text ~start ~stop () in
1183
ignore (input_buffer#delete_selection ());
1184
ignore (input_buffer#insert_interactive completion);
1185
input_buffer#move_mark `SEL_BOUND (it())#backward_char;
1191
method process_next_phrase verbosely display_goals do_highlight =
1192
let get_next_phrase () =
1194
prerr_endline "process_next_phrase starting now";
1195
if do_highlight then begin
1196
!push_info "Coq is computing";
1197
input_view#set_editable false;
1199
match self#find_phrase_starting_at self#get_start_of_input with
1201
if do_highlight then begin
1202
input_view#set_editable true;
1206
| Some(start,stop) ->
1207
prerr_endline "process_next_phrase : to_process highlight";
1208
if do_highlight then begin
1209
input_buffer#apply_tag_by_name ~start ~stop "to_process";
1210
prerr_endline "process_next_phrase : to_process applied";
1212
prerr_endline "process_next_phrase : getting phrase";
1213
Some((start,stop),start#get_slice ~stop) in
1214
let remove_tag (start,stop) =
1215
if do_highlight then begin
1216
input_buffer#remove_tag_by_name ~start ~stop "to_process" ;
1217
input_view#set_editable true;
1220
let mark_processed reset_info complete (start,stop) ast =
1221
let b = input_buffer in
1222
b#move_mark ~where:stop (`NAME "start_of_input");
1224
(if complete then "processed" else "unjustified") ~start ~stop;
1225
if (self#get_insert#compare) stop <= 0 then
1227
b#place_cursor stop;
1228
self#recenter_insert
1230
let start_of_phrase_mark = `MARK (b#create_mark start) in
1231
let end_of_phrase_mark = `MARK (b#create_mark stop) in
1234
start_of_phrase_mark
1235
end_of_phrase_mark ast;
1236
if display_goals then self#show_goals;
1237
remove_tag (start,stop) in
1239
match sync get_next_phrase () with
1241
| Some (loc,phrase) ->
1242
(match self#send_to_coq verbosely false phrase true true true with
1243
| Some (complete,(reset_info,ast)) ->
1244
sync (mark_processed reset_info complete) loc ast; true
1245
| None -> sync remove_tag loc; false)
1248
method insert_this_phrase_on_success
1249
show_output show_msg localize coqphrase insertphrase =
1250
let mark_processed reset_info complete ast =
1251
let stop = self#get_start_of_input in
1252
if stop#starts_line then
1253
input_buffer#insert ~iter:stop insertphrase
1254
else input_buffer#insert ~iter:stop ("\n"^insertphrase);
1255
let start = self#get_start_of_input in
1256
input_buffer#move_mark ~where:stop (`NAME "start_of_input");
1257
input_buffer#apply_tag_by_name
1258
(if complete then "processed" else "unjustified") ~start ~stop;
1259
if (self#get_insert#compare) stop <= 0 then
1260
input_buffer#place_cursor stop;
1261
let start_of_phrase_mark = `MARK (input_buffer#create_mark start) in
1262
let end_of_phrase_mark = `MARK (input_buffer#create_mark stop) in
1263
push_phrase reset_info start_of_phrase_mark end_of_phrase_mark ast;
1265
(*Auto insert save on success...
1266
try (match Coq.get_current_goals () with
1268
(match self#send_to_coq "Save.\n" true true true with
1271
let stop = self#get_start_of_input in
1272
if stop#starts_line then
1273
input_buffer#insert ~iter:stop "Save.\n"
1274
else input_buffer#insert ~iter:stop "\nSave.\n";
1275
let start = self#get_start_of_input in
1276
input_buffer#move_mark ~where:stop (`NAME"start_of_input");
1277
input_buffer#apply_tag_by_name "processed" ~start ~stop;
1278
if (self#get_insert#compare) stop <= 0 then
1279
input_buffer#place_cursor stop;
1280
let start_of_phrase_mark =
1281
`MARK (input_buffer#create_mark start) in
1282
let end_of_phrase_mark =
1283
`MARK (input_buffer#create_mark stop) in
1285
reset_info start_of_phrase_mark end_of_phrase_mark ast
1290
match self#send_to_coq false false coqphrase show_output show_msg localize with
1291
| Some (complete,(reset_info,ast)) ->
1292
sync (mark_processed reset_info complete) ast; true
1295
(fun _ -> self#insert_message ("Unsuccessfully tried: "^coqphrase))
1299
method process_until_iter_or_error stop =
1300
let stop' = `OFFSET stop#offset in
1301
let start = self#get_start_of_input#copy in
1302
let start' = `OFFSET start#offset in
1304
input_buffer#apply_tag_by_name ~start ~stop "to_process";
1305
input_view#set_editable false) ();
1306
!push_info "Coq is computing";
1307
let get_current () =
1308
if !current.stop_before then
1309
match self#find_phrase_starting_at self#get_start_of_input with
1310
| None -> self#get_start_of_input
1311
| Some (_, stop2) -> stop2
1313
self#get_start_of_input
1317
while ((stop#compare (get_current())>=0)
1318
&& (self#process_next_phrase false false false))
1319
do Util.check_for_interrupt () done
1321
prerr_endline "Interrupted during process_until_iter_or_error");
1324
(* Start and stop might be invalid if an eol was added at eof *)
1325
let start = input_buffer#get_iter start' in
1326
let stop = input_buffer#get_iter stop' in
1327
input_buffer#remove_tag_by_name ~start ~stop "to_process" ;
1328
input_view#set_editable true) ();
1331
method process_until_end_or_error =
1332
self#process_until_iter_or_error input_buffer#end_iter
1334
method reset_initial =
1338
let start = input_buffer#get_iter_at_mark inf.start in
1339
let stop = input_buffer#get_iter_at_mark inf.stop in
1340
input_buffer#move_mark ~where:start (`NAME "start_of_input");
1341
input_buffer#remove_tag_by_name "processed" ~start ~stop;
1342
input_buffer#remove_tag_by_name "unjustified" ~start ~stop;
1343
input_buffer#delete_mark inf.start;
1344
input_buffer#delete_mark inf.stop;
1347
Stack.clear processed_stack;
1348
self#clear_message)();
1349
Coq.reset_initial ()
1351
(* backtrack Coq to the phrase preceding iterator [i] *)
1352
method backtrack_to_no_lock i =
1353
prerr_endline "Backtracking_to iter starts now.";
1354
(* pop Coq commands until we reach iterator [i] *)
1355
let rec pop_commands done_smthg undos =
1360
if i#compare (input_buffer#get_iter_at_mark t.stop) < 0 then
1362
prerr_endline "Popped top command";
1363
pop_commands true (pop_command undos t)
1368
let undos = (0,0,NoBacktrack,0,undo_info()) in
1369
let done_smthg, undos = pop_commands false undos in
1370
prerr_endline "Popped commands";
1377
if is_empty () then input_buffer#start_iter
1378
else input_buffer#get_iter_at_mark (top ()).stop in
1379
prerr_endline "Removing (long) processed tag...";
1380
input_buffer#remove_tag_by_name
1382
~stop:self#get_start_of_input
1384
input_buffer#remove_tag_by_name
1386
~stop:self#get_start_of_input
1388
prerr_endline "Moving (long) start_of_input...";
1389
input_buffer#move_mark ~where:start (`NAME "start_of_input");
1395
!push_info "WARNING: undo failed badly -> Coq might be in an inconsistent state.
1396
Please restart and report NOW.";
1398
else prerr_endline "backtrack_to : discarded (...)"
1400
method backtrack_to i =
1401
if Mutex.try_lock coq_may_stop then
1402
(!push_info "Undoing...";
1403
self#backtrack_to_no_lock i; Mutex.unlock coq_may_stop;
1405
else prerr_endline "backtrack_to : discarded (lock is busy)"
1407
method go_to_insert =
1408
let point = self#get_insert in
1409
if point#compare self#get_start_of_input>=0
1410
then self#process_until_iter_or_error point
1411
else self#backtrack_to point
1413
method undo_last_step =
1414
if Mutex.try_lock coq_may_stop then
1415
(!push_info "Undoing last step...";
1417
let last_command = top () in
1418
let start = input_buffer#get_iter_at_mark last_command.start in
1419
let update_input () =
1420
prerr_endline "Removing processed tag...";
1421
input_buffer#remove_tag_by_name
1423
~stop:(input_buffer#get_iter_at_mark last_command.stop)
1425
input_buffer#remove_tag_by_name
1427
~stop:(input_buffer#get_iter_at_mark last_command.stop)
1429
prerr_endline "Moving start_of_input";
1430
input_buffer#move_mark
1432
(`NAME "start_of_input");
1433
input_buffer#place_cursor start;
1434
self#recenter_insert;
1438
let undo = pop_command (0,0,NoBacktrack,0,undo_info()) last_command in
1440
sync update_input ()
1442
| Size 0 -> (* !flash_info "Nothing to Undo"*)()
1445
Mutex.unlock coq_may_stop)
1446
else prerr_endline "undo_last_step discarded"
1451
ignore (Thread.create
1453
prerr_endline "Blaster called";
1454
let c = Blaster_window.present_blaster_window () in
1455
if Mutex.try_lock c#lock then begin
1457
Decl_mode.check_not_proof_mode "No blaster in Proof mode";
1458
let current_gls = try get_current_goals () with _ -> [] in
1460
let set_goal i (s,t) =
1461
let gnb = string_of_int i in
1462
let s = gnb ^":"^s in
1463
let t' = gnb ^": progress "^t in
1464
let t'' = gnb ^": "^t in
1468
(fun () -> try_interptac t')
1469
(sync(fun () -> self#insert_command t'' t''))
1471
let set_current_goal (s,t) =
1475
(fun () -> try_interptac ("progress "^t))
1476
(sync(fun () -> self#insert_command t t))
1478
begin match current_gls with
1480
| (hyp_l,current_gl)::r ->
1481
List.iter set_current_goal (concl_menu current_gl);
1484
List.iter set_current_goal (hyp_menu hyp))
1489
List.iter (set_goal !i) (concl_menu gl);
1493
let _ = c#blaster () in
1495
end else prerr_endline "Blaster discarded")
1498
method insert_command cp ip =
1499
async(fun _ -> self#clear_message)();
1500
ignore (self#insert_this_phrase_on_success true false false cp ip)
1502
method tactic_wizard l =
1503
async(fun _ -> self#clear_message)();
1507
self#insert_this_phrase_on_success true false false
1508
("progress "^p^".\n") (p^".\n")) l)
1510
method active_keypress_handler k =
1511
let state = GdkEvent.Key.state k in
1514
| l when List.mem `MOD1 l ->
1515
let k = GdkEvent.Key.keyval k in
1516
if GdkKeysyms._Return=k
1518
if (input_buffer#insert_interactive "\n") then
1520
let i= self#get_insert#backward_word_start in
1521
prerr_endline "active_kp_hf: Placing cursor";
1522
self#process_until_iter_or_error i
1525
| l when List.mem `CONTROL l ->
1526
let k = GdkEvent.Key.keyval k in
1527
if GdkKeysyms._Break=k
1531
if GdkEvent.Key.keyval k = GdkKeysyms._Tab then begin
1532
prerr_endline "active_kp_handler for Tab";
1533
self#indent_current_line;
1537
method disconnected_keypress_handler k =
1538
match GdkEvent.Key.state k with
1539
| l when List.mem `CONTROL l ->
1540
let k = GdkEvent.Key.keyval k in
1547
val mutable deact_id = None
1548
val mutable act_id = None
1550
method deactivate () =
1552
(match act_id with None -> ()
1555
input_view#misc#disconnect id;
1556
prerr_endline "DISCONNECTED old active : ";
1560
(input_view#event#connect#key_press self#disconnected_keypress_handler);
1561
prerr_endline "CONNECTED inactive : ";
1562
print_id (Option.get deact_id)
1564
method activate () =
1566
(match deact_id with None -> ()
1567
| Some id -> input_view#misc#disconnect id;
1568
prerr_endline "DISCONNECTED old inactive : ";
1572
(input_view#event#connect#key_press self#active_keypress_handler);
1573
prerr_endline "CONNECTED active : ";
1574
print_id (Option.get act_id);
1576
(Option.get ((Vector.get input_views index).analyzed_view)) #filename
1579
| Some f -> let dir = Filename.dirname f in
1580
if not (is_in_loadpath dir) then
1582
ignore (Coq.interp false
1583
(Printf.sprintf "Add LoadPath \"%s\". " dir))
1586
method electric_handler =
1587
input_buffer#connect#insert_text ~callback:
1590
if last_index then begin
1592
if (last_array.(1) ^ last_array.(0) = ".\n") then raise Found
1595
if (last_array.(0) ^ last_array.(1) = ".\n") then raise Found
1599
ignore (self#process_next_phrase false true true)
1602
last_index <- not last_index;)
1604
method private electric_paren tag =
1605
let oparen_code = Glib.Utf8.to_unichar "(" (ref 0) in
1606
let cparen_code = Glib.Utf8.to_unichar ")" (ref 0) in
1607
ignore (input_buffer#connect#insert_text ~callback:
1609
input_buffer#remove_tag
1610
~start:input_buffer#start_iter
1611
~stop:input_buffer#end_iter
1613
if x = "" then () else
1614
match x.[String.length x - 1] with
1616
let hit = self#get_insert in
1617
let count = ref 0 in
1618
if hit#nocopy#backward_find_char
1620
if c = oparen_code && !count = 0 then true
1621
else if c = cparen_code then
1623
else if c = oparen_code then
1629
prerr_endline "Found matching parenthesis";
1630
input_buffer#apply_tag tag ~start:hit ~stop:hit#forward_char
1636
method help_for_keyword () =
1638
browse_keyword (self#insert_message) (get_current_word ())
1641
ignore (message_buffer#connect#insert_text
1642
~callback:(fun it s -> ignore
1643
(message_view#scroll_to_mark
1647
ignore (input_buffer#connect#insert_text
1648
~callback:(fun it s ->
1649
if (it#compare self#get_start_of_input)<0
1650
then GtkSignal.stop_emit ();
1651
if String.length s > 1 then
1652
(prerr_endline "insert_text: Placing cursor";input_buffer#place_cursor it)));
1653
ignore (input_buffer#connect#after#apply_tag
1654
~callback:(fun tag ~start ~stop ->
1655
if (start#compare self#get_start_of_input)>=0
1658
input_buffer#remove_tag_by_name
1662
input_buffer#remove_tag_by_name
1669
ignore (input_buffer#connect#after#insert_text
1670
~callback:(fun it s ->
1671
if auto_complete_on &&
1672
String.length s = 1 && s <> " " && s <> "\n"
1674
let v = Option.get (get_current_view ()).analyzed_view
1677
v#complete_at_offset
1678
((v#view#buffer#get_iter `SEL_BOUND)#offset)
1680
if has_completed then
1681
input_buffer#move_mark `SEL_BOUND (input_buffer#get_iter `SEL_BOUND)#forward_char;
1686
ignore (input_buffer#connect#modified_changed
1689
if input_buffer#modified then
1691
~icon:(match (Option.get (current_all.analyzed_view))#filename with
1695
else set_tab_image index ~icon:`YES;
1697
ignore (input_buffer#connect#changed
1698
~callback:(fun () ->
1699
last_modification_time <- Unix.time ();
1700
let r = input_view#visible_rect in
1702
input_view#get_iter_at_location
1703
~x:(Gdk.Rectangle.x r + Gdk.Rectangle.width r)
1704
~y:(Gdk.Rectangle.y r + Gdk.Rectangle.height r)
1706
input_buffer#remove_tag_by_name
1707
~start:self#get_start_of_input
1710
Highlight.highlight_around_current_line
1714
ignore (input_buffer#add_selection_clipboard (cb()));
1715
let paren_highlight_tag = input_buffer#create_tag ~name:"paren" [`BACKGROUND "purple"] in
1716
self#electric_paren paren_highlight_tag;
1717
ignore (input_buffer#connect#after#mark_set
1718
~callback:(fun it (m:Gtk.text_mark) ->
1721
"Line: %5d Char: %3d" (self#get_insert#line + 1)
1722
(self#get_insert#line_offset + 1));
1723
match GtkText.Mark.get_name m with
1725
input_buffer#remove_tag
1726
~start:input_buffer#start_iter
1727
~stop:input_buffer#end_iter
1728
paren_highlight_tag;
1730
prerr_endline (s^" moved")
1733
ignore (input_buffer#connect#insert_text
1735
prerr_endline "Should recenter ?";
1736
if String.contains s '\n' then begin
1737
prerr_endline "Should recenter : yes";
1738
self#recenter_insert
1742
let create_input_tab filename =
1743
let b = GText.buffer () in
1744
let _ = GMisc.label () in
1745
let v_box = GPack.hbox ~homogeneous:false () in
1746
let _ = GMisc.image ~packing:v_box#pack () in
1747
let _ = GMisc.label ~text:filename ~packing:v_box#pack () in
1748
let appendp x = ignore ((notebook ())#append_page
1749
~tab_label:v_box#coerce x) in
1750
let fr1 = GBin.frame ~shadow_type:`ETCHED_OUT
1753
let sw1 = GBin.scrolled_window
1758
let tv1 = Undo.undoable_view ~buffer:b ~packing:(sw1#add) () in
1759
prerr_endline ("Language: "^ b#start_iter#language);
1760
tv1#misc#set_name "ScriptWindow";
1761
let _ = tv1#set_editable true in
1762
let _ = tv1#set_wrap_mode `NONE in
1763
b#place_cursor ~where:(b#start_iter);
1764
ignore (tv1#event#connect#button_press ~callback:
1765
(fun ev -> GdkEvent.Button.button ev = 3));
1766
(* ignore (tv1#event#connect#button_press ~callback:
1768
if (GdkEvent.Button.button ev=2) then
1770
prerr_endline "Paste invoked";
1772
(get_current_view()).view#as_view
1773
GtkText.View.Signals.paste_clipboard;
1778
tv1#misc#grab_focus ();
1779
ignore (tv1#buffer#create_mark
1780
~name:"start_of_input"
1781
tv1#buffer#start_iter);
1782
ignore (tv1#buffer#create_tag
1784
[`FOREGROUND "blue"]);
1785
ignore (tv1#buffer#create_tag
1787
[`FOREGROUND "orange red"]);
1788
ignore (tv1#buffer#create_tag
1790
[`FOREGROUND "brown"]);
1791
ignore (tv1#buffer#create_tag
1793
[`FOREGROUND "dark red"]);
1794
ignore (tv1#buffer#create_tag
1796
[`UNDERLINE `DOUBLE ; `FOREGROUND "red"]);
1797
ignore (tv1#buffer#create_tag
1799
[`BACKGROUND "light blue" ;`EDITABLE false]);
1800
ignore (tv1#buffer#create_tag
1802
[`BACKGROUND "light green" ;`EDITABLE false]);
1803
ignore (tv1#buffer#create_tag (* Proof mode *)
1805
[`UNDERLINE `SINGLE ; `FOREGROUND "red";
1806
`BACKGROUND "gold" ;`EDITABLE false]);
1807
ignore (tv1#buffer#create_tag
1809
[`BACKGROUND "blue"; `FOREGROUND "white"]);
1813
let last_make = ref "";;
1814
let last_make_index = ref 0;;
1815
let search_compile_error_regexp =
1817
"File \"\\([^\"]+\\)\", line \\([0-9]+\\), characters \\([0-9]+\\)-\\([0-9]+\\)";;
1819
let search_next_error () =
1820
let _ = Str.search_forward search_compile_error_regexp !last_make !last_make_index in
1821
let f = Str.matched_group 1 !last_make
1822
and l = int_of_string (Str.matched_group 2 !last_make)
1823
and b = int_of_string (Str.matched_group 3 !last_make)
1824
and e = int_of_string (Str.matched_group 4 !last_make)
1825
and msg_index = Str.match_beginning ()
1827
last_make_index := Str.group_end 4;
1829
String.sub !last_make msg_index (String.length !last_make - msg_index))
1832
(* Statup preferences *)
1836
let w = GWindow.window
1837
~wm_class:"CoqIde" ~wm_name:"CoqIde"
1838
~allow_grow:true ~allow_shrink:true
1839
~width:!current.window_width ~height:!current.window_height
1843
let icon_image = lib_ide_file "coq.png" in
1844
let icon = GdkPixbuf.from_file icon_image in
1845
w#set_icon (Some icon)
1848
let vbox = GPack.vbox ~homogeneous:false ~packing:w#add () in
1852
let menubar = GMenu.menu_bar ~packing:vbox#pack () in
1855
let toolbar = GButton.toolbar
1856
~orientation:`HORIZONTAL
1859
~packing:(* handle#add *)
1860
(vbox#pack ~expand:false ~fill:false)
1864
(fun b -> if b then toolbar#misc#show () else toolbar#misc#hide ());
1866
let factory = new GMenu.factory ~accel_path:"<CoqIde MenuBar>/" menubar in
1867
let accel_group = factory#accel_group in
1870
let file_menu = factory#add_submenu "_File" in
1872
let file_factory = new GMenu.factory ~accel_path:"<CoqIde MenuBar>/File/" file_menu ~accel_group in
1874
(* File/Load Menu *)
1875
let load_file handler f =
1876
let f = absolute_filename f in
1878
prerr_endline "Loading file starts";
1881
| {analyzed_view=Some av} ->
1882
(match av#filename with
1884
| Some fn -> same_file f fn)
1887
prerr_endline "Loading: must open";
1888
let b = Buffer.create 1024 in
1889
prerr_endline "Loading: get raw content";
1890
with_file handler f ~f:(input_channel b);
1891
prerr_endline "Loading: convert content";
1892
let s = do_convert (Buffer.contents b) in
1893
prerr_endline "Loading: create view";
1894
let view = create_input_tab (Glib.Convert.filename_to_utf8
1895
(Filename.basename f))
1897
prerr_endline "Loading: change font";
1898
view#misc#modify_font !current.text_font;
1899
prerr_endline "Loading: adding view";
1900
let index = add_input_view {view = view;
1901
analyzed_view = None;
1904
let av = (new analyzed_view index) in
1905
prerr_endline "Loading: register view";
1906
(get_input_view index).analyzed_view <- Some av;
1907
prerr_endline "Loading: set filename";
1908
av#set_filename (Some f);
1909
prerr_endline "Loading: stats";
1911
let input_buffer = view#buffer in
1912
prerr_endline "Loading: fill buffer";
1913
input_buffer#set_text s;
1914
input_buffer#place_cursor input_buffer#start_iter;
1915
prerr_endline ("Loading: switch to view "^ string_of_int index);
1916
set_current_view index;
1917
set_tab_image index ~icon:`YES;
1918
prerr_endline "Loading: highlight";
1919
Highlight.highlight_all input_buffer;
1920
input_buffer#set_modified false;
1921
prerr_endline "Loading: clear undo";
1923
prerr_endline "Loading: success"
1925
| Vector.Found i -> set_current_view i
1926
| e -> handler ("Load failed: "^(Printexc.to_string e))
1928
let load f = load_file !flash_info f in
1929
let load_m = file_factory#add_item "_New"
1930
~key:GdkKeysyms._N in
1932
match select_file_for_save ~title:"Create file" () with
1936
ignore (load_m#connect#activate (load_f));
1938
let load_m = file_factory#add_item "_Open"
1939
~key:GdkKeysyms._O in
1941
match select_file_for_open ~title:"Load file" () with
1945
ignore (load_m#connect#activate (load_f));
1947
(* File/Save Menu *)
1948
let save_m = file_factory#add_item "_Save"
1949
~key:GdkKeysyms._S in
1953
let current = get_current_view () in
1955
(match (Option.get current.analyzed_view)#filename with
1957
begin match select_file_for_save ~title:"Save file" ()
1961
if (Option.get current.analyzed_view)#save_as f then begin
1962
set_current_tab_label (Filename.basename f);
1963
!flash_info ("File " ^ f ^ " saved")
1965
else warning ("Save Failed (check if " ^ f ^ " is writable)")
1968
if (Option.get current.analyzed_view)#save f then
1969
!flash_info ("File " ^ f ^ " saved")
1970
else warning ("Save Failed (check if " ^ f ^ " is writable)")
1974
| e -> warning "Save: unexpected error"
1976
ignore (save_m#connect#activate save_f);
1978
(* File/Save As Menu *)
1979
let saveas_m = file_factory#add_item "S_ave as"
1982
let current = get_current_view () in
1983
try (match (Option.get current.analyzed_view)#filename with
1985
begin match select_file_for_save ~title:"Save file as" ()
1989
if (Option.get current.analyzed_view)#save_as f then begin
1990
set_current_tab_label (Filename.basename f);
1993
else !flash_info "Save Failed"
1996
begin match select_file_for_save
1997
~dir:(ref (Filename.dirname f))
1998
~filename:(Filename.basename f)
1999
~title:"Save file as" ()
2003
if (Option.get current.analyzed_view)#save_as f then begin
2004
set_current_tab_label (Filename.basename f);
2006
end else !flash_info "Save Failed"
2008
with e -> !flash_info "Save Failed"
2010
ignore (saveas_m#connect#activate saveas_f);
2012
(* File/Save All Menu *)
2013
let saveall_m = file_factory#add_item "Sa_ve all" in
2017
| {view = view ; analyzed_view = Some av} ->
2018
begin match av#filename with
2026
let has_something_to_save () =
2029
| {view=view} -> view#buffer#modified
2033
ignore (saveall_m#connect#activate saveall_f);
2035
(* File/Revert Menu *)
2036
let revert_m = file_factory#add_item "_Revert all buffers" in
2040
{view = view ; analyzed_view = Some av} ->
2042
match av#filename,av#stats with
2043
| Some f,Some stats ->
2044
let new_stats = Unix.stat f in
2045
if new_stats.Unix.st_mtime > stats.Unix.st_mtime
2047
| Some _, None -> av#revert
2049
with _ -> av#revert)
2053
ignore (revert_m#connect#activate revert_f);
2055
(* File/Close Menu *)
2057
file_factory#add_item "_Close buffer" ~key:GdkKeysyms._W in
2059
let v = Option.get !active_view in
2060
let act = get_current_view_page () in
2061
if v = act then !flash_info "Cannot close an active view"
2062
else remove_current_view_page ()
2064
ignore (close_m#connect#activate close_f);
2066
(* File/Print Menu *)
2068
let v = get_current_view () in
2069
let av = Option.get v.analyzed_view in
2070
match av#filename with
2072
!flash_info "Cannot print: this buffer has no name"
2075
"cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^
2076
!current.cmd_coqdoc ^ " -ps " ^ Filename.quote (Filename.basename f) ^
2077
" | " ^ !current.cmd_print
2079
let print_window = GWindow.window
2084
~wm_name: "CodIDE" () in
2085
let vbox_print = GPack.vbox
2088
~packing:print_window#add () in
2091
~text:"Print using the following command:"
2092
~packing:vbox_print#add () in
2093
let print_entry = GEdit.entry
2097
~packing:vbox_print#add () in
2098
let hbox_print = GPack.hbox
2100
~packing:vbox_print#add () in
2101
let print_cancel_button = GButton.button ~stock:`CANCEL ~label:"Cancel" ~packing:hbox_print#add () in
2102
let print_button = GButton.button ~stock:`PRINT ~label:"Print" ~packing:hbox_print#add () in
2103
let callback_print () =
2104
let cmd = print_entry#text in
2105
let s,_ = run_command av#insert_message cmd in
2106
!flash_info (cmd ^ if s = Unix.WEXITED 0 then " succeeded" else " failed");
2107
print_window#destroy ()
2109
ignore (print_cancel_button#connect#clicked ~callback:print_window#destroy) ;
2110
ignore (print_button#connect#clicked ~callback:callback_print);
2111
print_window#misc#show();
2113
let _ = file_factory#add_item "_Print..."
2115
~callback:print_f in
2117
(* File/Export to Menu *)
2118
let export_f kind () =
2119
let v = get_current_view () in
2120
let av = Option.get v.analyzed_view in
2121
match av#filename with
2123
!flash_info "Cannot print: this buffer has no name"
2125
let basef = Filename.basename f in
2127
let basef_we = try Filename.chop_extension basef with _ -> basef in
2129
| "latex" -> basef_we ^ ".tex"
2130
| "dvi" | "ps" | "pdf" | "html" -> basef_we ^ "." ^ kind
2134
"cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^
2135
!current.cmd_coqdoc ^ " --" ^ kind ^ " -o " ^ (Filename.quote output) ^ " " ^ (Filename.quote basef)
2137
let s,_ = run_command av#insert_message cmd in
2139
if s = Unix.WEXITED 0
2143
let file_export_m = file_factory#add_submenu "E_xport to" in
2145
let file_export_factory = new GMenu.factory ~accel_path:"<CoqIde MenuBar>/Export/" file_export_m ~accel_group in
2147
file_export_factory#add_item "_Html" ~callback:(export_f "html")
2150
file_export_factory#add_item "_LaTeX" ~callback:(export_f "latex")
2153
file_export_factory#add_item "_Dvi" ~callback:(export_f "dvi")
2156
file_export_factory#add_item "_Pdf" ~callback:(export_f "pdf")
2159
file_export_factory#add_item "_Ps" ~callback:(export_f "ps")
2162
(* File/Rehighlight Menu *)
2163
let rehighlight_m = file_factory#add_item "Reh_ighlight" ~key:GdkKeysyms._L in
2164
ignore (rehighlight_m#connect#activate
2166
Highlight.highlight_all
2167
(get_current_view()).view#buffer;
2168
(Option.get (get_current_view()).analyzed_view)#recenter_insert));
2170
(* File/Quit Menu *)
2173
if has_something_to_save () then
2174
match (GToolbox.question_box ~title:"Quit"
2175
~buttons:["Save Named Buffers and Quit";
2176
"Quit without Saving";
2180
(let img = GMisc.image () in
2181
img#set_stock `DIALOG_WARNING;
2182
img#set_icon_size `DIALOG;
2184
"There are unsaved buffers"
2186
with 1 -> saveall_f () ; exit 0
2191
let _ = file_factory#add_item "_Quit" ~key:GdkKeysyms._Q
2194
ignore (w#event#connect#delete (fun _ -> quit_f (); true));
2197
let edit_menu = factory#add_submenu "_Edit" in
2198
let edit_f = new GMenu.factory ~accel_path:"<CoqIde MenuBar>/Edit/" edit_menu ~accel_group in
2199
ignore(edit_f#add_item "_Undo" ~key:GdkKeysyms._u ~callback:
2200
(do_if_not_computing "undo"
2202
ignore ((Option.get ((get_current_view()).analyzed_view))#
2203
without_auto_complete
2204
(fun () -> (get_current_view()).view#undo) ()))));
2205
ignore(edit_f#add_item "_Clear Undo Stack"
2206
(* ~key:GdkKeysyms._exclam *)
2209
ignore (get_current_view()).view#clear_undo));
2210
ignore(edit_f#add_separator ());
2211
ignore(edit_f#add_item "Cut" ~key:GdkKeysyms._X ~callback:
2212
(fun () -> GtkSignal.emit_unit
2213
(get_current_view()).view#as_view
2214
GtkText.View.S.cut_clipboard));
2215
ignore(edit_f#add_item "Copy" ~key:GdkKeysyms._C ~callback:
2216
(fun () -> GtkSignal.emit_unit
2217
(get_current_view()).view#as_view
2218
GtkText.View.S.copy_clipboard));
2219
ignore(edit_f#add_item "Paste" ~key:GdkKeysyms._V ~callback:
2221
try GtkSignal.emit_unit
2222
(get_current_view()).view#as_view
2223
GtkText.View.S.paste_clipboard
2224
with _ -> prerr_endline "EMIT PASTE FAILED"));
2225
ignore (edit_f#add_separator ());
2229
let toggle_auto_complete_i =
2230
edit_f#add_check_item "_Auto Completion"
2231
~active:!current.auto_complete
2237
(fun b -> match (get_current_view()).analyzed_view with
2238
| Some av -> av#set_auto_complete b
2242
let last_found = ref None in
2243
let search_backward = ref false in
2244
let find_w = GWindow.window
2245
(* ~wm_class:"CoqIde" ~wm_name:"CoqIde" *)
2246
(* ~allow_grow:true ~allow_shrink:true *)
2247
(* ~width:!current.window_width ~height:!current.window_height *)
2249
~title:"CoqIde search/replace" ()
2251
let find_box = GPack.table
2253
~col_spacings:10 ~row_spacings:10 ~border_width:10
2254
~homogeneous:false ~packing:find_w#add () in
2257
GMisc.label ~text:"Find:"
2259
~packing:(find_box#attach ~left:0 ~top:0 ~fill:`X) ()
2261
let find_entry = GEdit.entry
2263
~packing: (find_box#attach ~left:1 ~top:0 ~expand:`X)
2267
GMisc.label ~text:"Replace with:"
2269
~packing:(find_box#attach ~left:0 ~top:1 ~fill:`X) ()
2271
let replace_entry = GEdit.entry
2273
~packing: (find_box#attach ~left:1 ~top:1 ~expand:`X)
2277
GButton.check_button
2278
~label:"case sensitive"
2280
~packing: (find_box#attach ~left:1 ~top:2)
2286
let find_backwards_check =
2287
GButton.check_button
2288
~label:"search backwards"
2290
~packing: (find_box#attach ~left:1 ~top:3)
2294
let close_find_button =
2297
~packing: (find_box#attach ~left:2 ~top:0)
2300
let replace_button =
2303
~packing: (find_box#attach ~left:2 ~top:1)
2306
let replace_find_button =
2308
~label:"Replace and find"
2309
~packing: (find_box#attach ~left:2 ~top:2)
2312
let find_again_button =
2314
~label:"_Find again"
2315
~packing: (find_box#attach ~left:2 ~top:3)
2318
let find_again_backward_button =
2320
~label:"Find _backward"
2321
~packing: (find_box#attach ~left:2 ~top:4)
2325
let v = (get_current_view()).view in
2328
match !last_found with
2329
| None -> let i = b#get_iter_at_mark `INSERT in (i,i)
2330
| Some(start,stop) ->
2331
let start = b#get_iter_at_mark start
2332
and stop = b#get_iter_at_mark stop
2334
b#remove_tag_by_name ~start ~stop "found";
2341
let v = (get_current_view()).view in
2343
match !last_found with
2345
| Some(start,stop) ->
2346
let start = b#get_iter_at_mark start
2347
and stop = b#get_iter_at_mark stop
2349
b#delete ~start ~stop;
2350
b#insert ~iter:start replace_entry#text;
2353
let find_from (v : Undo.undoable_view)
2354
(b : GText.buffer) (starti : GText.iter) text =
2355
prerr_endline ("Searching for " ^ text);
2356
match (if !search_backward then starti#backward_search text
2357
else starti#forward_search text)
2360
| Some(start,stop) ->
2361
b#apply_tag_by_name "found" ~start ~stop;
2362
let start = `MARK (b#create_mark start)
2363
and stop = `MARK (b#create_mark stop)
2365
v#scroll_to_mark ~use_align:false ~yalign:0.75 ~within_margin:0.25
2367
last_found := Some(start,stop)
2370
let (v,b,starti,_) = last_find () in
2371
find_from v b starti find_entry#text
2373
let do_replace_find () =
2378
let (v,b,_,stop) = last_find () in
2379
b#place_cursor stop;
2381
v#coerce#misc#grab_focus()
2383
to_do_on_page_switch :=
2384
(fun i -> if find_w#misc#visible then close_find())::
2385
!to_do_on_page_switch;
2386
let find_again_forward () =
2387
search_backward := false;
2388
let (v,b,start,_) = last_find () in
2389
let start = start#forward_chars 1 in
2390
find_from v b start find_entry#text
2392
let find_again_backward () =
2393
search_backward := true;
2394
let (v,b,start,_) = last_find () in
2395
let start = start#backward_chars 1 in
2396
find_from v b start find_entry#text
2399
let s = GdkEvent.Key.state ev and k = GdkEvent.Key.keyval ev in
2400
if k = GdkKeysyms._Escape then
2402
let (v,b,_,stop) = last_find () in
2404
v#coerce#misc#grab_focus();
2407
else if k = GdkKeysyms._Return then
2412
else if List.mem `CONTROL s && k = GdkKeysyms._f then
2414
find_again_forward ();
2417
else if List.mem `CONTROL s && k = GdkKeysyms._b then
2419
find_again_backward ();
2422
else false (* to let default callback execute *)
2424
let find_f ~backward () =
2425
search_backward := backward;
2428
find_entry#misc#grab_focus ()
2430
let _ = edit_f#add_item "_Find in buffer"
2432
~callback:(find_f ~backward:false)
2434
let _ = edit_f#add_item "Find _backwards"
2436
~callback:(find_f ~backward:true)
2438
let _ = close_find_button#connect#clicked close_find in
2439
let _ = replace_button#connect#clicked do_replace in
2440
let _ = replace_find_button#connect#clicked do_replace_find in
2441
let _ = find_again_button#connect#clicked find_again_forward in
2442
let _ = find_again_backward_button#connect#clicked find_again_backward in
2443
let _ = find_entry#connect#changed do_find in
2444
let _ = find_entry#event#connect#key_press ~callback:key_find in
2445
let _ = find_w#event#connect#delete (fun _ -> find_w#misc#hide(); true) in
2447
let search_if = edit_f#add_item "Search _forward"
2448
~key:GdkKeysyms._greater
2450
let search_ib = edit_f#add_item "Search _backward"
2451
~key:GdkKeysyms._less
2455
let complete_i = edit_f#add_item "_Complete"
2456
~key:GdkKeysyms._comma
2458
(do_if_not_computing
2460
let v = Option.get (get_current_view ()).analyzed_view
2462
in v#complete_at_offset
2463
((v#view#buffer#get_iter `SEL_BOUND)#offset)
2466
complete_i#misc#set_state `INSENSITIVE;
2469
ignore(edit_f#add_item "Complete Word" ~key:GdkKeysyms._slash ~callback:
2472
let av = Option.get ((get_current_view()).analyzed_view) in
2473
av#complete_at_offset (av#get_insert)#offset
2476
ignore(edit_f#add_separator ());
2477
(* external editor *)
2479
edit_f#add_item "External editor" ~callback:
2481
let av = Option.get ((get_current_view()).analyzed_view) in
2482
match av#filename with
2483
| None -> warning "Call to external editor available only on named files"
2486
let com = Flags.subst_command_placeholder !current.cmd_editor (Filename.quote f) in
2487
let _ = run_command av#insert_message com in
2490
let _ = edit_f#add_separator () in
2492
let reset_revert_timer () =
2493
disconnect_revert_timer ();
2494
if !current.global_auto_revert then
2495
revert_timer := Some
2496
(GMain.Timeout.add ~ms:!current.global_auto_revert_delay
2499
do_if_not_computing "revert" (sync revert_f) ();
2501
in reset_revert_timer (); (* to enable statup preferences timer *)
2503
let auto_save_f () =
2506
{view = view ; analyzed_view = Some av} ->
2515
let reset_auto_save_timer () =
2516
disconnect_auto_save_timer ();
2517
if !current.auto_save then
2518
auto_save_timer := Some
2519
(GMain.Timeout.add ~ms:!current.auto_save_delay
2522
do_if_not_computing "autosave" (sync auto_save_f) ();
2524
in reset_auto_save_timer (); (* to enable statup preferences timer *)
2528
edit_f#add_item "_Preferences"
2529
~callback:(fun () -> configure ~apply:update_notebook_pos (); reset_revert_timer ())
2533
configuration_factory#add_item "_Save preferences"
2534
~callback:(fun () -> save_pref ())
2537
(* Navigation Menu *)
2538
let navigation_menu = factory#add_submenu "_Navigation" in
2539
let navigation_factory =
2540
new GMenu.factory navigation_menu
2541
~accel_path:"<CoqIde MenuBar>/Navigation/"
2543
~accel_modi:!current.modifier_for_navigation
2545
let do_or_activate f () =
2546
let current = get_current_view () in
2547
let analyzed_view = Option.get current.analyzed_view in
2548
if analyzed_view#is_active then
2549
ignore (f analyzed_view)
2552
!flash_info "New proof started";
2553
activate_input (notebook ())#current_page;
2554
ignore (f analyzed_view)
2558
let do_or_activate f =
2559
do_if_not_computing "do_or_activate"
2561
(fun av -> f av ; !pop_info();!push_info (Coq.current_status())))
2564
let add_to_menu_toolbar text ~tooltip ?key ~callback icon =
2566
match key with None -> ()
2567
| Some key -> ignore (navigation_factory#add_item text ~key ~callback)
2569
ignore (toolbar#insert_button
2572
~icon:(stock_to_widget ~size:`LARGE_TOOLBAR icon)
2578
~tooltip:"Save current buffer"
2583
~tooltip:"Close current buffer"
2588
~tooltip:"Forward one command"
2589
~key:GdkKeysyms._Down
2590
~callback:(do_or_activate (fun a -> a#process_next_phrase true true true))
2592
add_to_menu_toolbar "_Backward"
2593
~tooltip:"Backward one command"
2595
~callback:(do_or_activate (fun a -> a#undo_last_step))
2599
~tooltip:"Go to cursor"
2600
~key:GdkKeysyms._Right
2601
~callback:(do_or_activate (fun a-> a#go_to_insert))
2605
~tooltip:"Go to start"
2606
~key:GdkKeysyms._Home
2607
~callback:(do_or_activate (fun a -> a#reset_initial))
2611
~tooltip:"Go to end"
2612
~key:GdkKeysyms._End
2613
~callback:(do_or_activate (fun a -> a#process_until_end_or_error))
2615
add_to_menu_toolbar "_Interrupt"
2616
~tooltip:"Interrupt computations"
2617
~key:GdkKeysyms._Break
2622
let tactics_menu = factory#add_submenu "_Try Tactics" in
2623
let tactics_factory =
2624
new GMenu.factory tactics_menu
2625
~accel_path:"<CoqIde MenuBar>/Tactics/"
2627
~accel_modi:!current.modifier_for_tactics
2629
let do_if_active_raw f () =
2630
let current = get_current_view () in
2631
let analyzed_view = Option.get current.analyzed_view in
2632
if analyzed_view#is_active then ignore (f analyzed_view)
2634
let do_if_active f =
2635
do_if_not_computing "do_if_active" (do_if_active_raw f) in
2639
tactics_factory#add_item "_Blaster"
2641
~callback: (do_if_active_raw (fun a -> a#blaster ()))
2642
(* Custom locking mechanism! *)
2644
blaster_i#misc#set_state `INSENSITIVE;
2647
ignore (tactics_factory#add_item "_auto"
2649
~callback:(do_if_active (fun a -> a#insert_command "progress auto.\n" "auto.\n"))
2651
ignore (tactics_factory#add_item "_auto with *"
2652
~key:GdkKeysyms._asterisk
2653
~callback:(do_if_active (fun a -> a#insert_command
2654
"progress auto with *.\n"
2655
"auto with *.\n")));
2656
ignore (tactics_factory#add_item "_eauto"
2658
~callback:(do_if_active (fun a -> a#insert_command
2662
ignore (tactics_factory#add_item "_eauto with *"
2663
~key:GdkKeysyms._ampersand
2664
~callback:(do_if_active (fun a -> a#insert_command
2665
"progress eauto with *.\n"
2668
ignore (tactics_factory#add_item "_intuition"
2670
~callback:(do_if_active (fun a -> a#insert_command
2671
"progress intuition.\n"
2674
ignore (tactics_factory#add_item "_omega"
2676
~callback:(do_if_active (fun a -> a#insert_command
2677
"omega.\n" "omega.\n"))
2679
ignore (tactics_factory#add_item "_simpl"
2681
~callback:(do_if_active (fun a -> a#insert_command "progress simpl.\n" "simpl.\n" ))
2683
ignore (tactics_factory#add_item "_tauto"
2685
~callback:(do_if_active (fun a -> a#insert_command "tauto.\n" "tauto.\n" ))
2687
ignore (tactics_factory#add_item "_trivial"
2689
~callback:(do_if_active( fun a -> a#insert_command "progress trivial.\n" "trivial.\n" ))
2693
ignore (toolbar#insert_button
2694
~tooltip:"Proof Wizard"
2696
~icon:(stock_to_widget ~size:`LARGE_TOOLBAR `DIALOG_INFO)
2697
~callback:(do_if_active (fun a -> a#tactic_wizard
2698
!current.automatic_tactics
2704
ignore (tactics_factory#add_item "<Proof _Wizard>"
2705
~key:GdkKeysyms._dollar
2706
~callback:(do_if_active (fun a -> a#tactic_wizard
2707
!current.automatic_tactics
2711
ignore (tactics_factory#add_separator ());
2712
let add_simple_template (factory: GMenu.menu GMenu.factory)
2715
let l = String.length text - 1 in
2716
if String.get text l = '.'
2720
ignore (factory#add_item menu_text
2722
(fun () -> let {view = view } = get_current_view () in
2723
ignore (view#buffer#insert_interactive text)))
2729
| [s] -> add_simple_template tactics_factory ("_"^s, s)
2733
let f = tactics_factory#add_submenu a in
2734
let ff = new GMenu.factory f ~accel_group in
2739
((String.sub x 0 1)^
2741
(String.sub x 1 (String.length x - 1)),
2745
Coq_commands.tactics;
2747
(* Templates Menu *)
2748
let templates_menu = factory#add_submenu "Te_mplates" in
2749
let templates_factory = new GMenu.factory templates_menu
2750
~accel_path:"<CoqIde MenuBar>/Templates/"
2752
~accel_modi:!current.modifier_for_templates
2754
let add_complex_template (menu_text, text, offset, len, key) =
2755
(* Templates/Lemma *)
2757
let {view = view } = get_current_view () in
2758
if view#buffer#insert_interactive text then begin
2759
let iter = view#buffer#get_iter_at_mark `INSERT in
2760
ignore (iter#nocopy#backward_chars offset);
2761
view#buffer#move_mark `INSERT iter;
2762
ignore (iter#nocopy#backward_chars len);
2763
view#buffer#move_mark `SEL_BOUND iter;
2765
ignore (templates_factory#add_item menu_text ~callback ?key)
2767
add_complex_template
2768
("_Lemma __", "Lemma new_lemma : .\nProof.\n\nSave.\n",
2769
19, 9, Some GdkKeysyms._L);
2770
add_complex_template
2771
("_Theorem __", "Theorem new_theorem : .\nProof.\n\nSave.\n",
2772
19, 11, Some GdkKeysyms._T);
2773
add_complex_template
2774
("_Definition __", "Definition ident := .\n",
2775
6, 5, Some GdkKeysyms._D);
2776
add_complex_template
2777
("_Inductive __", "Inductive ident : :=\n | : .\n",
2778
14, 5, Some GdkKeysyms._I);
2779
add_complex_template
2780
("_Fixpoint __", "Fixpoint ident (_ : _) {struct _} : _ :=\n.\n",
2781
29, 5, Some GdkKeysyms._F);
2782
add_complex_template("_Scheme __",
2783
"Scheme new_scheme := Induction for _ Sort _
2784
with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
2786
(* Template for match *)
2788
let w = get_current_word () in
2790
let cases = Coq.make_cases w
2792
let print c = function
2793
| [x] -> Format.fprintf c " | %s => _@\n" x
2794
| x::l -> Format.fprintf c " | (%s%a) => _@\n" x
2795
(print_list (fun c s -> Format.fprintf c " %s" s)) l
2796
| [] -> assert false
2798
let b = Buffer.create 1024 in
2799
let fmt = Format.formatter_of_buffer b in
2800
Format.fprintf fmt "@[match var with@\n%aend@]@."
2801
(print_list print) cases;
2802
let s = Buffer.contents b in
2804
let {view = view } = get_current_view () in
2805
ignore (view#buffer#delete_selection ());
2806
let m = view#buffer#create_mark
2807
(view#buffer#get_iter `INSERT)
2809
if view#buffer#insert_interactive s then
2810
let i = view#buffer#get_iter (`MARK m) in
2811
let _ = i#nocopy#forward_chars 9 in
2812
view#buffer#place_cursor i;
2813
view#buffer#move_mark ~where:(i#backward_chars 3)
2815
with Not_found -> !flash_info "Not an inductive type"
2817
ignore (templates_factory#add_item "match ..."
2823
let add_simple_template (factory: GMenu.menu GMenu.factory)
2826
let l = String.length text - 1 in
2827
if String.get text l = '.'
2831
ignore (factory#add_item menu_text
2833
(fun () -> let {view = view } = get_current_view () in
2834
ignore (view#buffer#insert_interactive text)))
2837
ignore (templates_factory#add_separator ());
2839
List.iter (add_simple_template templates_factory)
2841
"_auto with *", "auto with * ";
2843
"_eauto with *", "eauto with * ";
2844
"_intuition", "intuition ";
2848
"tri_vial", "trivial ";
2850
ignore (templates_factory#add_separator ());
2856
| [s] -> add_simple_template templates_factory ("_"^s, s)
2860
let f = templates_factory#add_submenu a in
2861
let ff = new GMenu.factory f ~accel_group in
2866
((String.sub x 0 1)^
2868
(String.sub x 1 (String.length x - 1)),
2872
Coq_commands.commands;
2875
let queries_menu = factory#add_submenu "_Queries" in
2876
let queries_factory = new GMenu.factory queries_menu ~accel_group
2877
~accel_path:"<CoqIde MenuBar>/Queries"
2881
(* Command/Show commands *)
2883
queries_factory#add_item "_SearchAbout " ~key:GdkKeysyms._F2
2884
~callback:(fun () -> let term = get_current_word () in
2885
(Command_windows.command_window ())#new_command
2886
~command:"SearchAbout"
2891
queries_factory#add_item "_Check " ~key:GdkKeysyms._F3
2892
~callback:(fun () -> let term = get_current_word () in
2893
(Command_windows.command_window ())#new_command
2899
queries_factory#add_item "_Print " ~key:GdkKeysyms._F4
2900
~callback:(fun () -> let term = get_current_word () in
2901
(Command_windows.command_window ())#new_command
2907
queries_factory#add_item "_Locate"
2908
~callback:(fun () -> let term = get_current_word () in
2909
(Command_windows.command_window ())#new_command
2915
queries_factory#add_item "_Whelp Locate"
2916
~callback:(fun () -> let term = get_current_word () in
2917
(Command_windows.command_window ())#new_command
2918
~command:"Whelp Locate"
2925
let display_menu = factory#add_submenu "_Display" in
2926
let view_factory = new GMenu.factory display_menu
2927
~accel_path:"<CoqIde MenuBar>/Display/"
2929
~accel_modi:!current.modifier_for_display
2932
let _ = ignore (view_factory#add_check_item
2933
"Display _implicit arguments"
2935
~callback:(fun _ -> printing_state.printing_implicit <- not printing_state.printing_implicit; do_or_activate (fun a -> a#show_goals) ())) in
2937
let _ = ignore (view_factory#add_check_item
2938
"Display _coercions"
2940
~callback:(fun _ -> printing_state.printing_coercions <- not printing_state.printing_coercions; do_or_activate (fun a -> a#show_goals) ())) in
2942
let _ = ignore (view_factory#add_check_item
2943
"Display raw _matching expressions"
2945
~callback:(fun _ -> printing_state.printing_raw_matching <- not printing_state.printing_raw_matching; do_or_activate (fun a -> a#show_goals) ())) in
2947
let _ = ignore (view_factory#add_check_item
2948
"Deactivate _notations display"
2950
~callback:(fun _ -> printing_state.printing_no_notation <- not printing_state.printing_no_notation; do_or_activate (fun a -> a#show_goals) ())) in
2952
let _ = ignore (view_factory#add_check_item
2953
"Display _all basic low-level contents"
2955
~callback:(fun _ -> printing_state.printing_all <- not printing_state.printing_all; do_or_activate (fun a -> a#show_goals) ())) in
2957
let _ = ignore (view_factory#add_check_item
2958
"Display _existential variable instances"
2960
~callback:(fun _ -> printing_state.printing_evar_instances <- not printing_state.printing_evar_instances; do_or_activate (fun a -> a#show_goals) ())) in
2962
let _ = ignore (view_factory#add_check_item
2963
"Display _universe levels"
2965
~callback:(fun _ -> printing_state.printing_universes <- not printing_state.printing_universes; do_or_activate (fun a -> a#show_goals) ())) in
2967
let _ = ignore (view_factory#add_check_item
2968
"Display all _low-level contents"
2970
~callback:(fun _ -> printing_state.printing_full_all <- not printing_state.printing_full_all; do_or_activate (fun a -> a#show_goals) ())) in
2974
let unicode_menu = factory#add_submenu "_Unicode" in
2975
let unicode_factory = new GMenu.factory unicode_menu
2976
~accel_path:"<CoqIde MenuBar>/Unicode/"
2980
let logic_symbols_menu = unicode_factory#add_submenu "Math operators" in
2981
let logic_factory = new GMenu.factory logic_symbols_menu
2982
~accel_path:"<CoqIde MenuBar>/Unicode/Math operators"
2986
let new_unicode_item s = ignore (
2987
logic_factory#add_item s
2988
~callback:(fun () ->
2989
let v = get_current_view () in
2990
ignore (v.view#buffer#insert_interactive s)))
2993
for i = 0x2200 to 0x22FF do
2994
List.iter new_unicode_item [Glib.Utf8.from_unichar i];
3002
let externals_menu = factory#add_submenu "_Compile" in
3003
let externals_factory = new GMenu.factory externals_menu
3004
~accel_path:"<CoqIde MenuBar>/Compile/"
3009
(* Command/Compile Menu *)
3011
let v = get_current_view () in
3012
let av = Option.get v.analyzed_view in
3014
match av#filename with
3016
!flash_info "Active buffer has no name"
3018
let cmd = !current.cmd_coqc ^ " -I "
3019
^ (Filename.quote (Filename.dirname f))
3020
^ " " ^ (Filename.quote f) in
3021
let s,res = run_command av#insert_message cmd in
3022
if s = Unix.WEXITED 0 then
3023
!flash_info (f ^ " successfully compiled")
3025
!flash_info (f ^ " failed to compile");
3026
activate_input (notebook ())#current_page;
3027
av#process_until_end_or_error;
3028
av#insert_message "Compilation output:\n";
3029
av#insert_message res
3033
externals_factory#add_item "_Compile Buffer" ~callback:compile_f
3036
(* Command/Make Menu *)
3038
let v = get_current_view () in
3039
let av = Option.get v.analyzed_view in
3040
match av#filename with
3042
!flash_info "Cannot make: this buffer has no name"
3045
"cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^ !current.cmd_make in
3050
av#insert_message "Command output:\n";
3051
let s,res = run_command av#insert_message cmd in
3053
last_make_index := 0;
3054
!flash_info (!current.cmd_make ^ if s = Unix.WEXITED 0 then " succeeded" else " failed")
3056
let _ = externals_factory#add_item "_Make"
3062
(* Compile/Next Error *)
3065
let file,line,start,stop,error_msg = search_next_error () in
3067
let v = get_current_view () in
3068
let av = Option.get v.analyzed_view in
3069
let input_buffer = v.view#buffer in
3071
let init = input_buffer#start_iter in
3072
let i = init#forward_lines (line-1) in
3075
let convert_pos = byte_offset_to_char_offset phrase in
3076
let start = convert_pos start in
3077
let stop = convert_pos stop in
3080
let starti = i#forward_chars start in
3081
let stopi = i#forward_chars stop in
3083
let starti = input_buffer#get_iter_at_byte ~line:(line-1) start in
3084
let stopi = input_buffer#get_iter_at_byte ~line:(line-1) stop in
3085
input_buffer#apply_tag_by_name "error"
3088
input_buffer#place_cursor starti;
3089
av#set_message error_msg;
3090
v.view#misc#grab_focus ()
3092
last_make_index := 0;
3093
let v = get_current_view () in
3094
let av = Option.get v.analyzed_view in
3095
av#set_message "No more errors.\n"
3098
externals_factory#add_item "_Next error"
3100
~callback:next_error in
3103
(* Command/CoqMakefile Menu*)
3104
let coq_makefile_f () =
3105
let v = get_current_view () in
3106
let av = Option.get v.analyzed_view in
3107
match av#filename with
3109
!flash_info "Cannot make makefile: this buffer has no name"
3112
"cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^ !current.cmd_coqmakefile in
3113
let s,res = run_command av#insert_message cmd in
3115
(!current.cmd_coqmakefile ^ if s = Unix.WEXITED 0 then " succeeded" else " failed")
3117
let _ = externals_factory#add_item "_Make makefile" ~callback:coq_makefile_f
3120
let configuration_menu = factory#add_submenu "_Windows" in
3121
let configuration_factory = new GMenu.factory configuration_menu
3122
~accel_path:"<CoqIde MenuBar>/Windows"
3127
configuration_factory#add_item
3128
"Show/Hide _Query Pane"
3129
~key:GdkKeysyms._Escape
3130
~callback:(fun () -> if (Command_windows.command_window ())#frame#misc#visible then
3131
(Command_windows.command_window ())#frame#misc#hide ()
3133
(Command_windows.command_window ())#frame#misc#show ())
3136
configuration_factory#add_check_item
3137
"Show/Hide _Toolbar"
3139
!current.show_toolbar <- not !current.show_toolbar;
3140
!show_toolbar !current.show_toolbar)
3142
let _ = configuration_factory#add_item
3143
"Detach _Script Window"
3145
(do_if_not_computing "detach script window" (sync
3147
let nb = notebook () in
3148
if nb#misc#toplevel#get_oid=w#coerce#get_oid then
3150
let nw = GWindow.window
3151
~width:(!current.window_width*2/3)
3152
~height:(!current.window_height*2/3)
3158
let parent = Option.get nb#misc#parent in
3159
ignore (nw#connect#destroy
3161
(fun () -> nb#misc#reparent parent));
3162
nw#add_accel_group accel_group;
3163
nb#misc#reparent nw#coerce
3167
(* let _ = configuration_factory#add_item
3168
"Detach _Command Pane"
3170
(do_if_not_computing "detach command pane" (sync
3172
let command_object = Command_windows.command_window() in
3173
let queries_frame = command_object#frame in
3174
if queries_frame#misc#toplevel#get_oid=w#coerce#get_oid then
3176
let nw = GWindow.window
3177
~width:(!current.window_width*2/3)
3178
~height:(!current.window_height*2/3)
3184
let parent = Option.get queries_frame#misc#parent in
3185
ignore (nw#connect#destroy
3187
(fun () -> queries_frame#misc#reparent parent));
3188
queries_frame#misc#show();
3189
queries_frame#misc#reparent nw#coerce
3195
configuration_factory#add_item
3198
(do_if_not_computing "detach view"
3200
match get_current_view () with
3201
| {view=v;analyzed_view=Some av} ->
3202
let w = GWindow.window ~show:true
3203
~width:(!current.window_width*2/3)
3204
~height:(!current.window_height*2/3)
3206
~title:(match av#filename with
3207
| None -> "*Unnamed*"
3211
let sb = GBin.scrolled_window
3221
ignore (w#connect#destroy
3223
(fun () -> av#remove_detached_view w));
3224
av#add_detached_view w
3231
let help_menu = factory#add_submenu "_Help" in
3232
let help_factory = new GMenu.factory help_menu
3233
~accel_path:"<CoqIde MenuBar>/Help/"
3236
let _ = help_factory#add_item "Browse Coq _Manual"
3239
let av = Option.get ((get_current_view ()).analyzed_view) in
3240
browse av#insert_message (!current.doc_url)) in
3241
let _ = help_factory#add_item "Browse Coq _Library"
3244
let av = Option.get ((get_current_view ()).analyzed_view) in
3245
browse av#insert_message !current.library_url) in
3247
help_factory#add_item "Help for _keyword" ~key:GdkKeysyms._F1
3248
~callback:(fun () ->
3249
let av = Option.get ((get_current_view ()).analyzed_view) in
3250
av#help_for_keyword ())
3252
let _ = help_factory#add_separator () in
3254
let faq_m = help_factory#add_item "_FAQ" in
3256
let about_m = help_factory#add_item "_About" in
3259
(* The vertical Separator between Scripts and Goals *)
3260
let queries_pane = GPack.paned `VERTICAL ~packing:(vbox#pack ~expand:true ) () in
3261
let hb = GPack.paned `HORIZONTAL ~border_width:5 ~packing:(queries_pane#pack1 ~shrink:false ~resize:true) () in
3262
let fr_notebook = GBin.frame ~shadow_type:`IN ~packing:hb#add1 () in
3263
_notebook := Some (GPack.notebook ~border_width:2 ~show_border:false ~scrollable:true
3264
~packing:fr_notebook#add
3266
update_notebook_pos ();
3267
let nb = notebook () in
3268
let hb2 = GPack.paned `VERTICAL ~packing:hb#add2 () in
3269
let fr_a = GBin.frame ~shadow_type:`IN ~packing:hb2#add () in
3270
let fr_b = GBin.frame ~shadow_type:`IN ~packing:hb2#add () in
3271
let sw2 = GBin.scrolled_window
3274
~packing:(fr_a#add) () in
3275
let sw3 = GBin.scrolled_window
3278
~packing:(fr_b#add) () in
3279
let command_object = Command_windows.command_window() in
3280
let queries_frame = command_object#frame in
3281
queries_pane#pack2 ~shrink:false ~resize:false (queries_frame#coerce);
3282
let lower_hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in
3283
let status_bar = GMisc.statusbar ~packing:(lower_hbox#pack ~expand:true) ()
3285
let search_lbl = GMisc.label ~text:"Search:"
3287
~packing:(lower_hbox#pack ~expand:false) ()
3289
let search_history = ref [] in
3290
let search_input = GEdit.combo ~popdown_strings:!search_history
3291
~enable_arrow_keys:true
3293
~packing:(lower_hbox#pack ~expand:false) ()
3295
search_input#disable_activate ();
3296
let ready_to_wrap_search = ref false in
3298
let start_of_search = ref None in
3299
let start_of_found = ref None in
3300
let end_of_found = ref None in
3301
let search_forward = ref true in
3302
let matched_word = ref None in
3304
let memo_search () =
3305
matched_word := Some search_input#entry#text
3307
(* if not (List.mem search_input#entry#text !search_history) then
3309
search_input#entry#text::!search_history;
3310
search_input#set_popdown_strings !search_history);
3311
start_of_search := None;
3312
ready_to_wrap_search := false
3317
prerr_endline "End Search";
3319
let v = (get_current_view ()).view in
3320
v#buffer#move_mark `SEL_BOUND (v#buffer#get_iter_at_mark `INSERT);
3321
v#coerce#misc#grab_focus ();
3322
search_input#entry#set_text "";
3323
search_lbl#misc#hide ();
3324
search_input#misc#hide ()
3326
let end_search_focus_out () =
3327
prerr_endline "End Search(focus out)";
3329
let v = (get_current_view ()).view in
3330
v#buffer#move_mark `SEL_BOUND (v#buffer#get_iter_at_mark `INSERT);
3331
search_input#entry#set_text "";
3332
search_lbl#misc#hide ();
3333
search_input#misc#hide ()
3335
ignore (search_input#entry#connect#activate ~callback:end_search);
3336
ignore (search_input#entry#event#connect#key_press
3337
~callback:(fun k -> let kv = GdkEvent.Key.keyval k in
3339
kv = GdkKeysyms._Right
3340
|| kv = GdkKeysyms._Up
3341
|| kv = GdkKeysyms._Left
3342
|| (kv = GdkKeysyms._g
3343
&& (List.mem `CONTROL (GdkEvent.Key.state k)))
3346
ignore (search_input#entry#event#connect#focus_out
3347
~callback:(fun _ -> end_search_focus_out (); false));
3348
to_do_on_page_switch :=
3350
start_of_search := None;
3351
ready_to_wrap_search:=false)::!to_do_on_page_switch;
3353
(* TODO : make it work !!! *)
3354
let rec search_f () =
3355
search_lbl#misc#show ();
3356
search_input#misc#show ();
3358
prerr_endline "search_f called";
3359
if !start_of_search = None then begin
3360
(* A full new search is starting *)
3362
Some ((get_current_view ()).view#buffer#create_mark
3363
((get_current_view ()).view#buffer#get_iter_at_mark `INSERT));
3364
start_of_found := !start_of_search;
3365
end_of_found := !start_of_search;
3366
matched_word := Some "";
3368
let txt = search_input#entry#text in
3369
let v = (get_current_view ()).view in
3370
let iit = v#buffer#get_iter_at_mark `SEL_BOUND
3371
and insert_iter = v#buffer#get_iter_at_mark `INSERT
3373
prerr_endline ("SELBOUND="^(string_of_int iit#offset));
3374
prerr_endline ("INSERT="^(string_of_int insert_iter#offset));
3377
if !search_forward then iit#forward_search txt
3378
else let npi = iit#forward_chars (Glib.Utf8.length txt) in
3380
(npi#offset = (v#buffer#get_iter_at_mark `INSERT)#offset),
3381
(let t = iit#get_text ~stop:npi in
3382
!flash_info (t^"\n"^txt);
3386
(!flash_info "T,T";iit#backward_search txt)
3387
| false,true -> !flash_info "F,T";Some (iit,npi)
3389
(iit#backward_search txt)
3393
if !ready_to_wrap_search then begin
3394
ready_to_wrap_search := false;
3395
!flash_info "Search wrapped";
3396
v#buffer#place_cursor
3397
(if !search_forward then v#buffer#start_iter else
3401
if !search_forward then !flash_info "Search at end"
3402
else !flash_info "Search at start";
3403
ready_to_wrap_search := true
3405
| Some (start,stop) ->
3406
prerr_endline "search: before moving marks";
3407
prerr_endline ("SELBOUND="^(string_of_int (v#buffer#get_iter_at_mark `SEL_BOUND)#offset));
3408
prerr_endline ("INSERT="^(string_of_int (v#buffer#get_iter_at_mark `INSERT)#offset));
3410
v#buffer#move_mark `SEL_BOUND start;
3411
v#buffer#move_mark `INSERT stop;
3412
prerr_endline "search: after moving marks";
3413
prerr_endline ("SELBOUND="^(string_of_int (v#buffer#get_iter_at_mark `SEL_BOUND)#offset));
3414
prerr_endline ("INSERT="^(string_of_int (v#buffer#get_iter_at_mark `INSERT)#offset));
3415
v#scroll_to_mark `SEL_BOUND
3418
ignore (search_input#entry#event#connect#key_release
3421
if GdkEvent.Key.keyval ev = GdkKeysyms._Escape then begin
3422
let v = (get_current_view ()).view in
3423
(match !start_of_search with
3425
prerr_endline "search_key_rel: Placing sel_bound";
3428
(v#buffer#get_iter_at_mark `INSERT)
3429
| Some mk -> let it = v#buffer#get_iter_at_mark
3431
prerr_endline "search_key_rel: Placing cursor";
3432
v#buffer#place_cursor it;
3433
start_of_search := None
3435
search_input#entry#set_text "";
3436
v#coerce#misc#grab_focus ();
3440
ignore (search_input#entry#connect#changed search_f);
3443
ignore (search_if#connect#activate
3445
search_forward:= true;
3446
search_input#entry#coerce#misc#grab_focus ();
3450
ignore (search_ib#connect#activate
3452
search_forward:= false;
3454
(* Must restore the SEL_BOUND mark after
3456
let v = (get_current_view ()).view in
3457
let old_sel = v#buffer#get_iter_at_mark `SEL_BOUND
3459
search_input#entry#coerce#misc#grab_focus ();
3460
v#buffer#move_mark `SEL_BOUND old_sel;
3464
let status_context = status_bar#new_context "Messages" in
3465
let flash_context = status_bar#new_context "Flash" in
3466
ignore (status_context#push "Ready");
3467
status := Some status_bar;
3468
push_info := (fun s -> ignore (status_context#push s));
3469
pop_info := (fun () -> status_context#pop ());
3470
flash_info := (fun ?(delay=5000) s -> flash_context#flash ~delay s);
3472
(* Location display *)
3474
~text:"Line: 1 Char: 1"
3475
~packing:lower_hbox#pack () in
3476
l#coerce#misc#set_name "location";
3477
set_location := l#set_text;
3481
(let pb = GRange.progress_bar ~pulse_step:0.2 ~packing:lower_hbox#pack ()
3482
in pb#set_text "CoqIde started";pb)#pulse;
3483
let tv2 = GText.view ~packing:(sw2#add) () in
3484
tv2#misc#set_name "GoalWindow";
3485
let _ = tv2#set_editable false in
3486
let _ = tv2#buffer in
3487
let tv3 = GText.view ~packing:(sw3#add) () in
3488
tv2#misc#set_name "MessageWindow";
3489
let _ = tv2#set_wrap_mode `CHAR in
3490
let _ = tv3#set_wrap_mode `WORD in
3491
let _ = tv3#set_editable false in
3492
let _ = GtkBase.Widget.add_events tv2#as_widget
3493
[`ENTER_NOTIFY;`POINTER_MOTION] in
3495
tv2#event#connect#motion_notify
3498
let win = match tv2#get_window `WIDGET with
3499
| None -> assert false
3501
let x,y = Gdk.Window.get_pointer_location win in
3502
let b_x,b_y = tv2#window_to_buffer_coords ~tag:`WIDGET ~x ~y in
3503
let it = tv2#get_iter_at_location ~x:b_x ~y:b_y in
3504
let tags = it#tags in
3507
ignore(GtkText.Tag.event t#as_tag tv2#as_widget e it#as_iter))
3512
tv2#misc#modify_font fd;
3513
tv3#misc#modify_font fd;
3515
(fun {view=view} -> view#misc#modify_font fd)
3518
let about_full_string =
3519
"\nCoq is developed by the Coq Development Team\
3520
\n(INRIA - CNRS - University Paris 11 and partners)\
3521
\nWeb site: " ^ Coq_config.wwwcoq ^
3522
"\nFeature wish or bug report: http://logical.saclay.inria.fr/coq-bugs\
3524
\nCredits for CoqIDE, the Integrated Development Environment for Coq:\
3526
\nMain author : Benjamin Monate\
3527
\nContributors : Jean-Christophe Filliâtre\
3528
\n Pierre Letouzey, Claude Marché\
3529
\n Bruno Barras, Pierre Corbineau\
3530
\n Julien Narboux, Hugo Herbelin, ... \
3532
\nVersion information\
3533
\n-------------------\
3536
let initial_about (b:GText.buffer) =
3537
let initial_string = "Welcome to CoqIDE, an Integrated Development Environment for Coq\n" in
3538
let coq_version = Coq.short_version () in
3539
b#insert ~iter:b#start_iter "\n\n";
3540
if Glib.Utf8.validate ("You are running " ^ coq_version) then b#insert ~iter:b#start_iter ("You are running " ^ coq_version);
3541
if Glib.Utf8.validate initial_string then b#insert ~iter:b#start_iter initial_string;
3543
let image = lib_ide_file "coq.png" in
3544
let startup_image = GdkPixbuf.from_file image in
3545
b#insert ~iter:b#start_iter "\n\n";
3546
b#insert_pixbuf ~iter:b#start_iter ~pixbuf:startup_image;
3547
b#insert ~iter:b#start_iter "\n\n\t\t "
3551
let about (b:GText.buffer) =
3553
let image = lib_ide_file "coq.png" in
3554
let startup_image = GdkPixbuf.from_file image in
3555
b#insert ~iter:b#start_iter "\n\n";
3556
b#insert_pixbuf ~iter:b#start_iter ~pixbuf:startup_image;
3557
b#insert ~iter:b#start_iter "\n\n\t\t "
3559
if Glib.Utf8.validate about_full_string
3560
then b#insert about_full_string;
3561
let coq_version = Coq.version () in
3562
if Glib.Utf8.validate coq_version
3563
then b#insert coq_version
3566
initial_about tv2#buffer;
3567
w#add_accel_group accel_group;
3568
(* Remove default pango menu for textviews *)
3569
ignore (tv2#event#connect#button_press ~callback:
3570
(fun ev -> GdkEvent.Button.button ev = 3));
3571
ignore (tv3#event#connect#button_press ~callback:
3572
(fun ev -> GdkEvent.Button.button ev = 3));
3573
tv2#misc#set_can_focus true;
3574
tv3#misc#set_can_focus true;
3575
ignore (tv2#buffer#create_mark
3576
~name:"end_of_conclusion"
3577
tv2#buffer#start_iter);
3578
ignore (tv3#buffer#create_tag
3580
[`FOREGROUND "red"]);
3582
message_view := Some tv3;
3583
proof_view := Some tv2;
3584
tv2#misc#modify_font !current.text_font;
3585
tv3#misc#modify_font !current.text_font;
3586
ignore (about_m#connect#activate
3587
~callback:(fun () -> tv2#buffer#set_text ""; about tv2#buffer));
3589
ignore (faq_m#connect#activate
3590
~callback:(fun () ->
3591
load (lib_ide_file "FAQ")));
3594
resize_window := (fun () ->
3596
~width:!current.window_width
3597
~height:!current.window_height);
3599
ignore (w#misc#connect#size_allocate
3601
and old_h = ref 0 in
3602
fun {Gtk.width=w;Gtk.height=h} ->
3603
if !old_w <> w or !old_h <> h then
3607
hb#set_position (w/2);
3608
hb2#set_position (h/2);
3609
!current.window_height <- h;
3610
!current.window_width <- w;
3613
ignore(nb#connect#switch_page
3616
prerr_endline ("switch_page: starts " ^ string_of_int i);
3617
List.iter (function f -> f i) !to_do_on_page_switch;
3618
prerr_endline "switch_page: success")
3620
ignore(tv2#event#connect#enter_notify
3622
if !current.contextual_menus_on_goal then
3624
let w = (Option.get (get_active_view ()).analyzed_view) in
3625
!push_info "Computing advanced goal's menus";
3626
prerr_endline "Entering Goal Window. Computing Menus....";
3628
prerr_endline "....Done with Goal menu";
3633
if List.length files >=1 then
3636
if Sys.file_exists f then load f else
3637
let f = if Filename.check_suffix f ".v" then f else f^".v" in
3638
load_file (fun s -> print_endline s; exit 1) f)
3644
let view = create_input_tab "*Unnamed Buffer*" in
3645
let index = add_input_view {view = view;
3646
analyzed_view = None;
3649
(get_input_view index).analyzed_view <- Some (new analyzed_view index);
3650
activate_input index;
3651
set_tab_image index ~icon:`YES;
3652
view#misc#modify_font !current.text_font
3657
(* This function check every half of second if GeoProof has send
3658
something on his private clipboard *)
3660
let rec check_for_geoproof_input () =
3661
let cb_Dr = GData.clipboard (Gdk.Atom.intern "_GeoProof") in
3664
let s = cb_Dr#text in
3668
(get_current_view()).view#buffer#insert (s^"\n");
3669
cb_Dr#set_text "Ack"
3672
(* cb_Dr#clear does not work so i use : *)
3673
(* cb_Dr#set_text "Ack" *)
3678
let files = Coq.init () in
3680
GtkMain.Rc.add_default_file (lib_ide_file ".coqide-gtk2rc");
3682
GtkMain.Rc.add_default_file (Filename.concat System.home ".coqide-gtk2rc");
3683
with Not_found -> ());
3684
ignore (GtkMain.Main.init ());
3685
GtkData.AccelGroup.set_default_mod_mask
3686
(Some [`CONTROL;`SHIFT;`MOD1;`MOD3;`MOD4]);
3687
cb_ := Some (GData.clipboard Gdk.Atom.primary);
3689
Glib.Message.set_log_handler ~domain:"Gtk" ~levels:[`ERROR;`FLAG_FATAL;
3692
if level land Glib.Message.log_level `WARNING <> 0
3694
else failwith ("Coqide internal error: " ^ msg)));
3695
Command_windows.main ();
3696
Blaster_window.main 9;
3699
if !Coq_config.with_geoproof then ignore (Thread.create check_for_geoproof_input ());
3704
| Sys.Break -> prerr_endline "Interrupted." ; flush stderr
3706
Pervasives.prerr_endline ("CoqIde unexpected error:" ^ (Printexc.to_string e));
added
removed
ide/coqide.ml
