(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* 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 -> (bool*(Util.loc * Vernacexpr.vernac_expr)) option method set_message : string -> unit method show_pm_goal : 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 do_if_not_computing text f x = let threaded_task () = if Mutex.try_lock coq_computing then begin 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 () -> async !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)" in prerr_endline ("Launching thread " ^ text); ignore (Thread.create threaded_task ()) 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 (""^txt^""); 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 = (* TODO: avoid num and prime at the head of a word *) Glib.Unichar.isalnum c || c = underscore || c = prime 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 (is_word_char c) ) let inside_word it = let c = it#char in not (starts_word it) && not (ends_word it) && is_word_char c 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',_,_) | 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_pm_goal = proof_buffer#insert (Printf.sprintf " *** Declarative Mode ***\n"); try let (hyps,metas) = get_current_pm_goal () in List.iter (fun ((_,_,_,(s,_)) as _hyp) -> proof_buffer#insert (s^"\n")) hyps; proof_buffer#insert (String.make 38 '_' ^ "\n"); List.iter (fun (_,_,m) -> proof_buffer#insert (m^"\n")) metas; let my_mark = `NAME "end_of_conclusion" in proof_buffer#move_mark ~where:((proof_buffer#get_iter_at_mark `INSERT)) my_mark; ignore (proof_view#scroll_to_mark my_mark) with Not_found -> match Decl_mode.get_end_command (Pfedit.get_pftreestate ()) with Some endc -> proof_buffer#insert ("Subproof completed, now type "^endc^".") | None -> proof_buffer#insert "Proof completed." method show_goals = try proof_view#buffer#set_text ""; match Decl_mode.get_current_mode () with Decl_mode.Mode_none -> proof_buffer#insert (Coq.print_no_goal ()) | Decl_mode.Mode_tactic -> begin 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) end | Decl_mode.Mode_proof -> self#show_pm_goal 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 ""; match Decl_mode.get_current_mode () with Decl_mode.Mode_none -> proof_buffer#insert (Coq.print_no_goal ()) | Decl_mode.Mode_tactic -> begin match Coq.get_current_goals () with [] -> Util.anomaly "show_goals_full" | ((hyps,concl)::r) as s -> let last_shown_area = proof_buffer#create_tag [`BACKGROUND "light green"] in 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 end | Decl_mode.Mode_proof -> self#show_pm_goal with e -> prerr_endline (Printexc.to_string e) end method send_to_coq verbosely replace phrase show_output show_error localize = let display_output msg = self#insert_message (if show_output then msg else "") in let display_error e = let (s,loc) = Coq.process_exn e in assert (Glib.Utf8.validate s); self#insert_message s; message_view#misc#draw None; if localize then (match Util.option_map 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) in try full_goal_done <- false; prerr_endline "Send_to_coq starting now"; Decl_mode.clear_daimon_flag (); if replace then begin let r,info = Coq.interp_and_replace ("info " ^ phrase) in let complete = not (Decl_mode.get_daimon_flag ()) in let msg = read_stdout () in sync display_output msg; Some (complete,r) end else begin let r = Coq.interp verbosely phrase in let complete = not (Decl_mode.get_daimon_flag ()) in let msg = read_stdout () in sync display_output msg; Some (complete,r) end with e -> if show_error then sync display_error e; 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 _ = 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 = let get_next_phrase () = 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; 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; None | Some(start,stop) -> prerr_endline "process_next_phrase : to_process highlight"; 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"; Some((start,stop),start#get_slice ~stop) in let remove_tag (start,stop) = if do_highlight then begin input_buffer#remove_tag_by_name ~start ~stop "to_process" ; input_view#set_editable true; !pop_info (); end in let mark_processed complete (start,stop) ast = let b = input_buffer in b#move_mark ~where:stop (`NAME "start_of_input"); b#apply_tag_by_name (if complete then "processed" else "unjustified") ~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; remove_tag (start,stop) in begin match sync get_next_phrase () with None -> false | Some (loc,phrase) -> (match self#send_to_coq verbosely false phrase true true true with | Some (complete,ast) -> sync (mark_processed complete) loc ast; true | None -> sync remove_tag loc; false) end method insert_this_phrase_on_success show_output show_msg localize coqphrase insertphrase = let mark_processed complete ast = 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 (if complete then "processed" else "unjustified") ~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 _ -> ()*) in match self#send_to_coq false false coqphrase show_output show_msg localize with | Some (complete,ast) -> sync (mark_processed complete) ast; true | None -> sync (fun _ -> 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 sync (fun _ -> input_buffer#apply_tag_by_name ~start ~stop "to_process"; input_view#set_editable false) (); !push_info "Coq is computing"; let get_current () = if !current.stop_before then match self#find_phrase_starting_at self#get_start_of_input with | None -> self#get_start_of_input | Some (_, stop2) -> stop2 else begin self#get_start_of_input end in (try while ((stop#compare (get_current())>=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"); sync (fun _ -> 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 = sync (fun _ -> 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#remove_tag_by_name "unjustified" ~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 ()); sync (fun _ -> 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"; input_buffer#remove_tag_by_name ~start ~stop:self#get_start_of_input "unjustified"; 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"; input_buffer#remove_tag_by_name ~start ~stop:(input_buffer#get_iter_at_mark last_command.stop) "unjustified"; 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 ()); sync 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); sync 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); sync update_input () | { ast = (_, a) } when is_state_preserving a -> ignore (pop ()); sync 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 (); Decl_mode.check_not_proof_mode "No blaster in Proof mode"; let current_gls = try get_current_goals () with _ -> [] 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') (sync(fun () -> self#insert_command t'' t'')) in let set_current_goal (s,t) = c#set "Goal 1" s (fun () -> try_interptac ("progress "^t)) (sync(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 = async(fun _ -> self#clear_message)(); ignore (self#insert_this_phrase_on_success true false false cp ip) method tactic_wizard l = async(fun _ -> 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); match (out_some ((Vector.get input_views index).analyzed_view)) #filename with | None -> () | Some f -> let dir = Filename.dirname f in if not (is_in_loadpath dir) then begin ignore (Coq.interp false (Printf.sprintf "Add LoadPath \"%s\". " dir)) end 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 begin input_buffer#remove_tag_by_name ~start ~stop "processed"; input_buffer#remove_tag_by_name ~start ~stop "unjustified" end ) ); 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 _ = GMisc.label () in let v_box = GPack.hbox ~homogeneous:false () in let _ = GMisc.image ~packing:v_box#pack () in let _ = 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 (* Proof mode *) ~name:"unjustified" [`UNDERLINE `SINGLE ; `FOREGROUND "red"; `BACKGROUND "gold" ;`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 (try let icon_image = lib_ide_file "coq.ico" in let icon = GdkPixbuf.from_file icon_image in w#set_icon (Some icon) with _ -> ()); 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:"/" 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:"/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 -> 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} -> 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} -> (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" ~key:GdkKeysyms._W 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 _ = file_factory#add_item "_Print" ~key:GdkKeysyms._P ~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:"/Export/" file_export_m ~accel_group in let _ = file_export_factory#add_item "_Html" ~callback:(export_f "html") in let _ = file_export_factory#add_item "_LaTeX" ~callback:(export_f "latex") in let _ = file_export_factory#add_item "_Dvi" ~callback:(export_f "dvi") in let _ = 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 _ = 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:"/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: (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: (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 _ = 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 _ = 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 _ = 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 _ = edit_f#add_item "_Find in buffer" ~key:GdkKeysyms._F ~callback:(find_f ~backward:false) in let _ = 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: (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" (sync 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} -> (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" (sync auto_save_f) (); true)) in reset_auto_save_timer (); (* to enable statup preferences timer *) let _ = 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:"/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" ~callback:save_f `SAVE; add_to_menu_toolbar "_Close" ~tooltip:"Close current buffer" ~callback:close_f `CLOSE; 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 "_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:"/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 "" ~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: (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:"/Templates/" ~accel_group ~accel_modi:!current.modifier_for_templates in let add_complex_template (menu_text, text, offset, len, key) = (* Templates/Lemma *) let callback () = 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: (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:"/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 let _ = queries_factory#add_item "_Whelp Locate" ~callback:(fun () -> let term = get_current_word () in (Command_windows.command_window ())#new_command ~command:"Whelp Locate" ~term ()) in (* Externals *) let externals_menu = factory#add_submenu "_Compile" in let externals_factory = new GMenu.factory externals_menu ~accel_path:"/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 _ = 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 _ = 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 _ = 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:"/Windows" ~accel_group in let _ = configuration_factory#add_item "Show _Query Window" (* ~key:GdkKeysyms._F12 *) ~callback:(Command_windows.command_window ())#window#present in let _ = configuration_factory#add_item "Show/Hide _Toolbar" ~callback:(fun () -> !current.show_toolbar <- not !current.show_toolbar; !show_toolbar !current.show_toolbar) in let _ = configuration_factory#add_item "Detach _Script Window" ~callback: (do_if_not_computing "detach script window" (sync (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 _ = 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:"/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:5 ~packing:vbox#add () in let fr_notebook = GBin.frame ~shadow_type:`IN ~packing:hb#add1 () in _notebook := Some (GPack.notebook ~border_width:2 ~show_border:false ~scrollable:true ~packing:fr_notebook#add ()); let nb = notebook () in let hb2 = GPack.paned `VERTICAL ~packing:hb#add2 () in let fr_a = GBin.frame ~shadow_type:`IN ~packing:hb2#add () in let fr_b = GBin.frame ~shadow_type:`IN ~packing:hb2#add () in let sw2 = GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:(fr_a#add) () in let sw3 = GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:(fr_b#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 _ = 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 -> 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) 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 = lib_ide_file "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 (lib_ide_file "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; ;; (* This function check every half of second if GeoProof has send something on his private clipboard *) let rec check_for_geoproof_input () = let cb_Dr = GData.clipboard (Gdk.Atom.intern "_GeoProof") in while true do Thread.delay 0.1; let s = cb_Dr#text in (match s with Some s -> if s <> "Ack" then (get_current_view()).view#buffer#insert (s^"\n"); cb_Dr#set_text "Ack" | None -> () ); (* cb_Dr#clear does not work so i use : *) (* cb_Dr#set_text "Ack" *) done let start () = let files = Coq.init () in ignore_break (); GtkMain.Rc.add_default_file (lib_ide_file ".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 -> if level land Glib.Message.log_level `WARNING <> 0 then Pp.warning msg else failwith ("Coqide internal error: " ^ msg))); Command_windows.main (); Blaster_window.main 9; main files; if !Coq_config.with_geoproof then ignore (Thread.create check_for_geoproof_input ()); 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