summaryrefslogtreecommitdiff
path: root/ide/coqide.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/coqide.ml')
-rw-r--r--ide/coqide.ml3386
1 files changed, 3386 insertions, 0 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
new file mode 100644
index 00000000..2169862e
--- /dev/null
+++ b/ide/coqide.ml
@@ -0,0 +1,3386 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id: coqide.ml,v 1.99.2.2 2004/07/18 11:20:15 herbelin Exp $ *)
+
+open Preferences
+open Vernacexpr
+open Coq
+open Ideutils
+
+let out_some s = match s with
+ | None -> failwith "Internal error in out_some" | Some f -> f
+
+let cb_ = ref None
+let cb () = ((out_some !cb_):GData.clipboard)
+let last_cb_content = ref ""
+
+let (message_view:GText.view option ref) = ref None
+let (proof_view:GText.view option ref) = ref None
+
+let (_notebook:GPack.notebook option ref) = ref None
+let notebook () = out_some !_notebook
+
+
+(* Tabs contain the name of the edited file and 2 status informations:
+ Saved state + Focused proof buffer *)
+let decompose_tab w =
+ let vbox = new GPack.box ((Gobject.try_cast w "GtkBox"):Gtk.box Gtk.obj) in
+ let l = vbox#children in
+ match l with
+ | [img;lbl] ->
+ let img = new GMisc.image
+ ((Gobject.try_cast img#as_widget "GtkImage"):
+ Gtk.image Gtk.obj)
+ in
+ let lbl = GMisc.label_cast lbl in
+ vbox,img,lbl
+ | _ -> assert false
+
+let set_tab_label i n =
+ let nb = notebook () in
+ let _,_,lbl = decompose_tab (nb#get_tab_label(nb#get_nth_page i))#as_widget
+ in
+ lbl#set_use_markup true;
+ (* lbl#set_text n *) lbl#set_label n
+
+
+let set_tab_image ~icon i =
+ let nb = notebook () in
+ let _,img,_ = decompose_tab (nb#get_tab_label(nb#get_nth_page i))#as_widget
+ in
+ img#set_icon_size `SMALL_TOOLBAR;
+ img#set_stock icon
+
+let set_current_tab_image ~icon = set_tab_image ~icon (notebook())#current_page
+
+let set_current_tab_label n = set_tab_label (notebook())#current_page n
+
+let get_tab_label i =
+ let nb = notebook () in
+ let _,_,lbl = decompose_tab (nb#get_tab_label(nb#get_nth_page i))#as_widget
+ in
+ lbl#text
+
+let get_full_tab_label i =
+ let nb = notebook () in
+ let _,_,lbl = decompose_tab (nb#get_tab_label(nb#get_nth_page i))#as_widget
+ in
+ lbl
+
+let get_current_tab_label () = get_tab_label (notebook())#current_page
+
+let get_current_page () =
+ let i = (notebook())#current_page in
+ (notebook())#get_nth_page i
+
+(* This function must remove "focused proof" decoration *)
+let reset_tab_label i =
+ set_tab_label i (get_tab_label i)
+
+let to_do_on_page_switch = ref []
+
+module Vector = struct
+ exception Found of int
+ type 'a t = ('a option) array ref
+ let create () = ref [||]
+ let length t = Array.length !t
+ let get t i = out_some (Array.get !t i)
+ let set t i v = Array.set !t i (Some v)
+ let remove t i = Array.set !t i None
+ let append t e = t := Array.append !t [|Some e|]; (Array.length !t)-1
+ let iter f t = Array.iter (function | None -> () | Some x -> f x) !t
+ let find_or_fail f t =
+ let test i = function | None -> () | Some e -> if f e then raise (Found i) in
+ Array.iteri test t
+
+ let exists f t =
+ let l = Array.length !t in
+ let rec test i =
+ (i < l) && (((!t.(i) <> None) && f (out_some !t.(i))) || test (i+1))
+ in
+ test 0
+end
+
+type 'a viewable_script =
+ {view : Undo.undoable_view;
+ mutable analyzed_view : 'a option;
+ }
+
+
+class type analyzed_views=
+object('self)
+ val mutable act_id : GtkSignal.id option
+ val current_all : 'self viewable_script
+ val mutable deact_id : GtkSignal.id option
+ val input_buffer : GText.buffer
+ val input_view : Undo.undoable_view
+ val last_array : string array
+ val mutable last_index : bool
+ val message_buffer : GText.buffer
+ val message_view : GText.view
+ val proof_buffer : GText.buffer
+ val proof_view : GText.view
+ val mutable is_active : bool
+ val mutable read_only : bool
+ val mutable filename : string option
+ val mutable stats : Unix.stats option
+ val mutable detached_views : GWindow.window list
+ method without_auto_complete : 'a 'b. ('a -> 'b) -> 'a -> 'b
+ method set_auto_complete : bool -> unit
+
+ method kill_detached_views : unit -> unit
+ method add_detached_view : GWindow.window -> unit
+ method remove_detached_view : GWindow.window -> unit
+
+ method view : Undo.undoable_view
+ method filename : string option
+ method stats : Unix.stats option
+ method set_filename : string option -> unit
+ method update_stats : unit
+ method revert : unit
+ method auto_save : unit
+ method save : string -> bool
+ method save_as : string -> bool
+ method read_only : bool
+ method set_read_only : bool -> unit
+ method is_active : bool
+ method activate : unit -> unit
+ method active_keypress_handler : GdkEvent.Key.t -> bool
+ method backtrack_to : GText.iter -> unit
+ method backtrack_to_no_lock : GText.iter -> unit
+ method clear_message : unit
+ method deactivate : unit -> unit
+ method disconnected_keypress_handler : GdkEvent.Key.t -> bool
+ method electric_handler : GtkSignal.id
+ method find_phrase_starting_at :
+ GText.iter -> (GText.iter * GText.iter) option
+ method get_insert : GText.iter
+ method get_start_of_input : GText.iter
+ method go_to_insert : unit
+ method indent_current_line : unit
+ method insert_command : string -> string -> unit
+ method tactic_wizard : string list -> unit
+ method insert_message : string -> unit
+ method insert_this_phrase_on_success :
+ bool -> bool -> bool -> string -> string -> bool
+ method process_next_phrase : bool -> bool -> bool -> bool
+ method process_until_iter_or_error : GText.iter -> unit
+ method process_until_end_or_error : unit
+ method recenter_insert : unit
+ method reset_initial : unit
+ method send_to_coq :
+ bool -> bool -> string ->
+ bool -> bool -> bool -> (Util.loc * Vernacexpr.vernac_expr) option
+ method set_message : string -> unit
+ method show_goals : unit
+ method show_goals_full : unit
+ method undo_last_step : unit
+ method help_for_keyword : unit -> unit
+ method complete_at_offset : int -> bool
+
+ method blaster : unit -> unit
+end
+
+let (input_views:analyzed_views viewable_script Vector.t) = Vector.create ()
+
+
+let signals_to_crash = [Sys.sigabrt; Sys.sigalrm; Sys.sigfpe; Sys.sighup;
+ Sys.sigill; Sys.sigpipe; Sys.sigquit;
+ (* Sys.sigsegv; Sys.sigterm;*) Sys.sigusr2]
+
+let crash_save i =
+(* ignore (Unix.sigprocmask Unix.SIG_BLOCK signals_to_crash);*)
+ Pervasives.prerr_endline "Trying to save all buffers in .crashcoqide files";
+ let count = ref 0 in
+ Vector.iter
+ (function {view=view; analyzed_view = Some av } ->
+ (let filename = match av#filename with
+ | None ->
+ incr count;
+ "Unnamed_coqscript_"^(string_of_int !count)^".crashcoqide"
+ | Some f -> f^".crashcoqide"
+ in
+ try
+ if try_export filename (view#buffer#get_text ()) then
+ Pervasives.prerr_endline ("Saved "^filename)
+ else Pervasives.prerr_endline ("Could not save "^filename)
+ with _ -> Pervasives.prerr_endline ("Could not save "^filename))
+ | _ -> Pervasives.prerr_endline "Unanalyzed view found. Please report."
+ )
+ input_views;
+ Pervasives.prerr_endline "Done. Please report.";
+ if i <> 127 then exit i
+
+let ignore_break () =
+ List.iter
+ (fun i ->
+ try Sys.set_signal i (Sys.Signal_handle crash_save)
+ with _ -> prerr_endline "Signal ignored (normal if Win32)")
+ signals_to_crash;
+ Sys.set_signal Sys.sigint Sys.Signal_ignore
+
+(* Locking machinery for Coq kernel *)
+let coq_computing = Mutex.create ()
+
+(* To prevent Coq from interrupting during undoing...*)
+let coq_may_stop = Mutex.create ()
+
+let break () =
+ prerr_endline "User break received:";
+ if not (Mutex.try_lock coq_computing) then
+ begin
+ prerr_endline " trying to stop computation:";
+ if Mutex.try_lock coq_may_stop then begin
+ Util.interrupt := true;
+ prerr_endline " interrupt flag set. Computation should stop soon...";
+ Mutex.unlock coq_may_stop
+ end else prerr_endline " interruption refused (may not stop now)";
+ end
+ else begin
+ Mutex.unlock coq_computing;
+ prerr_endline " ignored (not computing)"
+ end
+
+let full_do_if_not_computing text f x =
+ ignore
+ (Thread.create
+ (async
+ (fun () ->
+ if Mutex.try_lock coq_computing
+ then
+ begin
+ prerr_endline ("Launching thread " ^ text);
+ let w = Blaster_window.blaster_window () in
+ if not (Mutex.try_lock w#lock) then begin
+ break ();
+ let lck = Mutex.create () in
+ Mutex.lock lck;
+ prerr_endline "Waiting on blaster...";
+ Condition.wait w#blaster_killed lck;
+ prerr_endline "Waiting on blaster ok";
+ Mutex.unlock lck
+ end else Mutex.unlock w#lock;
+ let idle =
+ Glib.Timeout.add ~ms:300
+ ~callback:(fun () -> !pulse ();true) in
+ begin
+ prerr_endline "Getting lock";
+ try
+ f x;
+ Glib.Timeout.remove idle;
+ prerr_endline "Releasing lock";
+ Mutex.unlock coq_computing;
+ with e ->
+ Glib.Timeout.remove idle;
+ prerr_endline "Releasing lock (on error)";
+ Mutex.unlock coq_computing;
+ raise e
+ end
+ end
+ else
+ prerr_endline
+ "Discarded order (computations are ongoing)"))
+ ())
+
+let do_if_not_computing text f x =
+ ignore (full_do_if_not_computing text f x)
+
+
+let add_input_view tv =
+ Vector.append input_views tv
+
+let get_input_view i =
+ if 0 <= i && i < Vector.length input_views
+ then
+ Vector.get input_views i
+ else raise Not_found
+
+let active_view = ref None
+
+let get_active_view () = Vector.get input_views (out_some !active_view)
+
+let set_active_view i =
+ (match !active_view with None -> () | Some i ->
+ reset_tab_label i);
+ (notebook ())#goto_page i;
+ let txt = get_current_tab_label () in
+ set_current_tab_label ("<span background=\"light green\">"^txt^"</span>");
+ active_view := Some i
+
+let set_current_view i = (notebook ())#goto_page i
+
+let kill_input_view i =
+ let v = Vector.get input_views i in
+ (match v.analyzed_view with
+ | Some v -> v#kill_detached_views ()
+ | None -> ());
+ v.view#destroy ();
+ v.analyzed_view <- None;
+ Vector.remove input_views i
+
+let get_current_view_page () = (notebook ())#current_page
+let get_current_view () = Vector.get input_views (notebook ())#current_page
+let remove_current_view_page () =
+ let c = (notebook ())#current_page in
+ kill_input_view c;
+ ((notebook ())#get_nth_page c)#misc#hide ()
+
+
+let is_word_char c =
+ Glib.Unichar.isalnum c || c = underscore || c = prime || c = arobase
+
+let starts_word it =
+ prerr_endline ("Starts word ? '"^(Glib.Utf8.from_unichar it#char)^"'");
+ (not it#copy#nocopy#backward_char ||
+ (let c = it#backward_char#char in
+ not (is_word_char c)))
+
+let ends_word it =
+ (not it#copy#nocopy#forward_char ||
+ let c = it#forward_char#char in
+ not (Glib.Unichar.isalnum c || c = underscore || c = prime || c = arobase)
+ )
+
+let inside_word it =
+ let c = it#char in
+ not (starts_word it) &&
+ not (ends_word it) &&
+ (Glib.Unichar.isalnum c || c = underscore || c = prime || c = arobase)
+
+let is_on_word_limit it = inside_word it || ends_word it
+
+let rec find_word_start it =
+ prerr_endline "Find word start";
+ if not it#nocopy#backward_char then
+ (prerr_endline "find_word_start: cannot backward"; it)
+ else if is_word_char it#char
+ then find_word_start it
+ else (it#nocopy#forward_char;
+ prerr_endline ("Word start at: "^(string_of_int it#offset));it)
+let find_word_start (it:GText.iter) = find_word_start it#copy
+
+let rec find_word_end it =
+ prerr_endline "Find word end";
+ if let c = it#char in c<>0 && is_word_char c
+ then begin
+ ignore (it#nocopy#forward_char);
+ find_word_end it
+ end else (prerr_endline ("Word end at: "^(string_of_int it#offset));it)
+let find_word_end it = find_word_end it#copy
+
+
+let get_word_around it =
+ let start = find_word_start it in
+ let stop = find_word_end it in
+ start,stop
+
+
+let rec complete_backward w (it:GText.iter) =
+ prerr_endline "Complete backward...";
+ match it#backward_search w with
+ | None -> (prerr_endline "backward_search failed";None)
+ | Some (start,stop) ->
+ prerr_endline ("complete_backward got a match:"^(string_of_int start#offset)^(string_of_int stop#offset));
+ if starts_word start then
+ let ne = find_word_end stop in
+ if ne#compare stop = 0
+ then complete_backward w start
+ else Some (start,stop,ne)
+ else complete_backward w start
+
+let rec complete_forward w (it:GText.iter) =
+ prerr_endline "Complete forward...";
+ match it#forward_search w with
+ | None -> None
+ | Some (start,stop) ->
+ if starts_word start then
+ let ne = find_word_end stop in
+ if ne#compare stop = 0 then
+ complete_forward w stop
+ else Some (stop,stop,ne)
+ else complete_forward w stop
+
+(* Reset this to None on page change ! *)
+let (last_completion:(string*int*int*bool) option ref) = ref None
+
+let () = to_do_on_page_switch :=
+ (fun i -> last_completion := None)::!to_do_on_page_switch
+
+let rec complete input_buffer w (offset:int) =
+ match !last_completion with
+ | Some (lw,loffset,lpos,backward)
+ when lw=w && loffset=offset ->
+ begin
+ let iter = input_buffer#get_iter (`OFFSET lpos) in
+ if backward then
+ match complete_backward w iter with
+ | None ->
+ last_completion :=
+ Some (lw,loffset,
+ (find_word_end
+ (input_buffer#get_iter (`OFFSET loffset)))#offset ,
+ false);
+ None
+ | Some (ss,start,stop) as result ->
+ last_completion :=
+ Some (w,offset,ss#offset,true);
+ result
+ else
+ match complete_forward w iter with
+ | None ->
+ last_completion := None;
+ None
+ | Some (ss,start,stop) as result ->
+ last_completion :=
+ Some (w,offset,ss#offset,false);
+ result
+ end
+ | _ -> begin
+ match complete_backward w (input_buffer#get_iter (`OFFSET offset)) with
+ | None ->
+ last_completion :=
+ Some (w,offset,(find_word_end (input_buffer#get_iter
+ (`OFFSET offset)))#offset,false);
+ complete input_buffer w offset
+ | Some (ss,start,stop) as result ->
+ last_completion := Some (w,offset,ss#offset,true);
+ result
+ end
+
+let get_current_word () =
+ let av = out_some ((get_current_view ()).analyzed_view) in
+ match GtkBase.Clipboard.wait_for_text (cb ())#as_clipboard with
+ | None ->
+ prerr_endline "None selected";
+ let it = av#get_insert in
+ let start = find_word_start it in
+ let stop = find_word_end start in
+ av#view#buffer#move_mark `SEL_BOUND start;
+ av#view#buffer#move_mark `INSERT stop;
+ av#view#buffer#get_text ~slice:true ~start ~stop ()
+ | Some t ->
+ prerr_endline "Some selected";
+ prerr_endline t;
+ t
+
+
+let input_channel b ic =
+ let buf = String.create 1024 and len = ref 0 in
+ while len := input ic buf 0 1024; !len > 0 do
+ Buffer.add_substring b buf 0 !len
+ done
+
+let with_file name ~f =
+ let ic = open_in_gen [Open_rdonly;Open_creat] 0o644 name in
+ try f ic; close_in ic with exn ->
+ close_in ic; !flash_info ("Error: "^Printexc.to_string exn)
+
+type info = {start:GText.mark;
+ stop:GText.mark;
+ ast:Util.loc * Vernacexpr.vernac_expr;
+ reset_info:Coq.reset_info;
+ }
+
+exception Size of int
+let (processed_stack:info Stack.t) = Stack.create ()
+let push x = Stack.push x processed_stack
+let pop () = try Stack.pop processed_stack with Stack.Empty -> raise (Size 0)
+let top () = try Stack.top processed_stack with Stack.Empty -> raise (Size 0)
+let is_empty () = Stack.is_empty processed_stack
+
+
+(* push a new Coq phrase *)
+
+let update_on_end_of_proof id =
+ let lookup_lemma = function
+ | { ast = _, ( VernacDefinition (_, _, ProveBody _, _)
+ | VernacDeclareTacticDefinition _
+ | VernacStartTheoremProof _) ;
+ reset_info = Reset (_, r) } ->
+ if not !r then begin
+ prerr_endline "Toggling Reset info to true";
+ r := true; raise Exit end
+ else begin
+ prerr_endline "Toggling Changing Reset id";
+ r := false
+ end
+ | { ast = _, (VernacAbort _ | VernacAbortAll | VernacGoal _) } -> raise Exit
+ | _ -> ()
+ in
+ try Stack.iter lookup_lemma processed_stack with Exit -> ()
+
+let update_on_end_of_segment id =
+ let lookup_section = function
+ | { ast = _, ( VernacBeginSection id'
+ | VernacDefineModule (id',_,_,None)
+ | VernacDeclareModule (id',_,_,None)
+ | VernacDeclareModuleType (id',_,None));
+ reset_info = Reset (_, r) }
+ when id = id' -> raise Exit
+ | { reset_info = Reset (_, r) } -> r := false
+ | _ -> ()
+ in
+ try Stack.iter lookup_section processed_stack with Exit -> ()
+
+let push_phrase start_of_phrase_mark end_of_phrase_mark ast =
+ let x = {start = start_of_phrase_mark;
+ stop = end_of_phrase_mark;
+ ast = ast;
+ reset_info = Coq.compute_reset_info (snd ast)
+ }
+ in
+ push x;
+ match snd ast with
+ | VernacEndProof (Proved (_, None)) -> update_on_end_of_proof ()
+ | VernacEndSegment id -> update_on_end_of_segment id
+ | _ -> ()
+
+let repush_phrase x =
+ let x = { x with reset_info = Coq.compute_reset_info (snd x.ast) } in
+ push x;
+ match snd x.ast with
+ | VernacEndProof (Proved (_, None)) -> update_on_end_of_proof ()
+ | VernacEndSegment id -> update_on_end_of_segment id
+ | _ -> ()
+
+(* For electric handlers *)
+exception Found
+
+(* For find_phrase_starting_at *)
+exception Stop of int
+
+let activate_input i =
+ (match !active_view with
+ | None -> ()
+ | Some n ->
+ let a_v = out_some (Vector.get input_views n).analyzed_view in
+ a_v#deactivate ();
+ a_v#reset_initial
+ );
+ let activate_function = (out_some (Vector.get input_views i).analyzed_view)#activate in
+ activate_function ();
+ set_active_view i
+
+let warning msg =
+ GToolbox.message_box ~title:"Warning"
+ ~icon:(let img = GMisc.image () in
+ img#set_stock `DIALOG_WARNING;
+ img#set_icon_size `DIALOG;
+ img#coerce)
+ msg
+
+
+class analyzed_view index =
+ let {view = input_view_} as current_all_ = get_input_view index in
+ let proof_view_ = out_some !proof_view in
+ let message_view_ = out_some !message_view in
+object(self)
+ val current_all = current_all_
+ val input_view = current_all_.view
+ val proof_view = out_some !proof_view
+ val message_view = out_some !message_view
+ val input_buffer = input_view_#buffer
+ val proof_buffer = proof_view_#buffer
+ val message_buffer = message_view_#buffer
+ val mutable is_active = false
+ val mutable read_only = false
+ val mutable filename = None
+ val mutable stats = None
+ val mutable last_modification_time = 0.
+ val mutable last_auto_save_time = 0.
+ val mutable detached_views = []
+
+ val mutable auto_complete_on = !current.auto_complete
+
+ method private toggle_auto_complete =
+ auto_complete_on <- not auto_complete_on
+ method set_auto_complete t = auto_complete_on <- t
+ method without_auto_complete : 'a 'b. ('a -> 'b) -> 'a -> 'b = fun f x ->
+ let old = auto_complete_on in
+ self#set_auto_complete false;
+ let y = f x in
+ self#set_auto_complete old;
+ y
+ method add_detached_view (w:GWindow.window) =
+ detached_views <- w::detached_views
+ method remove_detached_view (w:GWindow.window) =
+ detached_views <- List.filter (fun e -> w#misc#get_oid<>e#misc#get_oid) detached_views
+
+ method kill_detached_views () =
+ List.iter (fun w -> w#destroy ()) detached_views;
+ detached_views <- []
+
+ method view = input_view
+ method filename = filename
+ method stats = stats
+ method set_filename f =
+ filename <- f;
+ match f with
+ | Some f -> stats <- my_stat f
+ | None -> ()
+
+ method update_stats =
+ match filename with
+ | Some f -> stats <- my_stat f
+ | _ -> ()
+
+ method revert =
+ match filename with
+ | Some f -> begin
+ let do_revert () = begin
+ !push_info "Reverting buffer";
+ try
+ if is_active then self#reset_initial;
+ let b = Buffer.create 1024 in
+ with_file f ~f:(input_channel b);
+ let s = try_convert (Buffer.contents b) in
+ input_buffer#set_text s;
+ self#update_stats;
+ input_buffer#place_cursor input_buffer#start_iter;
+ input_buffer#set_modified false;
+ !pop_info ();
+ !flash_info "Buffer reverted";
+ Highlight.highlight_all input_buffer;
+ with _ ->
+ !pop_info ();
+ !flash_info "Warning: could not revert buffer";
+ end
+ in
+ if input_buffer#modified then
+ match (GToolbox.question_box
+ ~title:"Modified buffer changed on disk"
+ ~buttons:["Revert from File";
+ "Overwrite File";
+ "Disable Auto Revert"]
+ ~default:0
+ ~icon:(stock_to_widget `DIALOG_WARNING)
+ "Some unsaved buffers changed on disk"
+ )
+ with 1 -> do_revert ()
+ | 2 -> if self#save f then !flash_info "Overwritten" else
+ !flash_info "Could not overwrite file"
+ | _ ->
+ prerr_endline "Auto revert set to false";
+ !current.global_auto_revert <- false;
+ disconnect_revert_timer ()
+ else do_revert ()
+ end
+ | None -> ()
+
+ method save f =
+ if try_export f (input_buffer#get_text ()) then begin
+ filename <- Some f;
+ input_buffer#set_modified false;
+ stats <- my_stat f;
+ (match self#auto_save_name with
+ | None -> ()
+ | Some fn -> try Sys.remove fn with _ -> ());
+ true
+ end
+ else false
+
+ method private auto_save_name =
+ match filename with
+ | None -> None
+ | Some f ->
+ let dir = Filename.dirname f in
+ let base = (fst !current.auto_save_name) ^
+ (Filename.basename f) ^
+ (snd !current.auto_save_name)
+ in Some (Filename.concat dir base)
+
+ method private need_auto_save =
+ input_buffer#modified &&
+ last_modification_time > last_auto_save_time
+
+ method auto_save =
+ if self#need_auto_save then begin
+ match self#auto_save_name with
+ | None -> ()
+ | Some fn ->
+ try
+ last_auto_save_time <- Unix.time();
+ prerr_endline ("Autosave time : "^(string_of_float (Unix.time())));
+ if try_export fn (input_buffer#get_text ()) then begin
+ !flash_info ~delay:1000 "Autosaved"
+ end
+ else warning
+ ("Autosave failed (check if " ^ fn ^ " is writable)")
+ with _ ->
+ warning ("Autosave: unexpected error while writing "^fn)
+ end
+
+ method save_as f =
+ if Sys.file_exists f then
+ match (GToolbox.question_box ~title:"File exists on disk"
+ ~buttons:["Overwrite";
+ "Cancel";]
+ ~default:1
+ ~icon:
+ (let img = GMisc.image () in
+ img#set_stock `DIALOG_WARNING;
+ img#set_icon_size `DIALOG;
+ img#coerce)
+ ("File "^f^"already exists")
+ )
+ with 1 -> self#save f
+ | _ -> false
+ else self#save f
+
+ method set_read_only b = read_only<-b
+ method read_only = read_only
+ method is_active = is_active
+ method insert_message s =
+ message_buffer#insert s;
+ message_view#misc#draw None
+
+ method set_message s =
+ message_buffer#set_text s;
+ message_view#misc#draw None
+
+ method clear_message = message_buffer#set_text ""
+ val mutable last_index = true
+ val last_array = [|"";""|]
+ method get_start_of_input = input_buffer#get_iter_at_mark (`NAME "start_of_input")
+
+ method get_insert = get_insert input_buffer
+
+ method recenter_insert =
+ (* BUG : to investigate further:
+ FIXED : Never call GMain.* in thread !
+ PLUS : GTK BUG ??? Cannot be called from a thread...
+ ADDITION: using sync instead of async causes deadlock...*)
+ ignore (GtkThread.async (
+ input_view#scroll_to_mark
+ ~use_align:false
+ ~yalign:0.75
+ ~within_margin:0.25)
+ `INSERT)
+
+
+ method indent_current_line =
+ let get_nb_space it =
+ let it = it#copy in
+ let nb_sep = ref 0 in
+ let continue = ref true in
+ while !continue do
+ if it#char = space then begin
+ incr nb_sep;
+ if not it#nocopy#forward_char then continue := false;
+ end else continue := false
+ done;
+ !nb_sep
+ in
+ let previous_line = self#get_insert in
+ if previous_line#nocopy#backward_line then begin
+ let previous_line_spaces = get_nb_space previous_line in
+ let current_line_start = self#get_insert#set_line_offset 0 in
+ let current_line_spaces = get_nb_space current_line_start in
+ if input_buffer#delete_interactive
+ ~start:current_line_start
+ ~stop:(current_line_start#forward_chars current_line_spaces)
+ ()
+ then
+ let current_line_start = self#get_insert#set_line_offset 0 in
+ input_buffer#insert
+ ~iter:current_line_start
+ (String.make previous_line_spaces ' ')
+ end
+
+
+ method show_goals =
+ try
+ proof_view#buffer#set_text "";
+ let s = Coq.get_current_goals () in
+ match s with
+ | [] -> proof_buffer#insert (Coq.print_no_goal ())
+ | (hyps,concl)::r ->
+ let goal_nb = List.length s in
+ proof_buffer#insert (Printf.sprintf "%d subgoal%s\n"
+ goal_nb
+ (if goal_nb<=1 then "" else "s"));
+ List.iter
+ (fun ((_,_,_,(s,_)) as hyp) ->
+ proof_buffer#insert (s^"\n"))
+ hyps;
+ proof_buffer#insert (String.make 38 '_' ^ "(1/"^
+ (string_of_int goal_nb)^
+ ")\n")
+ ;
+ let _,_,_,sconcl = concl in
+ proof_buffer#insert sconcl;
+ proof_buffer#insert "\n";
+ let my_mark = `NAME "end_of_conclusion" in
+ proof_buffer#move_mark
+ ~where:((proof_buffer#get_iter_at_mark `INSERT)) my_mark;
+ proof_buffer#insert "\n\n";
+ let i = ref 1 in
+ List.iter
+ (function (_,(_,_,_,concl)) ->
+ incr i;
+ proof_buffer#insert (String.make 38 '_' ^"("^
+ (string_of_int !i)^
+ "/"^
+ (string_of_int goal_nb)^
+ ")\n");
+ proof_buffer#insert concl;
+ proof_buffer#insert "\n\n";
+ )
+ r;
+ ignore (proof_view#scroll_to_mark my_mark)
+ with e -> prerr_endline ("Don't worry be happy despite: "^Printexc.to_string e)
+
+
+ val mutable full_goal_done = true
+
+ method show_goals_full =
+ if not full_goal_done then
+ begin
+ try
+ proof_view#buffer#set_text "";
+ let s = Coq.get_current_goals () in
+ let last_shown_area = proof_buffer#create_tag [`BACKGROUND "light green"]
+ in
+ match s with
+ | [] -> proof_buffer#insert (Coq.print_no_goal ())
+ | (hyps,concl)::r ->
+ let goal_nb = List.length s in
+ proof_buffer#insert (Printf.sprintf "%d subgoal%s\n"
+ goal_nb
+ (if goal_nb<=1 then "" else "s"));
+ let coq_menu commands =
+ let tag = proof_buffer#create_tag []
+ in
+ ignore
+ (tag#connect#event ~callback:
+ (fun ~origin ev it ->
+ begin match GdkEvent.get_type ev with
+ | `BUTTON_PRESS ->
+ let ev = (GdkEvent.Button.cast ev) in
+ if (GdkEvent.Button.button ev) = 3
+ then begin
+ let loc_menu = GMenu.menu () in
+ let factory = new GMenu.factory loc_menu in
+ let add_coq_command (cp,ip) =
+ ignore
+ (factory#add_item cp
+ ~callback:
+ (fun () -> ignore
+ (self#insert_this_phrase_on_success
+ true
+ true
+ false
+ ("progress "^ip^"\n")
+ (ip^"\n"))
+ )
+ )
+ in
+ List.iter add_coq_command commands;
+ loc_menu#popup
+ ~button:3
+ ~time:(GdkEvent.Button.time ev);
+ end
+ | `MOTION_NOTIFY ->
+ proof_buffer#remove_tag
+ ~start:proof_buffer#start_iter
+ ~stop:proof_buffer#end_iter
+ last_shown_area;
+ prerr_endline "Before find_tag_limits";
+
+ let s,e = find_tag_limits tag
+ (new GText.iter it)
+ in
+ prerr_endline "After find_tag_limits";
+ proof_buffer#apply_tag
+ ~start:s
+ ~stop:e
+ last_shown_area;
+
+ prerr_endline "Applied tag";
+ ()
+ | _ -> ()
+ end;false
+ )
+ );
+ tag
+ in
+ List.iter
+ (fun ((_,_,_,(s,_)) as hyp) ->
+ let tag = coq_menu (hyp_menu hyp) in
+ proof_buffer#insert ~tags:[tag] (s^"\n"))
+ hyps;
+ proof_buffer#insert
+ (String.make 38 '_' ^"(1/"^
+ (string_of_int goal_nb)^
+ ")\n")
+ ;
+ let tag = coq_menu (concl_menu concl) in
+ let _,_,_,sconcl = concl in
+ proof_buffer#insert ~tags:[tag] sconcl;
+ proof_buffer#insert "\n";
+ let my_mark = `NAME "end_of_conclusion" in
+ proof_buffer#move_mark
+ ~where:((proof_buffer#get_iter_at_mark `INSERT)) my_mark;
+ proof_buffer#insert "\n\n";
+ let i = ref 1 in
+ List.iter
+ (function (_,(_,_,_,concl)) ->
+ incr i;
+ proof_buffer#insert
+ (String.make 38 '_' ^"("^
+ (string_of_int !i)^
+ "/"^
+ (string_of_int goal_nb)^
+ ")\n");
+ proof_buffer#insert concl;
+ proof_buffer#insert "\n\n";
+ )
+ r;
+ ignore (proof_view#scroll_to_mark my_mark) ;
+ full_goal_done <- true;
+ with e -> prerr_endline (Printexc.to_string e)
+ end
+
+ method send_to_coq verbosely replace phrase show_output show_error localize =
+ try
+ full_goal_done <- false;
+ prerr_endline "Send_to_coq starting now";
+ if replace then begin
+ let r,info =
+(* full_do_if_not_computing "coq eval and replace" *)
+ Coq.interp_and_replace ("Info " ^ phrase)
+ in
+ let msg = read_stdout () in
+ self#insert_message (if show_output then msg else "");
+
+ Some r
+
+ end else begin
+ let r = Some (Coq.interp verbosely phrase) in
+ let msg = read_stdout () in
+ self#insert_message (if show_output then msg else "");
+ r
+ end
+ with e ->
+ (if show_error then
+ let (s,loc) = Coq.process_exn e in
+ assert (Glib.Utf8.validate s);
+ self#set_message s;
+ message_view#misc#draw None;
+ if localize then
+ (match Util.option_app Util.unloc loc with
+ | None -> ()
+ | Some (start,stop) ->
+ let convert_pos = byte_offset_to_char_offset phrase in
+ let start = convert_pos start in
+ let stop = convert_pos stop in
+ let i = self#get_start_of_input in
+ let starti = i#forward_chars start in
+ let stopi = i#forward_chars stop in
+ input_buffer#apply_tag_by_name "error"
+ ~start:starti
+ ~stop:stopi;
+ input_buffer#place_cursor starti;
+ ));
+ None
+
+ method find_phrase_starting_at (start:GText.iter) =
+ prerr_endline "find_phrase_starting_at starting now";
+ let trash_bytes = ref "" in
+ let end_iter = start#copy in
+ let lexbuf_function s count =
+ let i = ref 0 in
+ let n_trash = String.length !trash_bytes in
+ String.blit !trash_bytes 0 s 0 n_trash;
+ i := n_trash;
+ try
+ while !i <= count - 1 do
+ let c = end_iter#char in
+ if c = 0 then raise (Stop !i);
+ let c' = Glib.Utf8.from_unichar c in
+ let n = String.length c' in
+ if (n<=0) then exit (-2);
+ if n > count - !i then
+ begin
+ let ri = count - !i in
+ String.blit c' 0 s !i ri;
+ trash_bytes := String.sub c' ri (n-ri);
+ i := count ;
+ end else begin
+ String.blit c' 0 s !i n;
+ i:= !i + n
+ end;
+ if not end_iter#nocopy#forward_char then
+ raise (Stop !i)
+ done;
+ count
+ with Stop x ->
+ x
+ in
+ try
+ trash_bytes := "";
+ let phrase = Find_phrase.get (Lexing.from_function lexbuf_function)
+ in
+ end_iter#nocopy#set_offset (start#offset + !Find_phrase.length);
+ Some (start,end_iter)
+ with
+ | Find_phrase.EOF s ->
+ (* Phrase is at the end of the buffer*)
+ let si = start#offset in
+ let ei = si + !Find_phrase.length in
+ end_iter#nocopy#set_offset (ei - 1);
+ input_buffer#insert ~iter:end_iter "\n";
+ Some (input_buffer#get_iter (`OFFSET si),
+ input_buffer#get_iter (`OFFSET ei))
+ | _ -> None
+
+ method complete_at_offset (offset:int) =
+ prerr_endline ("Completion at offset : " ^ string_of_int offset);
+ let it () = input_buffer#get_iter (`OFFSET offset) in
+ let iit = it () in
+ let start = find_word_start iit in
+ if ends_word iit then
+ let w = input_buffer#get_text
+ ~start
+ ~stop:iit
+ ()
+ in
+ if String.length w <> 0 then begin
+ prerr_endline ("Completion of prefix : '" ^ w^"'");
+ match complete input_buffer w start#offset with
+ | None -> false
+ | Some (ss,start,stop) ->
+ let completion = input_buffer#get_text ~start ~stop () in
+ ignore (input_buffer#delete_selection ());
+ ignore (input_buffer#insert_interactive completion);
+ input_buffer#move_mark `SEL_BOUND (it())#backward_char;
+ true
+ end else false
+ else false
+
+
+ method process_next_phrase verbosely display_goals do_highlight =
+ begin
+ try
+ self#clear_message;
+ prerr_endline "process_next_phrase starting now";
+ if do_highlight then begin
+ !push_info "Coq is computing";
+ input_view#set_editable false;
+ end;
+ begin match (self#find_phrase_starting_at self#get_start_of_input)
+ with
+ | None ->
+ if do_highlight then begin
+ input_view#set_editable true;
+ !pop_info ();
+ end; false
+ | Some(start,stop) ->
+ prerr_endline "process_next_phrase : to_process highlight";
+ let b = input_buffer in
+ if do_highlight then begin
+ input_buffer#apply_tag_by_name ~start ~stop "to_process";
+ prerr_endline "process_next_phrase : to_process applied";
+ end;
+ prerr_endline "process_next_phrase : getting phrase";
+ let phrase = start#get_slice ~stop in
+ let r =
+ match self#send_to_coq verbosely false phrase true true true with
+ | Some ast ->
+ begin
+ b#move_mark ~where:stop (`NAME "start_of_input");
+ b#apply_tag_by_name "processed" ~start ~stop;
+ if (self#get_insert#compare) stop <= 0 then
+ begin
+ b#place_cursor stop;
+ self#recenter_insert
+ end;
+ let start_of_phrase_mark = `MARK (b#create_mark start) in
+ let end_of_phrase_mark = `MARK (b#create_mark stop) in
+ push_phrase
+ start_of_phrase_mark
+ end_of_phrase_mark ast;
+ if display_goals then self#show_goals;
+ true
+ end
+ | None -> false
+ in
+ if do_highlight then begin
+ b#remove_tag_by_name ~start ~stop "to_process" ;
+ input_view#set_editable true;
+ !pop_info ();
+ end;
+ r;
+ end
+ with e -> raise e
+ end
+
+ method insert_this_phrase_on_success
+ show_output show_msg localize coqphrase insertphrase =
+ match self#send_to_coq false false coqphrase show_output show_msg localize with
+ | Some ast ->
+ begin
+ let stop = self#get_start_of_input in
+ if stop#starts_line then
+ input_buffer#insert ~iter:stop insertphrase
+ else input_buffer#insert ~iter:stop ("\n"^insertphrase);
+ let start = self#get_start_of_input in
+ input_buffer#move_mark ~where:stop (`NAME "start_of_input");
+ input_buffer#apply_tag_by_name "processed" ~start ~stop;
+ if (self#get_insert#compare) stop <= 0 then
+ input_buffer#place_cursor stop;
+ let start_of_phrase_mark = `MARK (input_buffer#create_mark start)
+ in
+ let end_of_phrase_mark = `MARK (input_buffer#create_mark stop) in
+ push_phrase start_of_phrase_mark end_of_phrase_mark ast;
+ self#show_goals;
+ (*Auto insert save on success...
+ try (match Coq.get_current_goals () with
+ | [] ->
+ (match self#send_to_coq "Save.\n" true true true with
+ | Some ast ->
+ begin
+ let stop = self#get_start_of_input in
+ if stop#starts_line then
+ input_buffer#insert ~iter:stop "Save.\n"
+ else input_buffer#insert ~iter:stop "\nSave.\n";
+ let start = self#get_start_of_input in
+ input_buffer#move_mark ~where:stop (`NAME "start_of_input");
+ input_buffer#apply_tag_by_name "processed" ~start ~stop;
+ if (self#get_insert#compare) stop <= 0 then
+ input_buffer#place_cursor stop;
+ let start_of_phrase_mark = `MARK (input_buffer#create_mark start)
+ in
+ let end_of_phrase_mark = `MARK (input_buffer#create_mark stop) in
+ push_phrase start_of_phrase_mark end_of_phrase_mark ast
+ end
+ | None -> ())
+ | _ -> ())
+ with _ -> ()*)
+ true
+ end
+ | None -> self#insert_message ("Unsuccessfully tried: "^coqphrase);
+ false
+
+ method process_until_iter_or_error stop =
+ let stop' = `OFFSET stop#offset in
+ let start = self#get_start_of_input#copy in
+ let start' = `OFFSET start#offset in
+ input_buffer#apply_tag_by_name
+ ~start
+ ~stop
+ "to_process";
+ input_view#set_editable false;
+ !push_info "Coq is computing";
+ process_pending ();
+ (try
+ while ((stop#compare self#get_start_of_input>=0)
+ && (self#process_next_phrase false false false))
+ do Util.check_for_interrupt () done
+ with Sys.Break ->
+ prerr_endline "Interrupted during process_until_iter_or_error");
+ self#show_goals;
+ (* Start and stop might be invalid if an eol was added at eof *)
+ let start = input_buffer#get_iter start' in
+ let stop = input_buffer#get_iter stop' in
+ input_buffer#remove_tag_by_name ~start ~stop "to_process" ;
+ input_view#set_editable true;
+ !pop_info()
+
+ method process_until_end_or_error =
+ self#process_until_iter_or_error input_buffer#end_iter
+
+ method reset_initial =
+ Stack.iter
+ (function inf ->
+ let start = input_buffer#get_iter_at_mark inf.start in
+ let stop = input_buffer#get_iter_at_mark inf.stop in
+ input_buffer#move_mark ~where:start (`NAME "start_of_input");
+ input_buffer#remove_tag_by_name "processed" ~start ~stop;
+ input_buffer#delete_mark inf.start;
+ input_buffer#delete_mark inf.stop;
+ )
+ processed_stack;
+ Stack.clear processed_stack;
+ self#clear_message;
+ Coq.reset_initial ()
+
+
+ (* backtrack Coq to the phrase preceding iterator [i] *)
+ method backtrack_to_no_lock i =
+ prerr_endline "Backtracking_to iter starts now.";
+ (* re-synchronize Coq to the current state of the stack *)
+ let rec synchro () =
+ if is_empty () then
+ Coq.reset_initial ()
+ else begin
+ let t = pop () in
+ begin match t.reset_info with
+ | Reset (id, ({contents=true} as v)) -> v:=false;
+ (match snd t.ast with
+ | VernacBeginSection _ | VernacDefineModule _
+ | VernacDeclareModule _ | VernacDeclareModuleType _
+ | VernacEndSegment _
+ -> reset_to_mod id
+ | _ -> reset_to id)
+ | _ -> synchro ()
+ end;
+ interp_last t.ast;
+ repush_phrase t
+ end
+ in
+ let add_undo t = match t with | Some n -> Some (succ n) | None -> None
+ in
+ (* pop Coq commands until we reach iterator [i] *)
+ let rec pop_commands done_smthg undos =
+ if is_empty () then
+ done_smthg, undos
+ else
+ let t = top () in
+ if i#compare (input_buffer#get_iter_at_mark t.stop) < 0 then begin
+ ignore (pop ());
+ let undos = if is_tactic (snd t.ast) then add_undo undos else None in
+ pop_commands true undos
+ end else
+ done_smthg, undos
+ in
+ let done_smthg, undos = pop_commands false (Some 0) in
+ prerr_endline "Popped commands";
+ if done_smthg then
+ begin
+ try
+ (match undos with
+ | None -> synchro ()
+ | Some n -> try Pfedit.undo n with _ -> synchro ());
+ let start = if is_empty () then input_buffer#start_iter
+ else input_buffer#get_iter_at_mark (top ()).stop
+ in
+ prerr_endline "Removing (long) processed tag...";
+ input_buffer#remove_tag_by_name
+ ~start
+ ~stop:self#get_start_of_input
+ "processed";
+ prerr_endline "Moving (long) start_of_input...";
+ input_buffer#move_mark ~where:start (`NAME "start_of_input");
+ self#show_goals;
+ clear_stdout ();
+ self#clear_message;
+ with _ ->
+ !push_info "WARNING: undo failed badly -> Coq might be in an inconsistent state.
+Please restart and report NOW.";
+ end
+ else prerr_endline "backtrack_to : discarded (...)"
+
+ method backtrack_to i =
+ if Mutex.try_lock coq_may_stop then
+ (!push_info "Undoing...";self#backtrack_to_no_lock i ; Mutex.unlock coq_may_stop;
+ !pop_info ())
+ else prerr_endline "backtrack_to : discarded (lock is busy)"
+
+ method go_to_insert =
+ let point = self#get_insert in
+ if point#compare self#get_start_of_input>=0
+ then self#process_until_iter_or_error point
+ else self#backtrack_to point
+
+ method undo_last_step =
+ if Mutex.try_lock coq_may_stop then
+ (!push_info "Undoing last step...";
+ (try
+ let last_command = top () in
+ let start = input_buffer#get_iter_at_mark last_command.start in
+ let update_input () =
+ prerr_endline "Removing processed tag...";
+ input_buffer#remove_tag_by_name
+ ~start
+ ~stop:(input_buffer#get_iter_at_mark last_command.stop)
+ "processed";
+ prerr_endline "Moving start_of_input";
+ input_buffer#move_mark
+ ~where:start
+ (`NAME "start_of_input");
+ input_buffer#place_cursor start;
+ self#recenter_insert;
+ self#show_goals;
+ self#clear_message
+ in
+ begin match last_command with
+ | {ast=_, (VernacSolve _ | VernacTime (VernacSolve _))} ->
+ begin
+ try Pfedit.undo 1; ignore (pop ()); update_input ()
+ with _ -> self#backtrack_to_no_lock start
+ end
+ | {ast=_,t;reset_info=Reset (id, {contents=true})} ->
+ ignore (pop ());
+ (match t with
+ | VernacBeginSection _ | VernacDefineModule _
+ | VernacDeclareModule _ | VernacDeclareModuleType _
+ | VernacEndSegment _
+ -> reset_to_mod id
+ | _ -> reset_to id);
+ update_input ()
+ | { ast = _, ( VernacStartTheoremProof _
+ | VernacGoal _
+ | VernacDeclareTacticDefinition _
+ | VernacDefinition (_,_,ProveBody _,_));
+ reset_info=Reset(id,{contents=false})} ->
+ ignore (pop ());
+ (try
+ Pfedit.delete_current_proof ()
+ with e ->
+ begin
+ prerr_endline "WARNING : found a closed environment";
+ raise e
+ end);
+ update_input ()
+ | { ast = (_, a) } when is_state_preserving a ->
+ ignore (pop ());
+ update_input ()
+ | _ ->
+ self#backtrack_to_no_lock start
+ end;
+ with
+ | Size 0 -> (* !flash_info "Nothing to Undo"*)()
+ );
+ !pop_info ();
+ Mutex.unlock coq_may_stop)
+ else prerr_endline "undo_last_step discarded"
+
+
+ method blaster () =
+
+ ignore (Thread.create
+ (fun () ->
+ prerr_endline "Blaster called";
+ let c = Blaster_window.present_blaster_window () in
+ if Mutex.try_lock c#lock then begin
+ c#clear ();
+ let current_gls = try get_current_goals () with _ -> [] in
+ let gls_nb = List.length current_gls in
+
+ let set_goal i (s,t) =
+ let gnb = string_of_int i in
+ let s = gnb ^":"^s in
+ let t' = gnb ^": progress "^t in
+ let t'' = gnb ^": "^t in
+ c#set
+ ("Goal "^gnb)
+ s
+ (fun () -> try_interptac t')
+ (fun () -> self#insert_command t'' t'')
+ in
+ let set_current_goal (s,t) =
+ c#set
+ "Goal 1"
+ s
+ (fun () -> try_interptac ("progress "^t))
+ (fun () -> self#insert_command t t)
+ in
+ begin match current_gls with
+ | [] -> ()
+ | (hyp_l,current_gl)::r ->
+ List.iter set_current_goal (concl_menu current_gl);
+ List.iter
+ (fun hyp ->
+ List.iter set_current_goal (hyp_menu hyp))
+ hyp_l;
+ let i = ref 2 in
+ List.iter
+ (fun (hyp_l,gl) ->
+ List.iter (set_goal !i) (concl_menu gl);
+ incr i)
+ r
+ end;
+ let _ = c#blaster () in
+ Mutex.unlock c#lock
+ end else prerr_endline "Blaster discarded")
+ ())
+
+ method insert_command cp ip =
+ self#clear_message;
+ ignore (self#insert_this_phrase_on_success true false false cp ip)
+
+ method tactic_wizard l =
+ self#clear_message;
+ ignore
+ (List.exists
+ (fun p ->
+ self#insert_this_phrase_on_success true false false
+ ("progress "^p^".\n") (p^".\n")) l)
+
+ method active_keypress_handler k =
+ let state = GdkEvent.Key.state k in
+ begin
+ match state with
+ | l when List.mem `MOD1 l ->
+ let k = GdkEvent.Key.keyval k in
+ if GdkKeysyms._Return=k
+ then ignore(
+ if (input_buffer#insert_interactive "\n") then
+ begin
+ let i= self#get_insert#backward_word_start in
+ prerr_endline "active_kp_hf: Placing cursor";
+ self#process_until_iter_or_error i
+ end);
+ true
+ | l when List.mem `CONTROL l ->
+ let k = GdkEvent.Key.keyval k in
+ if GdkKeysyms._Break=k
+ then break ();
+ false
+ | l ->
+ if GdkEvent.Key.keyval k = GdkKeysyms._Tab then begin
+ prerr_endline "active_kp_handler for Tab";
+ self#indent_current_line;
+ true
+ end else false
+ end
+ method disconnected_keypress_handler k =
+ match GdkEvent.Key.state k with
+ | l when List.mem `CONTROL l ->
+ let k = GdkEvent.Key.keyval k in
+ if GdkKeysyms._c=k
+ then break ();
+ false
+ | l -> false
+
+
+ val mutable deact_id = None
+ val mutable act_id = None
+
+ method deactivate () =
+ is_active <- false;
+ (match act_id with None -> ()
+ | Some id ->
+ reset_initial ();
+ input_view#misc#disconnect id;
+ prerr_endline "DISCONNECTED old active : ";
+ print_id id;
+ );
+ deact_id <- Some
+ (input_view#event#connect#key_press self#disconnected_keypress_handler);
+ prerr_endline "CONNECTED inactive : ";
+ print_id (out_some deact_id)
+
+ method activate () =
+ is_active <- true;
+ (match deact_id with None -> ()
+ | Some id -> input_view#misc#disconnect id;
+ prerr_endline "DISCONNECTED old inactive : ";
+ print_id id
+ );
+ act_id <- Some
+ (input_view#event#connect#key_press self#active_keypress_handler);
+ prerr_endline "CONNECTED active : ";
+ print_id (out_some act_id);
+ let dir = (match
+ (out_some ((Vector.get input_views index).analyzed_view))
+ #filename
+ with
+ | None -> ()
+ | Some f ->
+ if not (is_in_coq_path f) then
+ begin
+ let dir = Filename.dirname f in
+ ignore (Coq.interp false
+ (Printf.sprintf "Add LoadPath \"%s\". " dir))
+ end)
+ in ()
+
+
+
+ method electric_handler =
+ input_buffer#connect#insert_text ~callback:
+ (fun it x ->
+ begin try
+ if last_index then begin
+ last_array.(0)<-x;
+ if (last_array.(1) ^ last_array.(0) = ".\n") then raise Found
+ end else begin
+ last_array.(1)<-x;
+ if (last_array.(0) ^ last_array.(1) = ".\n") then raise Found
+ end
+ with Found ->
+ begin
+ ignore (self#process_next_phrase false true true)
+ end;
+ end;
+ last_index <- not last_index;)
+
+ method private electric_paren tag =
+ let oparen_code = Glib.Utf8.to_unichar "(" (ref 0) in
+ let cparen_code = Glib.Utf8.to_unichar ")" (ref 0) in
+ ignore (input_buffer#connect#insert_text ~callback:
+ (fun it x ->
+ input_buffer#remove_tag
+ ~start:input_buffer#start_iter
+ ~stop:input_buffer#end_iter
+ tag;
+ if x = "" then () else
+ match x.[String.length x - 1] with
+ | ')' ->
+ let hit = self#get_insert in
+ let count = ref 0 in
+ if hit#nocopy#backward_find_char
+ (fun c ->
+ if c = oparen_code && !count = 0 then true
+ else if c = cparen_code then
+ (incr count;false)
+ else if c = oparen_code then
+ (decr count;false)
+ else false
+ )
+ then
+ begin
+ prerr_endline "Found matching parenthesis";
+ input_buffer#apply_tag tag ~start:hit ~stop:hit#forward_char
+ end
+ else ()
+ | _ -> ())
+ )
+
+ method help_for_keyword () =
+
+ browse_keyword (self#insert_message) (get_current_word ())
+
+ initializer
+ ignore (message_buffer#connect#insert_text
+ ~callback:(fun it s -> ignore
+ (message_view#scroll_to_mark
+ ~use_align:false
+ ~within_margin:0.49
+ `INSERT)));
+ ignore (input_buffer#connect#insert_text
+ ~callback:(fun it s ->
+ if (it#compare self#get_start_of_input)<0
+ then GtkSignal.stop_emit ();
+ if String.length s > 1 then
+ (prerr_endline "insert_text: Placing cursor";input_buffer#place_cursor it)));
+ ignore (input_buffer#connect#after#apply_tag
+ ~callback:(fun tag ~start ~stop ->
+ if (start#compare self#get_start_of_input)>=0
+ then
+ input_buffer#remove_tag_by_name
+ ~start
+ ~stop
+ "processed"
+ )
+ );
+ ignore (input_buffer#connect#after#insert_text
+ ~callback:(fun it s ->
+ if auto_complete_on &&
+ String.length s = 1 && s <> " " && s <> "\n"
+ then
+ let v = out_some (get_current_view ()).analyzed_view
+ in
+ let has_completed =
+ v#complete_at_offset
+ ((v#view#buffer#get_iter `SEL_BOUND)#offset)
+ in
+ if has_completed then
+ input_buffer#move_mark `SEL_BOUND (input_buffer#get_iter `SEL_BOUND)#forward_char;
+
+
+ )
+ );
+ ignore (input_buffer#connect#modified_changed
+ ~callback:
+ (fun () ->
+ if input_buffer#modified then
+ set_tab_image index
+ ~icon:(match (out_some (current_all.analyzed_view))#filename with
+ | None -> `SAVE_AS
+ | Some _ -> `SAVE
+ )
+ else set_tab_image index ~icon:`YES;
+ ));
+ ignore (input_buffer#connect#changed
+ ~callback:(fun () ->
+ last_modification_time <- Unix.time ();
+ let r = input_view#visible_rect in
+ let stop =
+ input_view#get_iter_at_location
+ ~x:(Gdk.Rectangle.x r + Gdk.Rectangle.width r)
+ ~y:(Gdk.Rectangle.y r + Gdk.Rectangle.height r)
+ in
+ input_buffer#remove_tag_by_name
+ ~start:self#get_start_of_input
+ ~stop
+ "error";
+ Highlight.highlight_around_current_line
+ input_buffer
+ )
+ );
+ ignore (input_buffer#add_selection_clipboard (cb()));
+ let paren_highlight_tag = input_buffer#create_tag ~name:"paren" [`BACKGROUND "purple"] in
+ self#electric_paren paren_highlight_tag;
+ ignore (input_buffer#connect#after#mark_set
+ ~callback:(fun it (m:Gtk.text_mark) ->
+ !set_location
+ (Printf.sprintf
+ "Line: %5d Char: %3d" (self#get_insert#line + 1)
+ (self#get_insert#line_offset + 1));
+ match GtkText.Mark.get_name m with
+ | Some "insert" ->
+ input_buffer#remove_tag
+ ~start:input_buffer#start_iter
+ ~stop:input_buffer#end_iter
+ paren_highlight_tag;
+ | Some s ->
+ prerr_endline (s^" moved")
+ | None -> () )
+ );
+ ignore (input_buffer#connect#insert_text
+ (fun it s ->
+ prerr_endline "Should recenter ?";
+ if String.contains s '\n' then begin
+ prerr_endline "Should recenter : yes";
+ self#recenter_insert
+ end))
+end
+
+let create_input_tab filename =
+ let b = GText.buffer () in
+ let tablabel = GMisc.label () in
+ let v_box = GPack.hbox ~homogeneous:false () in
+ let image = GMisc.image ~packing:v_box#pack () in
+ let label = GMisc.label ~text:filename ~packing:v_box#pack () in
+ let fr1 = GBin.frame ~shadow_type:`ETCHED_OUT
+ ~packing:((notebook ())#append_page
+ ~tab_label:v_box#coerce) ()
+ in
+ let sw1 = GBin.scrolled_window
+ ~vpolicy:`AUTOMATIC
+ ~hpolicy:`AUTOMATIC
+ ~packing:fr1#add ()
+ in
+ let tv1 = Undo.undoable_view ~buffer:b ~packing:(sw1#add) () in
+ prerr_endline ("Language: "^ b#start_iter#language);
+ tv1#misc#set_name "ScriptWindow";
+ let _ = tv1#set_editable true in
+ let _ = tv1#set_wrap_mode `NONE in
+ b#place_cursor ~where:(b#start_iter);
+ ignore (tv1#event#connect#button_press ~callback:
+ (fun ev -> GdkEvent.Button.button ev = 3));
+(* ignore (tv1#event#connect#button_press ~callback:
+ (fun ev ->
+ if (GdkEvent.Button.button ev=2) then
+ (try
+ prerr_endline "Paste invoked";
+ GtkSignal.emit_unit
+ (get_current_view()).view#as_view
+ GtkText.View.Signals.paste_clipboard;
+ true
+ with _ -> false)
+ else false
+ ));*)
+ tv1#misc#grab_focus ();
+ ignore (tv1#buffer#create_mark
+ ~name:"start_of_input"
+ tv1#buffer#start_iter);
+ ignore (tv1#buffer#create_tag
+ ~name:"kwd"
+ [`FOREGROUND "blue"]);
+ ignore (tv1#buffer#create_tag
+ ~name:"decl"
+ [`FOREGROUND "orange red"]);
+ ignore (tv1#buffer#create_tag
+ ~name:"comment"
+ [`FOREGROUND "brown"]);
+ ignore (tv1#buffer#create_tag
+ ~name:"reserved"
+ [`FOREGROUND "dark red"]);
+ ignore (tv1#buffer#create_tag
+ ~name:"error"
+ [`UNDERLINE `DOUBLE ; `FOREGROUND "red"]);
+ ignore (tv1#buffer#create_tag
+ ~name:"to_process"
+ [`BACKGROUND "light blue" ;`EDITABLE false]);
+ ignore (tv1#buffer#create_tag
+ ~name:"processed"
+ [`BACKGROUND "light green" ;`EDITABLE false]);
+ ignore (tv1#buffer#create_tag
+ ~name:"found"
+ [`BACKGROUND "blue"; `FOREGROUND "white"]);
+ tv1
+
+
+let last_make = ref "";;
+let last_make_index = ref 0;;
+let search_compile_error_regexp =
+ Str.regexp
+ "File \"\\([^\"]+\\)\", line \\([0-9]+\\), characters \\([0-9]+\\)-\\([0-9]+\\)";;
+
+let search_next_error () =
+ let _ = Str.search_forward search_compile_error_regexp !last_make !last_make_index in
+ let f = Str.matched_group 1 !last_make
+ and l = int_of_string (Str.matched_group 2 !last_make)
+ and b = int_of_string (Str.matched_group 3 !last_make)
+ and e = int_of_string (Str.matched_group 4 !last_make)
+ and msg_index = Str.match_beginning ()
+ in
+ last_make_index := Str.group_end 4;
+ (f,l,b,e,
+ String.sub !last_make msg_index (String.length !last_make - msg_index))
+
+let main files =
+ (* Statup preferences *)
+ load_pref ();
+
+ (* Main window *)
+ let w = GWindow.window
+ ~wm_class:"CoqIde" ~wm_name:"CoqIde"
+ ~allow_grow:true ~allow_shrink:true
+ ~width:!current.window_width ~height:!current.window_height
+ ~title:"CoqIde" ()
+ in
+(*
+ let icon_image = Filename.concat lib_ide "coq.ico" in
+ let icon = GdkPixbuf.from_file icon_image in
+ w#set_icon (Some icon);
+*)
+ let vbox = GPack.vbox ~homogeneous:false ~packing:w#add () in
+
+
+ (* Menu bar *)
+ let menubar = GMenu.menu_bar ~packing:vbox#pack () in
+
+ (* Toolbar *)
+ let toolbar = GButton.toolbar
+ ~orientation:`HORIZONTAL
+ ~style:`ICONS
+ ~tooltips:true
+ ~packing:(* handle#add *)
+ (vbox#pack ~expand:false ~fill:false)
+ ()
+ in
+ show_toolbar :=
+ (fun b -> if b then toolbar#misc#show () else toolbar#misc#hide ());
+
+ let factory = new GMenu.factory ~accel_path:"<CoqIde MenuBar>/" menubar in
+ let accel_group = factory#accel_group in
+
+ (* File Menu *)
+ let file_menu = factory#add_submenu "_File" in
+
+ let file_factory = new GMenu.factory ~accel_path:"<CoqIde MenuBar>/File/" file_menu ~accel_group in
+
+ (* File/Load Menu *)
+ let load f =
+ let f = absolute_filename f in
+ try
+ prerr_endline "Loading file starts";
+ Vector.find_or_fail
+ (function
+ | {analyzed_view=Some av} ->
+ (match av#filename with
+ | None -> false
+ | Some fn -> same_file f fn)
+ | _ -> false)
+ !input_views;
+ prerr_endline "Loading: must open";
+ let b = Buffer.create 1024 in
+ prerr_endline "Loading: get raw content";
+ with_file f ~f:(input_channel b);
+ prerr_endline "Loading: convert content";
+ let s = do_convert (Buffer.contents b) in
+ prerr_endline "Loading: create view";
+ let view = create_input_tab (Glib.Convert.filename_to_utf8
+ (Filename.basename f))
+ in
+ prerr_endline "Loading: change font";
+ view#misc#modify_font !current.text_font;
+ prerr_endline "Loading: adding view";
+ let index = add_input_view {view = view;
+ analyzed_view = None;
+ }
+ in
+ let av = (new analyzed_view index) in
+ prerr_endline "Loading: register view";
+ (get_input_view index).analyzed_view <- Some av;
+ prerr_endline "Loading: set filename";
+ av#set_filename (Some f);
+ prerr_endline "Loading: stats";
+ av#update_stats;
+ let input_buffer = view#buffer in
+ prerr_endline "Loading: fill buffer";
+ input_buffer#set_text s;
+ input_buffer#place_cursor input_buffer#start_iter;
+ prerr_endline ("Loading: switch to view "^ string_of_int index);
+ set_current_view index;
+ set_tab_image index ~icon:`YES;
+ prerr_endline "Loading: highlight";
+ Highlight.highlight_all input_buffer;
+ input_buffer#set_modified false;
+ prerr_endline "Loading: clear undo";
+ av#view#clear_undo;
+ prerr_endline "Loading: success"
+ with
+ | Vector.Found i -> set_current_view i
+ | e -> !flash_info ("Load failed: "^(Printexc.to_string e))
+ in
+ let load_m = file_factory#add_item "_Open/Create"
+ ~key:GdkKeysyms._O in
+ let load_f () =
+ match select_file ~title:"Load file" () with
+ | None -> ()
+ | (Some f) as fn -> load f
+ in
+ ignore (load_m#connect#activate (load_f));
+
+ (* File/Save Menu *)
+ let save_m = file_factory#add_item "_Save"
+ ~key:GdkKeysyms._S in
+
+
+ let save_f () =
+ let current = get_current_view () in
+ try
+ (match (out_some current.analyzed_view)#filename with
+ | None ->
+ begin match GToolbox.select_file ~title:"Save file" ()
+ with
+ | None -> ()
+ | Some f ->
+ if (out_some current.analyzed_view)#save_as f then begin
+ set_current_tab_label (Filename.basename f);
+ !flash_info ("File " ^ f ^ " saved")
+ end
+ else warning ("Save Failed (check if " ^ f ^ " is writable)")
+ end
+ | Some f ->
+ if (out_some current.analyzed_view)#save f then
+ !flash_info ("File " ^ f ^ " saved")
+ else warning ("Save Failed (check if " ^ f ^ " is writable)")
+
+ )
+ with
+ | e -> warning "Save: unexpected error"
+ in
+ ignore (save_m#connect#activate save_f);
+
+ (* File/Save As Menu *)
+ let saveas_m = file_factory#add_item "S_ave as"
+ in
+ let saveas_f () =
+ let current = get_current_view () in
+ try (match (out_some current.analyzed_view)#filename with
+ | None ->
+ begin match GToolbox.select_file ~title:"Save file as" ()
+ with
+ | None -> ()
+ | Some f ->
+ if (out_some current.analyzed_view)#save_as f then begin
+ set_current_tab_label (Filename.basename f);
+ !flash_info "Saved"
+ end
+ else !flash_info "Save Failed"
+ end
+ | Some f ->
+ begin match GToolbox.select_file
+ ~dir:(ref (Filename.dirname f))
+ ~filename:(Filename.basename f)
+ ~title:"Save file as" ()
+ with
+ | None -> ()
+ | Some f ->
+ if (out_some current.analyzed_view)#save_as f then begin
+ set_current_tab_label (Filename.basename f);
+ !flash_info "Saved"
+ end else !flash_info "Save Failed"
+ end);
+ with e -> !flash_info "Save Failed"
+ in
+ ignore (saveas_m#connect#activate saveas_f);
+
+ (* File/Save All Menu *)
+ let saveall_m = file_factory#add_item "Sa_ve All" in
+ let saveall_f () =
+ Vector.iter
+ (function
+ | {view = view ; analyzed_view = Some av} as full ->
+ begin match av#filename with
+ | None -> ()
+ | Some f ->
+ ignore (av#save f)
+ end
+ | _ -> ()
+ ) input_views
+ in
+ let has_something_to_save () =
+ Vector.exists
+ (function
+ | {view=view} -> view#buffer#modified
+ )
+ input_views
+ in
+ ignore (saveall_m#connect#activate saveall_f);
+
+ (* File/Revert Menu *)
+ let revert_m = file_factory#add_item "_Revert All Buffers" in
+ let revert_f () =
+ Vector.iter
+ (function
+ {view = view ; analyzed_view = Some av} as full ->
+ (try
+ match av#filename,av#stats with
+ | Some f,Some stats ->
+ let new_stats = Unix.stat f in
+ if new_stats.Unix.st_mtime > stats.Unix.st_mtime
+ then av#revert
+ | Some _, None -> av#revert
+ | _ -> ()
+ with _ -> av#revert)
+ | _ -> ()
+ ) input_views
+ in
+ ignore (revert_m#connect#activate revert_f);
+
+ (* File/Close Menu *)
+ let close_m = file_factory#add_item "_Close Buffer" in
+ let close_f () =
+ let v = out_some !active_view in
+ let act = get_current_view_page () in
+ if v = act then !flash_info "Cannot close an active view"
+ else remove_current_view_page ()
+ in
+ ignore (close_m#connect#activate close_f);
+
+ (* File/Print Menu *)
+ let print_f () =
+ let v = get_current_view () in
+ let av = out_some v.analyzed_view in
+ match av#filename with
+ | None ->
+ !flash_info "Cannot print: this buffer has no name"
+ | Some f ->
+ let cmd =
+ "cd " ^ Filename.dirname f ^ "; " ^
+ !current.cmd_coqdoc ^ " -ps " ^ Filename.basename f ^
+ " | " ^ !current.cmd_print
+ in
+ let s,_ = run_command av#insert_message cmd in
+ !flash_info (cmd ^ if s = Unix.WEXITED 0 then " succeeded" else " failed")
+ in
+ let print_m = file_factory#add_item "_Print" ~callback:print_f in
+
+ (* File/Export to Menu *)
+ let export_f kind () =
+ let v = get_current_view () in
+ let av = out_some v.analyzed_view in
+ match av#filename with
+ | None ->
+ !flash_info "Cannot print: this buffer has no name"
+ | Some f ->
+ let basef = Filename.basename f in
+ let output =
+ let basef_we = try Filename.chop_extension basef with _ -> basef in
+ match kind with
+ | "latex" -> basef_we ^ ".tex"
+ | "dvi" | "ps" | "html" -> basef_we ^ "." ^ kind
+ | _ -> assert false
+ in
+ let cmd =
+ "cd " ^ Filename.dirname f ^ "; " ^
+ !current.cmd_coqdoc ^ " --" ^ kind ^ " -o " ^ output ^ " " ^ basef
+ in
+ let s,_ = run_command av#insert_message cmd in
+ !flash_info (cmd ^
+ if s = Unix.WEXITED 0
+ then " succeeded"
+ else " failed")
+ in
+ let file_export_m = file_factory#add_submenu "E_xport to" in
+
+ let file_export_factory = new GMenu.factory ~accel_path:"<CoqIde MenuBar>/Export/" file_export_m ~accel_group in
+ let export_html_m =
+ file_export_factory#add_item "_Html" ~callback:(export_f "html")
+ in
+ let export_latex_m =
+ file_export_factory#add_item "_LaTeX" ~callback:(export_f "latex")
+ in
+ let export_dvi_m =
+ file_export_factory#add_item "_Dvi" ~callback:(export_f "dvi")
+ in
+ let export_ps_m =
+ file_export_factory#add_item "_Ps" ~callback:(export_f "ps")
+ in
+
+ (* File/Rehighlight Menu *)
+ let rehighlight_m = file_factory#add_item "Reh_ighlight" ~key:GdkKeysyms._L in
+ ignore (rehighlight_m#connect#activate
+ (fun () ->
+ Highlight.highlight_all
+ (get_current_view()).view#buffer;
+ (out_some (get_current_view()).analyzed_view)#recenter_insert));
+
+ (* File/Quit Menu *)
+ let quit_f () =
+ save_pref();
+ if has_something_to_save () then
+ match (GToolbox.question_box ~title:"Quit"
+ ~buttons:["Save Named Buffers and Quit";
+ "Quit without Saving";
+ "Don't Quit"]
+ ~default:0
+ ~icon:
+ (let img = GMisc.image () in
+ img#set_stock `DIALOG_WARNING;
+ img#set_icon_size `DIALOG;
+ img#coerce)
+ "There are unsaved buffers"
+ )
+ with 1 -> saveall_f () ; exit 0
+ | 2 -> exit 0
+ | _ -> ()
+ else exit 0
+ in
+ let quit_m = file_factory#add_item "_Quit" ~key:GdkKeysyms._Q
+ ~callback:quit_f
+ in
+ ignore (w#event#connect#delete (fun _ -> quit_f (); true));
+
+ (* Edit Menu *)
+ let edit_menu = factory#add_submenu "_Edit" in
+ let edit_f = new GMenu.factory ~accel_path:"<CoqIde MenuBar>/Edit/" edit_menu ~accel_group in
+ ignore(edit_f#add_item "_Undo" ~key:GdkKeysyms._u ~callback:
+ (do_if_not_computing "undo"
+ (fun () ->
+ ignore ((out_some ((get_current_view()).analyzed_view))#
+ without_auto_complete
+ (fun () -> (get_current_view()).view#undo) ()))));
+ ignore(edit_f#add_item "_Clear Undo Stack"
+ (* ~key:GdkKeysyms._exclam *)
+ ~callback:
+ (fun () ->
+ ignore (get_current_view()).view#clear_undo));
+ ignore(edit_f#add_separator ());
+ ignore(edit_f#add_item "Cut" ~key:GdkKeysyms._X ~callback:
+ (do_if_not_computing "cut"
+ (fun () -> GtkSignal.emit_unit
+ (get_current_view()).view#as_view
+ GtkText.View.S.cut_clipboard)));
+ ignore(edit_f#add_item "Copy" ~key:GdkKeysyms._C ~callback:
+ (fun () -> GtkSignal.emit_unit
+ (get_current_view()).view#as_view
+ GtkText.View.S.copy_clipboard));
+ ignore(edit_f#add_item "Paste" ~key:GdkKeysyms._V ~callback:
+ (do_if_not_computing "paste"
+ (fun () ->
+ try GtkSignal.emit_unit
+ (get_current_view()).view#as_view
+ GtkText.View.S.paste_clipboard
+ with _ -> prerr_endline "EMIT PASTE FAILED")));
+ ignore (edit_f#add_separator ());
+
+
+(*
+ let toggle_auto_complete_i =
+ edit_f#add_check_item "_Auto Completion"
+ ~active:!current.auto_complete
+ ~callback:
+ in
+*)
+(*
+ auto_complete :=
+ (fun b -> match (get_current_view()).analyzed_view with
+ | Some av -> av#set_auto_complete b
+ | None -> ());
+*)
+
+ let last_found = ref None in
+ let search_backward = ref false in
+ let find_w = GWindow.window
+ (* ~wm_class:"CoqIde" ~wm_name:"CoqIde" *)
+ (* ~allow_grow:true ~allow_shrink:true *)
+ (* ~width:!current.window_width ~height:!current.window_height *)
+ ~position:`CENTER
+ ~title:"CoqIde search/replace" ()
+ in
+ let find_box = GPack.table
+ ~columns:3 ~rows:5
+ ~col_spacings:10 ~row_spacings:10 ~border_width:10
+ ~homogeneous:false ~packing:find_w#add () in
+
+ let find_lbl =
+ GMisc.label ~text:"Find:"
+ ~xalign:1.0
+ ~packing:(find_box#attach ~left:0 ~top:0 ~fill:`X) ()
+ in
+ let find_entry = GEdit.entry
+ ~editable: true
+ ~packing: (find_box#attach ~left:1 ~top:0 ~expand:`X)
+ ()
+ in
+ let replace_lbl =
+ GMisc.label ~text:"Replace with:"
+ ~xalign:1.0
+ ~packing:(find_box#attach ~left:0 ~top:1 ~fill:`X) ()
+ in
+ let replace_entry = GEdit.entry
+ ~editable: true
+ ~packing: (find_box#attach ~left:1 ~top:1 ~expand:`X)
+ ()
+ in
+ let case_sensitive_check =
+ GButton.check_button
+ ~label:"case sensitive"
+ ~active:true
+ ~packing: (find_box#attach ~left:1 ~top:2)
+ ()
+ in
+(*
+ let find_backwards_check =
+ GButton.check_button
+ ~label:"search backwards"
+ ~active:false
+ ~packing: (find_box#attach ~left:1 ~top:3)
+ ()
+ in
+*)
+ let close_find_button =
+ GButton.button
+ ~label:"Close"
+ ~packing: (find_box#attach ~left:2 ~top:0)
+ ()
+ in
+ let replace_button =
+ GButton.button
+ ~label:"Replace"
+ ~packing: (find_box#attach ~left:2 ~top:1)
+ ()
+ in
+ let replace_find_button =
+ GButton.button
+ ~label:"Replace and find"
+ ~packing: (find_box#attach ~left:2 ~top:2)
+ ()
+ in
+ let find_again_button =
+ GButton.button
+ ~label:"_Find again"
+ ~packing: (find_box#attach ~left:2 ~top:3)
+ ()
+ in
+ let find_again_backward_button =
+ GButton.button
+ ~label:"Find _backward"
+ ~packing: (find_box#attach ~left:2 ~top:4)
+ ()
+ in
+ let last_find () =
+ let v = (get_current_view()).view in
+ let b = v#buffer in
+ let start,stop =
+ match !last_found with
+ | None -> let i = b#get_iter_at_mark `INSERT in (i,i)
+ | Some(start,stop) ->
+ let start = b#get_iter_at_mark start
+ and stop = b#get_iter_at_mark stop
+ in
+ b#remove_tag_by_name ~start ~stop "found";
+ last_found:=None;
+ start,stop
+ in
+ (v,b,start,stop)
+ in
+ let do_replace () =
+ let v = (get_current_view()).view in
+ let b = v#buffer in
+ match !last_found with
+ | None -> ()
+ | Some(start,stop) ->
+ let start = b#get_iter_at_mark start
+ and stop = b#get_iter_at_mark stop
+ in
+ b#delete ~start ~stop;
+ b#insert ~iter:start replace_entry#text;
+ last_found:=None
+ in
+ let find_from (v : Undo.undoable_view)
+ (b : GText.buffer) (starti : GText.iter) text =
+ prerr_endline ("Searching for " ^ text);
+ match (if !search_backward then starti#backward_search text
+ else starti#forward_search text)
+ with
+ | None -> ()
+ | Some(start,stop) ->
+ b#apply_tag_by_name "found" ~start ~stop;
+ let start = `MARK (b#create_mark start)
+ and stop = `MARK (b#create_mark stop)
+ in
+ v#scroll_to_mark ~use_align:false ~yalign:0.75 ~within_margin:0.25
+ stop;
+ last_found := Some(start,stop)
+ in
+ let do_find () =
+ let (v,b,starti,_) = last_find () in
+ find_from v b starti find_entry#text
+ in
+ let do_replace_find () =
+ do_replace();
+ do_find()
+ in
+ let close_find () =
+ let (v,b,_,stop) = last_find () in
+ b#place_cursor stop;
+ find_w#misc#hide();
+ v#coerce#misc#grab_focus()
+ in
+ to_do_on_page_switch :=
+ (fun i -> if find_w#misc#visible then close_find())::
+ !to_do_on_page_switch;
+ let find_again_forward () =
+ search_backward := false;
+ let (v,b,start,_) = last_find () in
+ let start = start#forward_chars 1 in
+ find_from v b start find_entry#text
+ in
+ let find_again_backward () =
+ search_backward := true;
+ let (v,b,start,_) = last_find () in
+ let start = start#backward_chars 1 in
+ find_from v b start find_entry#text
+ in
+ let key_find ev =
+ let s = GdkEvent.Key.state ev and k = GdkEvent.Key.keyval ev in
+ if k = GdkKeysyms._Escape then
+ begin
+ let (v,b,_,stop) = last_find () in
+ find_w#misc#hide();
+ v#coerce#misc#grab_focus();
+ true
+ end
+ else if k = GdkKeysyms._Return then
+ begin
+ close_find();
+ true
+ end
+ else if List.mem `CONTROL s && k = GdkKeysyms._f then
+ begin
+ find_again_forward ();
+ true
+ end
+ else if List.mem `CONTROL s && k = GdkKeysyms._b then
+ begin
+ find_again_backward ();
+ true
+ end
+ else false (* to let default callback execute *)
+ in
+ let find_f ~backward () =
+ search_backward := backward;
+ find_w#show ();
+ find_w#present ();
+ find_entry#misc#grab_focus ()
+ in
+ let find_i = edit_f#add_item "_Find in buffer"
+ ~key:GdkKeysyms._F
+ ~callback:(find_f ~backward:false)
+ in
+ let find_back_i = edit_f#add_item "Find _backwards"
+ ~key:GdkKeysyms._B
+ ~callback:(find_f ~backward:true)
+ in
+ let _ = close_find_button#connect#clicked close_find in
+ let _ = replace_button#connect#clicked do_replace in
+ let _ = replace_find_button#connect#clicked do_replace_find in
+ let _ = find_again_button#connect#clicked find_again_forward in
+ let _ = find_again_backward_button#connect#clicked find_again_backward in
+ let _ = find_entry#connect#changed do_find in
+ let _ = find_entry#event#connect#key_press ~callback:key_find in
+ let _ = find_w#event#connect#delete (fun _ -> find_w#misc#hide(); true) in
+(*
+ let search_if = edit_f#add_item "Search _forward"
+ ~key:GdkKeysyms._greater
+ in
+ let search_ib = edit_f#add_item "Search _backward"
+ ~key:GdkKeysyms._less
+ in
+*)
+(*
+ let complete_i = edit_f#add_item "_Complete"
+ ~key:GdkKeysyms._comma
+ ~callback:
+ (do_if_not_computing
+ (fun b ->
+ let v = out_some (get_current_view ()).analyzed_view
+
+ in v#complete_at_offset
+ ((v#view#buffer#get_iter `SEL_BOUND)#offset)
+ ))
+ in
+ complete_i#misc#set_state `INSENSITIVE;
+*)
+
+ ignore(edit_f#add_item "Complete Word" ~key:GdkKeysyms._slash ~callback:
+ (do_if_not_computing "complete word"
+ (fun () ->
+ ignore (
+ let av = out_some ((get_current_view()).analyzed_view) in
+ av#complete_at_offset (av#get_insert)#offset
+ ))));
+
+ ignore(edit_f#add_separator ());
+ (* external editor *)
+ let _ =
+ edit_f#add_item "External editor" ~callback:
+ (fun () ->
+ let av = out_some ((get_current_view()).analyzed_view) in
+ match av#filename with
+ | None -> ()
+ | Some f ->
+ save_f ();
+ let l,r = !current.cmd_editor in
+ let _ = run_command av#insert_message (l ^ f ^ r) in
+ av#revert)
+ in
+ let _ = edit_f#add_separator () in
+ (* Preferences *)
+ let reset_revert_timer () =
+ disconnect_revert_timer ();
+ if !current.global_auto_revert then
+ revert_timer := Some
+ (GMain.Timeout.add ~ms:!current.global_auto_revert_delay
+ ~callback:
+ (fun () ->
+ do_if_not_computing "revert" (fun () -> revert_f ()) ();
+ true))
+ in reset_revert_timer (); (* to enable statup preferences timer *)
+
+ let auto_save_f () =
+ Vector.iter
+ (function
+ {view = view ; analyzed_view = Some av} as full ->
+ (try
+ av#auto_save
+ with _ -> ())
+ | _ -> ()
+ )
+ input_views
+ in
+
+ let reset_auto_save_timer () =
+ disconnect_auto_save_timer ();
+ if !current.auto_save then
+ auto_save_timer := Some
+ (GMain.Timeout.add ~ms:!current.auto_save_delay
+ ~callback:
+ (fun () ->
+ do_if_not_computing "autosave" (fun () -> auto_save_f ()) ();
+ true))
+ in reset_auto_save_timer (); (* to enable statup preferences timer *)
+
+
+ let edit_prefs_m =
+ edit_f#add_item "_Preferences"
+ ~callback:(fun () -> configure ();reset_revert_timer ())
+ in
+(*
+ let save_prefs_m =
+ configuration_factory#add_item "_Save preferences"
+ ~callback:(fun () -> save_pref ())
+ in
+*)
+ (* Navigation Menu *)
+ let navigation_menu = factory#add_submenu "_Navigation" in
+ let navigation_factory =
+ new GMenu.factory navigation_menu
+ ~accel_path:"<CoqIde MenuBar>/Navigation/"
+ ~accel_group
+ ~accel_modi:!current.modifier_for_navigation
+ in
+ let do_or_activate f () =
+ let current = get_current_view () in
+ let analyzed_view = out_some current.analyzed_view in
+ if analyzed_view#is_active then
+ ignore (f analyzed_view)
+ else
+ begin
+ !flash_info "New proof started";
+ activate_input (notebook ())#current_page;
+ ignore (f analyzed_view)
+ end
+ in
+
+ let do_or_activate f =
+ do_if_not_computing "do_or_activate" (do_or_activate (fun av -> f av ; !pop_info();!push_info (Coq.current_status())))
+ in
+
+ let add_to_menu_toolbar text ~tooltip ?key ~callback icon =
+ begin
+ match key with None -> ()
+ | Some key -> ignore (navigation_factory#add_item text ~key ~callback)
+ end;
+ ignore (toolbar#insert_button
+ ~tooltip
+ ~text:tooltip
+ ~icon:(stock_to_widget ~size:`LARGE_TOOLBAR icon)
+ ~callback
+ ())
+ in
+ add_to_menu_toolbar
+ "_Save"
+ ~tooltip:"Save current buffer"
+ (* ~key:GdkKeysyms._Down *)
+ ~callback:save_f
+ `SAVE;
+ add_to_menu_toolbar
+ "_Forward"
+ ~tooltip:"Forward one command"
+ ~key:GdkKeysyms._Down
+ ~callback:(do_or_activate (fun a -> a#process_next_phrase true true true))
+ `GO_DOWN;
+ add_to_menu_toolbar "_Backward"
+ ~tooltip:"Backward one command"
+ ~key:GdkKeysyms._Up
+ ~callback:(do_or_activate (fun a -> a#undo_last_step))
+ `GO_UP;
+(*
+ add_to_menu_toolbar
+ "_Forward to"
+ ~tooltip:"Forward to"
+ ~key:GdkKeysyms._Right
+ ~callback:(do_or_activate (fun a -> a#process_until_insert_or_error))
+ `GOTO_LAST;
+ add_to_menu_toolbar
+ "_Backward to"
+ ~tooltip:"Backward to"
+ ~key:GdkKeysyms._Left
+ ~callback:(do_or_activate (fun a-> a#backtrack_to_insert))
+ `GOTO_FIRST;
+*)
+ add_to_menu_toolbar
+ "_Go to"
+ ~tooltip:"Go to cursor"
+ ~key:GdkKeysyms._Right
+ ~callback:(do_or_activate (fun a-> a#go_to_insert))
+ `JUMP_TO;
+ add_to_menu_toolbar
+ "_Start"
+ ~tooltip:"Go to start"
+ ~key:GdkKeysyms._Home
+ ~callback:(do_or_activate (fun a -> a#reset_initial))
+ `GOTO_TOP;
+ add_to_menu_toolbar
+ "_End"
+ ~tooltip:"Go to end"
+ ~key:GdkKeysyms._End
+ ~callback:(do_or_activate (fun a -> a#process_until_end_or_error))
+ `GOTO_BOTTOM;
+ add_to_menu_toolbar "_Interrupt"
+ ~tooltip:"Interrupt computations"
+ ~key:GdkKeysyms._Break
+ ~callback:break
+ `STOP
+ ;
+
+ (* Tactics Menu *)
+ let tactics_menu = factory#add_submenu "_Try Tactics" in
+ let tactics_factory =
+ new GMenu.factory tactics_menu
+ ~accel_path:"<CoqIde MenuBar>/Tactics/"
+ ~accel_group
+ ~accel_modi:!current.modifier_for_tactics
+ in
+ let do_if_active_raw f () =
+ let current = get_current_view () in
+ let analyzed_view = out_some current.analyzed_view in
+ if analyzed_view#is_active then ignore (f analyzed_view)
+ in
+ let do_if_active f = do_if_not_computing "do_if_active" (do_if_active_raw f) in
+
+(*
+ let blaster_i =
+ tactics_factory#add_item "_Blaster"
+ ~key:GdkKeysyms._b
+ ~callback: (do_if_active_raw (fun a -> a#blaster ()))
+ (* Custom locking mechanism! *)
+ in
+ blaster_i#misc#set_state `INSENSITIVE;
+*)
+
+ ignore (tactics_factory#add_item "_auto"
+ ~key:GdkKeysyms._a
+ ~callback:(do_if_active (fun a -> a#insert_command "progress auto.\n" "auto.\n"))
+ );
+ ignore (tactics_factory#add_item "_auto with *"
+ ~key:GdkKeysyms._asterisk
+ ~callback:(do_if_active (fun a -> a#insert_command
+ "progress auto with *.\n"
+ "auto with *.\n")));
+ ignore (tactics_factory#add_item "_eauto"
+ ~key:GdkKeysyms._e
+ ~callback:(do_if_active (fun a -> a#insert_command
+ "progress eauto.\n"
+ "eauto.\n"))
+ );
+ ignore (tactics_factory#add_item "_eauto with *"
+ ~key:GdkKeysyms._ampersand
+ ~callback:(do_if_active (fun a -> a#insert_command
+ "progress eauto with *.\n"
+ "eauto with *.\n"))
+ );
+ ignore (tactics_factory#add_item "_intuition"
+ ~key:GdkKeysyms._i
+ ~callback:(do_if_active (fun a -> a#insert_command
+ "progress intuition.\n"
+ "intuition.\n"))
+ );
+ ignore (tactics_factory#add_item "_omega"
+ ~key:GdkKeysyms._o
+ ~callback:(do_if_active (fun a -> a#insert_command
+ "omega.\n" "omega.\n"))
+ );
+ ignore (tactics_factory#add_item "_simpl"
+ ~key:GdkKeysyms._s
+ ~callback:(do_if_active (fun a -> a#insert_command "progress simpl.\n" "simpl.\n" ))
+ );
+ ignore (tactics_factory#add_item "_tauto"
+ ~key:GdkKeysyms._p
+ ~callback:(do_if_active (fun a -> a#insert_command "tauto.\n" "tauto.\n" ))
+ );
+ ignore (tactics_factory#add_item "_trivial"
+ ~key:GdkKeysyms._v
+ ~callback:(do_if_active( fun a -> a#insert_command "progress trivial.\n" "trivial.\n" ))
+ );
+
+
+ ignore (toolbar#insert_button
+ ~tooltip:"Proof Wizard"
+ ~text:"Wizard"
+ ~icon:(stock_to_widget ~size:`LARGE_TOOLBAR `DIALOG_INFO)
+ ~callback:(do_if_active (fun a -> a#tactic_wizard
+ !current.automatic_tactics
+ ))
+ ());
+
+ ignore (tactics_factory#add_item "<Proof _Wizard>"
+ ~key:GdkKeysyms._dollar
+ ~callback:(do_if_active (fun a -> a#tactic_wizard
+ !current.automatic_tactics
+ ))
+ );
+
+ ignore (tactics_factory#add_separator ());
+ let add_simple_template (factory: GMenu.menu GMenu.factory)
+ (menu_text, text) =
+ let text =
+ let l = String.length text - 1 in
+ if String.get text l = '.'
+ then text ^"\n"
+ else text ^" "
+ in
+ ignore (factory#add_item menu_text
+ ~callback:
+ (do_if_not_computing "simple template"
+ (fun () -> let {view = view } = get_current_view () in
+ ignore (view#buffer#insert_interactive text))))
+ in
+ List.iter
+ (fun l ->
+ match l with
+ | [] -> ()
+ | [s] -> add_simple_template tactics_factory ("_"^s, s)
+ | s::_ ->
+ let a = "_@..." in
+ a.[1] <- s.[0];
+ let f = tactics_factory#add_submenu a in
+ let ff = new GMenu.factory f ~accel_group in
+ List.iter
+ (fun x ->
+ add_simple_template
+ ff
+ ((String.sub x 0 1)^
+ "_"^
+ (String.sub x 1 (String.length x - 1)),
+ x))
+ l
+ )
+ Coq_commands.tactics;
+
+ (* Templates Menu *)
+ let templates_menu = factory#add_submenu "Te_mplates" in
+ let templates_factory = new GMenu.factory templates_menu
+ ~accel_path:"<CoqIde MenuBar>/Templates/"
+ ~accel_group
+ ~accel_modi:!current.modifier_for_templates
+ in
+ let add_complex_template (menu_text, text, offset, len, key) =
+ (* Templates/Lemma *)
+ let callback = do_if_not_computing "complex template"
+ (fun () ->
+ let {view = view } = get_current_view () in
+ if view#buffer#insert_interactive text then begin
+ let iter = view#buffer#get_iter_at_mark `INSERT in
+ ignore (iter#nocopy#backward_chars offset);
+ view#buffer#move_mark `INSERT iter;
+ ignore (iter#nocopy#backward_chars len);
+ view#buffer#move_mark `SEL_BOUND iter;
+ end)
+ in
+ ignore (templates_factory#add_item menu_text ~callback ?key)
+ in
+ add_complex_template
+ ("_Lemma __", "Lemma new_lemma : .\nProof.\n\nSave.\n",
+ 19, 9, Some GdkKeysyms._L);
+ add_complex_template
+ ("_Theorem __", "Theorem new_theorem : .\nProof.\n\nSave.\n",
+ 19, 11, Some GdkKeysyms._T);
+ add_complex_template
+ ("_Definition __", "Definition ident := .\n",
+ 6, 5, Some GdkKeysyms._D);
+ add_complex_template
+ ("_Inductive __", "Inductive ident : :=\n | : .\n",
+ 14, 5, Some GdkKeysyms._I);
+ add_complex_template
+ ("_Fixpoint __", "Fixpoint ident (_ : _) {struct _} : _ :=\n.\n",
+ 29, 5, Some GdkKeysyms._F);
+ add_complex_template("_Scheme __",
+ "Scheme new_scheme := Induction for _ Sort _
+with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
+
+ (* Template for match *)
+ let callback () =
+ let w = get_current_word () in
+ try
+ let cases = Coq.make_cases w
+ in
+ let print c = function
+ | [x] -> Format.fprintf c " | %s => _@\n" x
+ | x::l -> Format.fprintf c " | (%s%a) => _@\n" x
+ (print_list (fun c s -> Format.fprintf c " %s" s)) l
+ | [] -> assert false
+ in
+ let b = Buffer.create 1024 in
+ let fmt = Format.formatter_of_buffer b in
+ Format.fprintf fmt "@[match var with@\n%aend@]@."
+ (print_list print) cases;
+ let s = Buffer.contents b in
+ prerr_endline s;
+ let {view = view } = get_current_view () in
+ ignore (view#buffer#delete_selection ());
+ let m = view#buffer#create_mark
+ (view#buffer#get_iter `INSERT)
+ in
+ if view#buffer#insert_interactive s then
+ let i = view#buffer#get_iter (`MARK m) in
+ let _ = i#nocopy#forward_chars 9 in
+ view#buffer#place_cursor i;
+ view#buffer#move_mark ~where:(i#backward_chars 3)
+ `SEL_BOUND
+ with Not_found -> !flash_info "Not an inductive type"
+ in
+ ignore (templates_factory#add_item "match ..."
+ ~key:GdkKeysyms._C
+ ~callback
+ );
+
+(*
+ let add_simple_template (factory: GMenu.menu GMenu.factory)
+ (menu_text, text) =
+ let text =
+ let l = String.length text - 1 in
+ if String.get text l = '.'
+ then text ^"\n"
+ else text ^" "
+ in
+ ignore (factory#add_item menu_text
+ ~callback:
+ (do_if_not_computing "simple template"
+ (fun () -> let {view = view } = get_current_view () in
+ ignore (view#buffer#insert_interactive text))))
+ in
+*)
+ ignore (templates_factory#add_separator ());
+(*
+ List.iter (add_simple_template templates_factory)
+ [ "_auto", "auto ";
+ "_auto with *", "auto with * ";
+ "_eauto", "eauto ";
+ "_eauto with *", "eauto with * ";
+ "_intuition", "intuition ";
+ "_omega", "omega ";
+ "_simpl", "simpl ";
+ "_tauto", "tauto ";
+ "tri_vial", "trivial ";
+ ];
+ ignore (templates_factory#add_separator ());
+*)
+ List.iter
+ (fun l ->
+ match l with
+ | [] -> ()
+ | [s] -> add_simple_template templates_factory ("_"^s, s)
+ | s::_ ->
+ let a = "_@..." in
+ a.[1] <- s.[0];
+ let f = templates_factory#add_submenu a in
+ let ff = new GMenu.factory f ~accel_group in
+ List.iter
+ (fun x ->
+ add_simple_template
+ ff
+ ((String.sub x 0 1)^
+ "_"^
+ (String.sub x 1 (String.length x - 1)),
+ x))
+ l
+ )
+ Coq_commands.commands;
+
+ (* Queries Menu *)
+ let queries_menu = factory#add_submenu "_Queries" in
+ let queries_factory = new GMenu.factory queries_menu ~accel_group
+ ~accel_path:"<CoqIde MenuBar>/Queries"
+ ~accel_modi:[]
+ in
+
+ (* Command/Show commands *)
+ let _ =
+ queries_factory#add_item "_SearchAbout " ~key:GdkKeysyms._F2
+ ~callback:(fun () -> let term = get_current_word () in
+ (Command_windows.command_window ())#new_command
+ ~command:"SearchAbout"
+ ~term
+ ())
+ in
+ let _ =
+ queries_factory#add_item "_Check " ~key:GdkKeysyms._F3
+ ~callback:(fun () -> let term = get_current_word () in
+ (Command_windows.command_window ())#new_command
+ ~command:"Check"
+ ~term
+ ())
+ in
+ let _ =
+ queries_factory#add_item "_Print " ~key:GdkKeysyms._F4
+ ~callback:(fun () -> let term = get_current_word () in
+ (Command_windows.command_window ())#new_command
+ ~command:"Print"
+ ~term
+ ())
+ in
+
+ (* Externals *)
+ let externals_menu = factory#add_submenu "_Compile" in
+ let externals_factory = new GMenu.factory externals_menu
+ ~accel_path:"<CoqIde MenuBar>/Compile/"
+ ~accel_group
+ ~accel_modi:[]
+ in
+
+ (* Command/Compile Menu *)
+ let compile_f () =
+ let v = get_current_view () in
+ let av = out_some v.analyzed_view in
+ save_f ();
+ match av#filename with
+ | None ->
+ !flash_info "Active buffer has no name"
+ | Some f ->
+ let s,res = run_command
+ av#insert_message
+ (!current.cmd_coqc ^ " " ^ f)
+ in
+ if s = Unix.WEXITED 0 then
+ !flash_info (f ^ " successfully compiled")
+ else begin
+ !flash_info (f ^ " failed to compile");
+ activate_input (notebook ())#current_page;
+ av#process_until_end_or_error;
+ av#insert_message "Compilation output:\n";
+ av#insert_message res
+ end
+ in
+ let compile_m =
+ externals_factory#add_item "_Compile Buffer" ~callback:compile_f
+ in
+
+ (* Command/Make Menu *)
+ let make_f () =
+ let v = get_active_view () in
+ let av = out_some v.analyzed_view in
+(*
+ save_f ();
+*)
+ av#insert_message "Command output:\n";
+ let s,res = run_command av#insert_message !current.cmd_make in
+ last_make := res;
+ last_make_index := 0;
+ !flash_info (!current.cmd_make ^ if s = Unix.WEXITED 0 then " succeeded" else " failed")
+ in
+ let make_m = externals_factory#add_item "_Make"
+ ~key:GdkKeysyms._F6
+ ~callback:make_f
+ in
+
+
+ (* Compile/Next Error *)
+ let next_error () =
+ try
+ let file,line,start,stop,error_msg = search_next_error () in
+ load file;
+ let v = get_current_view () in
+ let av = out_some v.analyzed_view in
+ let input_buffer = v.view#buffer in
+(*
+ let init = input_buffer#start_iter in
+ let i = init#forward_lines (line-1) in
+*)
+(*
+ let convert_pos = byte_offset_to_char_offset phrase in
+ let start = convert_pos start in
+ let stop = convert_pos stop in
+*)
+(*
+ let starti = i#forward_chars start in
+ let stopi = i#forward_chars stop in
+*)
+ let starti = input_buffer#get_iter_at_byte ~line:(line-1) start in
+ let stopi = input_buffer#get_iter_at_byte ~line:(line-1) stop in
+ input_buffer#apply_tag_by_name "error"
+ ~start:starti
+ ~stop:stopi;
+ input_buffer#place_cursor starti;
+ av#set_message error_msg;
+ v.view#misc#grab_focus ()
+ with Not_found ->
+ last_make_index := 0;
+ let v = get_current_view () in
+ let av = out_some v.analyzed_view in
+ av#set_message "No more errors.\n"
+ in
+ let next_error_m =
+ externals_factory#add_item "_Next error"
+ ~key:GdkKeysyms._F7
+ ~callback:next_error in
+
+
+ (* Command/CoqMakefile Menu*)
+ let coq_makefile_f () =
+ let v = get_active_view () in
+ let av = out_some v.analyzed_view in
+ let s,res = run_command av#insert_message !current.cmd_coqmakefile in
+ !flash_info
+ (!current.cmd_coqmakefile ^ if s = Unix.WEXITED 0 then " succeeded" else " failed")
+ in
+ let _ = externals_factory#add_item "_Make makefile" ~callback:coq_makefile_f
+ in
+ (* Windows Menu *)
+ let configuration_menu = factory#add_submenu "_Windows" in
+ let configuration_factory = new GMenu.factory configuration_menu ~accel_path:"<CoqIde MenuBar>/Windows" ~accel_group
+ in
+ let queries_show_m =
+ configuration_factory#add_item
+ "Show _Query Window"
+ (*
+ ~key:GdkKeysyms._F12
+ *)
+ ~callback:(Command_windows.command_window ())#window#present
+ in
+ let toolbar_show_m =
+ configuration_factory#add_item
+ "Show/Hide _Toolbar"
+ ~callback:(fun () ->
+ !current.show_toolbar <- not !current.show_toolbar;
+ !show_toolbar !current.show_toolbar)
+ in
+ let detach_menu = configuration_factory#add_item
+ "Detach _Script Window"
+ ~callback:
+ (do_if_not_computing "detach script window"
+ (fun () ->
+ let nb = notebook () in
+ if nb#misc#toplevel#get_oid=w#coerce#get_oid then
+ begin
+ let nw = GWindow.window ~show:true () in
+ let parent = out_some nb#misc#parent in
+ ignore (nw#connect#destroy
+ ~callback:
+ (fun () -> nb#misc#reparent parent));
+ nw#add_accel_group accel_group;
+ nb#misc#reparent nw#coerce
+ end
+ ))
+ in
+ let detach_current_view =
+ configuration_factory#add_item
+ "Detach _View"
+ ~callback:
+ (do_if_not_computing "detach view"
+ (fun () ->
+ match get_current_view () with
+ | {view=v;analyzed_view=Some av} ->
+ let w = GWindow.window ~show:true
+ ~width:(!current.window_width/2)
+ ~height:(!current.window_height)
+ ~title:(match av#filename with
+ | None -> "*Unnamed*"
+ | Some f -> f)
+ ()
+ in
+ let sb = GBin.scrolled_window
+ ~packing:w#add ()
+ in
+ let nv = GText.view
+ ~buffer:v#buffer
+ ~packing:sb#add
+ ()
+ in
+ nv#misc#modify_font
+ !current.text_font;
+ ignore (w#connect#destroy
+ ~callback:
+ (fun () -> av#remove_detached_view w));
+ av#add_detached_view w
+ | _ -> ()
+
+ ))
+ in
+ (* Help Menu *)
+
+ let help_menu = factory#add_submenu "_Help" in
+ let help_factory = new GMenu.factory help_menu
+ ~accel_path:"<CoqIde MenuBar>/Help/"
+ ~accel_modi:[]
+ ~accel_group in
+ let _ = help_factory#add_item "Browse Coq _Manual"
+ ~callback:
+ (fun () ->
+ let av = out_some ((get_current_view ()).analyzed_view) in
+ browse av#insert_message (!current.doc_url ^ "main.html")) in
+ let _ = help_factory#add_item "Browse Coq _Library"
+ ~callback:
+ (fun () ->
+ let av = out_some ((get_current_view ()).analyzed_view) in
+ browse av#insert_message !current.library_url) in
+ let _ =
+ help_factory#add_item "Help for _keyword" ~key:GdkKeysyms._F1
+ ~callback:(fun () ->
+ let av = out_some ((get_current_view ()).analyzed_view) in
+ av#help_for_keyword ())
+ in
+ let _ = help_factory#add_separator () in
+(*
+ let faq_m = help_factory#add_item "_FAQ" in
+*)
+ let about_m = help_factory#add_item "_About" in
+
+ (* End of menu *)
+
+ (* The vertical Separator between Scripts and Goals *)
+ let hb = GPack.paned `HORIZONTAL ~border_width:3 ~packing:vbox#add () in
+ _notebook := Some (GPack.notebook ~scrollable:true
+ ~packing:hb#add1
+ ());
+ let nb = notebook () in
+ let fr2 = GBin.frame ~shadow_type:`ETCHED_OUT ~packing:hb#add2 () in
+ let hb2 = GPack.paned `VERTICAL ~border_width:3 ~packing:fr2#add () in
+ let sw2 = GBin.scrolled_window
+ ~vpolicy:`AUTOMATIC
+ ~hpolicy:`AUTOMATIC
+ ~packing:(hb2#add) () in
+ let sw3 = GBin.scrolled_window
+ ~vpolicy:`AUTOMATIC
+ ~hpolicy:`AUTOMATIC
+ ~packing:(hb2#add) () in
+ let lower_hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in
+ let status_bar = GMisc.statusbar ~packing:(lower_hbox#pack ~expand:true) ()
+ in
+ let search_lbl = GMisc.label ~text:"Search:"
+ ~show:false
+ ~packing:(lower_hbox#pack ~expand:false) ()
+ in
+ let search_history = ref [] in
+ let search_input = GEdit.combo ~popdown_strings:!search_history
+ ~enable_arrow_keys:true
+ ~show:false
+ ~packing:(lower_hbox#pack ~expand:false) ()
+ in
+ search_input#disable_activate ();
+ let ready_to_wrap_search = ref false in
+
+ let start_of_search = ref None in
+ let start_of_found = ref None in
+ let end_of_found = ref None in
+ let search_forward = ref true in
+ let matched_word = ref None in
+
+ let memo_search () =
+ matched_word := Some search_input#entry#text
+
+(* if not (List.mem search_input#entry#text !search_history) then
+ (search_history :=
+ search_input#entry#text::!search_history;
+ search_input#set_popdown_strings !search_history);
+ start_of_search := None;
+ ready_to_wrap_search := false
+*)
+
+ in
+ let end_search () =
+ prerr_endline "End Search";
+ memo_search ();
+ let v = (get_current_view ()).view in
+ v#buffer#move_mark `SEL_BOUND (v#buffer#get_iter_at_mark `INSERT);
+ v#coerce#misc#grab_focus ();
+ search_input#entry#set_text "";
+ search_lbl#misc#hide ();
+ search_input#misc#hide ()
+ in
+ let end_search_focus_out () =
+ prerr_endline "End Search(focus out)";
+ memo_search ();
+ let v = (get_current_view ()).view in
+ v#buffer#move_mark `SEL_BOUND (v#buffer#get_iter_at_mark `INSERT);
+ search_input#entry#set_text "";
+ search_lbl#misc#hide ();
+ search_input#misc#hide ()
+ in
+ ignore (search_input#entry#connect#activate ~callback:end_search);
+ ignore (search_input#entry#event#connect#key_press
+ ~callback:(fun k -> let kv = GdkEvent.Key.keyval k in
+ if
+ kv = GdkKeysyms._Right
+ || kv = GdkKeysyms._Up
+ || kv = GdkKeysyms._Left
+ || (kv = GdkKeysyms._g
+ && (List.mem `CONTROL (GdkEvent.Key.state k)))
+ then end_search ();
+ false));
+ ignore (search_input#entry#event#connect#focus_out
+ ~callback:(fun _ -> end_search_focus_out (); false));
+ to_do_on_page_switch :=
+ (fun i ->
+ start_of_search := None;
+ ready_to_wrap_search:=false)::!to_do_on_page_switch;
+
+(* TODO : make it work !!! *)
+ let rec search_f () =
+ search_lbl#misc#show ();
+ search_input#misc#show ();
+
+ prerr_endline "search_f called";
+ if !start_of_search = None then begin
+ (* A full new search is starting *)
+ start_of_search :=
+ Some ((get_current_view ()).view#buffer#create_mark
+ ((get_current_view ()).view#buffer#get_iter_at_mark `INSERT));
+ start_of_found := !start_of_search;
+ end_of_found := !start_of_search;
+ matched_word := Some "";
+ end;
+ let txt = search_input#entry#text in
+ let v = (get_current_view ()).view in
+ let iit = v#buffer#get_iter_at_mark `SEL_BOUND
+ and insert_iter = v#buffer#get_iter_at_mark `INSERT
+ in
+ prerr_endline ("SELBOUND="^(string_of_int iit#offset));
+ prerr_endline ("INSERT="^(string_of_int insert_iter#offset));
+
+ (match
+ if !search_forward then iit#forward_search txt
+ else let npi = iit#forward_chars (Glib.Utf8.length txt) in
+ match
+ (npi#offset = (v#buffer#get_iter_at_mark `INSERT)#offset),
+ (let t = iit#get_text ~stop:npi in
+ !flash_info (t^"\n"^txt);
+ t = txt)
+ with
+ | true,true ->
+ (!flash_info "T,T";iit#backward_search txt)
+ | false,true -> !flash_info "F,T";Some (iit,npi)
+ | _,false ->
+ (iit#backward_search txt)
+
+ with
+ | None ->
+ if !ready_to_wrap_search then begin
+ ready_to_wrap_search := false;
+ !flash_info "Search wrapped";
+ v#buffer#place_cursor
+ (if !search_forward then v#buffer#start_iter else
+ v#buffer#end_iter);
+ search_f ()
+ end else begin
+ if !search_forward then !flash_info "Search at end"
+ else !flash_info "Search at start";
+ ready_to_wrap_search := true
+ end
+ | Some (start,stop) ->
+ prerr_endline "search: before moving marks";
+ prerr_endline ("SELBOUND="^(string_of_int (v#buffer#get_iter_at_mark `SEL_BOUND)#offset));
+ prerr_endline ("INSERT="^(string_of_int (v#buffer#get_iter_at_mark `INSERT)#offset));
+
+ v#buffer#move_mark `SEL_BOUND start;
+ v#buffer#move_mark `INSERT stop;
+ prerr_endline "search: after moving marks";
+ prerr_endline ("SELBOUND="^(string_of_int (v#buffer#get_iter_at_mark `SEL_BOUND)#offset));
+ prerr_endline ("INSERT="^(string_of_int (v#buffer#get_iter_at_mark `INSERT)#offset));
+ v#scroll_to_mark `SEL_BOUND
+ )
+ in
+ ignore (search_input#entry#event#connect#key_release
+ ~callback:
+ (fun ev ->
+ if GdkEvent.Key.keyval ev = GdkKeysyms._Escape then begin
+ let v = (get_current_view ()).view in
+ (match !start_of_search with
+ | None ->
+ prerr_endline "search_key_rel: Placing sel_bound";
+ v#buffer#move_mark
+ `SEL_BOUND
+ (v#buffer#get_iter_at_mark `INSERT)
+ | Some mk -> let it = v#buffer#get_iter_at_mark
+ (`MARK mk) in
+ prerr_endline "search_key_rel: Placing cursor";
+ v#buffer#place_cursor it;
+ start_of_search := None
+ );
+ search_input#entry#set_text "";
+ v#coerce#misc#grab_focus ();
+ end;
+ false
+ ));
+ ignore (search_input#entry#connect#changed search_f);
+
+(*
+ ignore (search_if#connect#activate
+ ~callback:(fun b ->
+ search_forward:= true;
+ search_input#entry#coerce#misc#grab_focus ();
+ search_f ();
+ )
+ );
+ ignore (search_ib#connect#activate
+ ~callback:(fun b ->
+ search_forward:= false;
+
+ (* Must restore the SEL_BOUND mark after
+ grab_focus ! *)
+ let v = (get_current_view ()).view in
+ let old_sel = v#buffer#get_iter_at_mark `SEL_BOUND
+ in
+ search_input#entry#coerce#misc#grab_focus ();
+ v#buffer#move_mark `SEL_BOUND old_sel;
+ search_f ();
+ ));
+*)
+ let status_context = status_bar#new_context "Messages" in
+ let flash_context = status_bar#new_context "Flash" in
+ ignore (status_context#push "Ready");
+ status := Some status_bar;
+ push_info := (fun s -> ignore (status_context#push s));
+ pop_info := (fun () -> status_context#pop ());
+ flash_info := (fun ?(delay=5000) s -> flash_context#flash ~delay s);
+
+ (* Location display *)
+ let l = GMisc.label
+ ~text:"Line: 1 Char: 1"
+ ~packing:lower_hbox#pack () in
+ l#coerce#misc#set_name "location";
+ set_location := l#set_text;
+
+ (* Progress Bar *)
+ pulse :=
+ (let pb = GRange.progress_bar ~pulse_step:0.2 ~packing:lower_hbox#pack ()
+ in pb#set_text "CoqIde started";pb)#pulse;
+ let tv2 = GText.view ~packing:(sw2#add) () in
+ tv2#misc#set_name "GoalWindow";
+ let _ = tv2#set_editable false in
+ let tb2 = tv2#buffer in
+ let tv3 = GText.view ~packing:(sw3#add) () in
+ tv2#misc#set_name "MessageWindow";
+ let _ = tv2#set_wrap_mode `CHAR in
+ let _ = tv3#set_wrap_mode `WORD in
+ let _ = tv3#set_editable false in
+ let _ = GtkBase.Widget.add_events tv2#as_widget
+ [`ENTER_NOTIFY;`POINTER_MOTION] in
+ let _ = tv2#event#connect#motion_notify
+ ~callback:
+ (fun e ->
+ (do_if_not_computing "motion notify"
+ (fun e ->
+ let win = match tv2#get_window `WIDGET with
+ | None -> assert false
+ | Some w -> w
+ in
+ let x,y = Gdk.Window.get_pointer_location win in
+ let b_x,b_y = tv2#window_to_buffer_coords
+ ~tag:`WIDGET
+ ~x
+ ~y
+ in
+ let it = tv2#get_iter_at_location ~x:b_x ~y:b_y in
+ let tags = it#tags in
+ List.iter
+ ( fun t ->
+ ignore (GtkText.Tag.event
+ t#as_tag
+ tv2#as_widget
+ e
+ it#as_iter))
+ tags;
+ false)) e;
+ false)
+ in
+ change_font :=
+ (fun fd ->
+ tv2#misc#modify_font fd;
+ tv3#misc#modify_font fd;
+ Vector.iter
+ (fun {view=view} -> view#misc#modify_font fd)
+ input_views;
+ );
+ let about (b:GText.buffer) =
+ (try
+ let image = Filename.concat lib_ide "coq.png" in
+ let startup_image = GdkPixbuf.from_file image in
+ b#insert_pixbuf ~iter:b#start_iter
+ ~pixbuf:startup_image;
+ b#insert ~iter:b#start_iter "\t\t";
+ with _ -> ());
+ let about_string =
+ "\nCoqIDE: an Integrated Development Environment for Coq\n\
+ \nMain author : Benjamin Monate\
+ \nContributors : Jean-Christophe Filliâtre\
+ \n Pierre Letouzey, Claude Marché\n\
+ \nFeature wish or bug report: use Web interface\n\
+ \n\thttp://coq.inria.fr/bin/coq-bugs\n\
+ \nVersion information\
+ \n-------------------\n"
+ in
+ if Glib.Utf8.validate about_string
+ then b#insert about_string;
+ let coq_version = Coq.version () in
+ if Glib.Utf8.validate coq_version
+ then b#insert coq_version;
+
+ in
+ about tv2#buffer;
+ w#add_accel_group accel_group;
+ (* Remove default pango menu for textviews *)
+ ignore (tv2#event#connect#button_press ~callback:
+ (fun ev -> GdkEvent.Button.button ev = 3));
+ ignore (tv3#event#connect#button_press ~callback:
+ (fun ev -> GdkEvent.Button.button ev = 3));
+ tv2#misc#set_can_focus true;
+ tv3#misc#set_can_focus true;
+ ignore (tv2#buffer#create_mark
+ ~name:"end_of_conclusion"
+ tv2#buffer#start_iter);
+ ignore (tv3#buffer#create_tag
+ ~name:"error"
+ [`FOREGROUND "red"]);
+ w#show ();
+ message_view := Some tv3;
+ proof_view := Some tv2;
+ tv2#misc#modify_font !current.text_font;
+ tv3#misc#modify_font !current.text_font;
+ ignore (about_m#connect#activate
+ ~callback:(fun () -> tv2#buffer#set_text ""; about tv2#buffer));
+(*
+ ignore (faq_m#connect#activate
+ ~callback:(fun () ->
+ load (Filename.concat lib_ide "FAQ")));
+
+*)
+ resize_window := (fun () ->
+ w#resize
+ ~width:!current.window_width
+ ~height:!current.window_height);
+
+ ignore (w#misc#connect#size_allocate
+ (let old_w = ref 0
+ and old_h = ref 0 in
+ fun {Gtk.width=w;Gtk.height=h} ->
+ if !old_w <> w or !old_h <> h then
+ begin
+ old_h := h;
+ old_w := w;
+ hb#set_position (w/2);
+ hb2#set_position (h/2);
+ !current.window_height <- h;
+ !current.window_width <- w;
+ end
+ ));
+ ignore(nb#connect#switch_page
+ ~callback:
+ (fun i ->
+ prerr_endline ("switch_page: starts " ^ string_of_int i);
+ List.iter (function f -> f i) !to_do_on_page_switch;
+ prerr_endline "switch_page: success")
+ );
+ ignore(tv2#event#connect#enter_notify
+ (fun _ ->
+ if !current.contextual_menus_on_goal then
+ begin
+ let w = (out_some (get_active_view ()).analyzed_view) in
+ !push_info "Computing advanced goal's menus";
+ prerr_endline "Entering Goal Window. Computing Menus....";
+ w#show_goals_full;
+ prerr_endline "....Done with Goal menu";
+ !pop_info();
+ end;
+ false;
+ ));
+ if List.length files >=1 then
+ begin
+ List.iter (fun f ->
+ if Sys.file_exists f then load f else
+ if Filename.check_suffix f ".v"
+ then load f
+ else load (f^".v")) files;
+ activate_input 0
+ end
+ else
+ begin
+ let view = create_input_tab "*Unnamed Buffer*" in
+ let index = add_input_view {view = view;
+ analyzed_view = None;
+ }
+ in
+ (get_input_view index).analyzed_view <- Some (new analyzed_view index);
+ activate_input index;
+ set_tab_image index ~icon:`YES;
+ view#misc#modify_font !current.text_font
+ end;
+
+;;
+
+let start () =
+ let files = Coq.init () in
+ ignore_break ();
+ GtkMain.Rc.add_default_file (Filename.concat lib_ide ".coqide-gtk2rc");
+ (try
+ GtkMain.Rc.add_default_file (Filename.concat System.home ".coqide-gtk2rc");
+ with Not_found -> ());
+ ignore (GtkMain.Main.init ());
+ GtkData.AccelGroup.set_default_mod_mask
+ (Some [`CONTROL;`SHIFT;`MOD1;`MOD3;`MOD4]);
+ cb_ := Some (GData.clipboard Gdk.Atom.primary);
+ ignore (
+ Glib.Message.set_log_handler ~domain:"Gtk" ~levels:[`ERROR;`FLAG_FATAL;
+ `WARNING;`CRITICAL]
+ (fun ~level msg -> failwith ("Coqide internal error: " ^ msg)));
+ Command_windows.main ();
+ Blaster_window.main 9;
+ main files;
+ while true do
+ try
+ GtkThread.main ()
+ with
+ | Sys.Break -> prerr_endline "Interrupted." ; flush stderr
+ | e ->
+ Pervasives.prerr_endline ("CoqIde unexpected error:" ^ (Printexc.to_string e));
+ flush stderr;
+ crash_save 127
+ done
+