(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* '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 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*reset_info) 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 end type viewable_script = {script : Undo.undoable_view; tab_label : GMisc.label; mutable filename : string; mutable encoding : string; proof_view : GText.view; message_view : GText.view; analyzed_view : analyzed_views; command_stack : (ide_info * Coq.reset_info) Stack.t; } let notebook_page_of_session {script=script;tab_label=bname;proof_view=proof;message_view=message} = let session_paned = GPack.paned `HORIZONTAL ~border_width:5 () in let script_frame = GBin.frame ~shadow_type:`IN ~packing:session_paned#add1 () in let script_scroll = GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:script_frame#add () in let state_paned = GPack.paned `VERTICAL ~packing:session_paned#add2 () in let proof_frame = GBin.frame ~shadow_type:`IN ~packing:state_paned#add1 () in let proof_scroll = GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:proof_frame#add () in let message_frame = GBin.frame ~shadow_type:`IN ~packing:state_paned#add2 () in let message_scroll = GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:message_frame#add () in let session_tab = GPack.hbox ~homogeneous:false () in let img = GMisc.image ~packing:session_tab#pack ~icon_size:`SMALL_TOOLBAR () in let _ = script#buffer#connect#modified_changed ~callback:(fun () -> if script#buffer#modified then img#set_stock `SAVE else img#set_stock `YES) in let _ = session_paned#misc#connect#size_allocate (let old_paned_width = ref 2 in let old_paned_height = ref 2 in (fun {Gtk.width=paned_width;Gtk.height=paned_height} -> if !old_paned_width <> paned_width || !old_paned_height <> paned_height then ( session_paned#set_position (session_paned#position * paned_width / !old_paned_width); state_paned#set_position (state_paned#position * paned_height / !old_paned_height); old_paned_width := paned_width; old_paned_height := paned_height; ))) in script_scroll#add script#coerce; proof_scroll#add proof#coerce; message_scroll#add message#coerce; session_tab#pack bname#coerce; img#set_stock `YES; session_paned#set_position 1; state_paned#set_position 1; (Some session_tab#coerce,None,session_paned#coerce) let session_notebook = Typed_notebook.create notebook_page_of_session ~border_width:2 ~show_border:false ~scrollable:true () let active_view = ref (~-1) let on_active_view f = if !active_view < 0 then failwith "no active view !" else f (session_notebook#get_nth_term !active_view) let cb = GData.clipboard Gdk.Atom.primary let last_cb_content = ref "" let update_notebook_pos () = let pos = match !current.vertical_tabs, !current.opposite_tabs with | false, false -> `TOP | false, true -> `BOTTOM | true , false -> `LEFT | true , true -> `RIGHT in session_notebook#set_tab_pos pos let set_active_view i = prerr_endline "entering set_active_view"; (try on_active_view (fun {tab_label=lbl} -> lbl#set_text lbl#text) with _ -> ()); session_notebook#goto_page i; let s = session_notebook#current_term in s.tab_label#set_use_markup true; s.tab_label#set_label (""^s.tab_label#text^""); active_view := i; prerr_endline "exiting set_active_view" let to_do_on_page_switch = ref [] 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);*) safe_prerr_endline "Trying to save all buffers in .crashcoqide files"; let count = ref 0 in List.iter (function {script=view; analyzed_view = av } -> (let filename = match av#filename with | None -> incr count; "Unnamed_coqscript_"^(string_of_int !count)^".crashcoqide" | Some f -> f^".crashcoqide" in try if try_export filename (view#buffer#get_text ()) then safe_prerr_endline ("Saved "^filename) else safe_prerr_endline ("Could not save "^filename) with _ -> safe_prerr_endline ("Could not save "^filename)) ) session_notebook#pages; safe_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 () = (* Beware: mutexes must be locked and unlocked in the same thread on at least FreeBSD (see bug #2431) *) if Mutex.try_lock coq_computing then begin prerr_endline "Getting lock"; try f x; prerr_endline "Releasing lock"; Mutex.unlock coq_computing; with e -> prerr_endline "Releasing lock (on error)"; Mutex.unlock coq_computing; raise e end else prerr_endline "Discarded order (computations are ongoing)" in prerr_endline ("Launching thread " ^ text); ignore (Glib.Timeout.add ~ms:300 ~callback: (fun () -> if Mutex.try_lock coq_computing then (Mutex.unlock coq_computing; false) else (pbar#pulse (); true))); ignore (Thread.create threaded_task ()) (* XXX - 1 appel *) let kill_input_view i = let v = session_notebook#get_nth_term i in v.analyzed_view#kill_detached_views (); v.script#destroy (); v.tab_label#destroy (); v.proof_view#destroy (); v.message_view#destroy (); session_notebook#remove_page 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 (* (* XXX - beaucoups d'appels, a garder *) let get_current_view = focused_session *) let remove_current_view_page () = let do_remove () = let c = session_notebook#current_page in kill_input_view c in let current = session_notebook#current_term in if not current.script#buffer#modified then do_remove () else match GToolbox.question_box ~title:"Close" ~buttons:["Save Buffer and Close"; "Close without Saving"; "Don't Close"] ~default:0 ~icon:(let img = GMisc.image () in img#set_stock `DIALOG_WARNING; img#set_icon_size `DIALOG; img#coerce) "This buffer has unsaved modifications" with | 1 -> begin match current.analyzed_view#filename with | None -> begin match select_file_for_save ~title:"Save file" () with | None -> () | Some f -> if current.analyzed_view#save_as f then begin flash_info ("File " ^ f ^ " saved") ; do_remove () end else warning ("Save Failed (check if " ^ f ^ " is writable)") end | Some f -> if current.analyzed_view#save f then begin flash_info ("File " ^ f ^ " saved") ; do_remove () end else warning ("Save Failed (check if " ^ f ^ " is writable)") end | 2 -> do_remove () | _ -> () (* 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 () = match session_notebook#current_term,cb#text with | {script=script; analyzed_view=av;},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 script#buffer#move_mark `SEL_BOUND start; script#buffer#move_mark `INSERT stop; script#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 handler name ~f = try let ic = open_in_gen [Open_rdonly;Open_creat] 0o644 name in try f ic; close_in ic with e -> close_in ic; raise e with Sys_error s -> handler s (* For electric handlers *) exception Found (* For find_phrase_starting_at *) exception Stop of int (* XXX *) let activate_input i = prerr_endline "entering activate_input"; (try on_active_view (fun {analyzed_view=a_v} -> a_v#reset_initial; a_v#deactivate ()) with _ -> ()); (session_notebook#get_nth_term i).analyzed_view#activate (); set_active_view i; prerr_endline "exiting activate_input" let apply_tag (buffer:GText.buffer) orig off_conv from upto sort = let conv_and_apply start stop tag = let start = orig#forward_chars (off_conv from) in let stop = orig#forward_chars (off_conv upto) in buffer#apply_tag ~start ~stop tag in match sort with | Coq_lex.Comment -> conv_and_apply from upto Tags.Script.comment | Coq_lex.Keyword -> conv_and_apply from upto Tags.Script.kwd | Coq_lex.Declaration -> conv_and_apply from upto Tags.Script.decl | Coq_lex.ProofDeclaration -> conv_and_apply from upto Tags.Script.proof_decl | Coq_lex.Qed -> conv_and_apply from upto Tags.Script.qed | Coq_lex.String -> () let remove_tags (buffer:GText.buffer) from upto = List.iter (buffer#remove_tag ~start:from ~stop:upto) [ Tags.Script.comment; Tags.Script.kwd; Tags.Script.decl; Tags.Script.proof_decl; Tags.Script.qed ] let split_slice_lax (buffer:GText.buffer) from upto = remove_tags buffer from upto; buffer#remove_tag ~start:from ~stop:upto Tags.Script.lax_end; let slice = buffer#get_text ~start:from ~stop:upto () in let slice = slice ^ " " in let rec split_substring str = let off_conv = byte_offset_to_char_offset str in let slice_len = String.length str in let sentence_len = Coq_lex.find_end_offset (apply_tag buffer from off_conv) str in let stop = from#forward_chars (pred (off_conv sentence_len)) in let start = stop#backward_char in buffer#apply_tag ~start ~stop Tags.Script.lax_end; if 1 < slice_len - sentence_len then begin (* remember that we added a trailing space *) ignore (from#nocopy#forward_chars (off_conv sentence_len)); split_substring (String.sub str sentence_len (slice_len - sentence_len)) end in split_substring slice let rec grab_safe_sentence_start (iter:GText.iter) soi = let lax_back = iter#backward_char#has_tag Tags.Script.lax_end in let on_space = List.mem iter#char [0x09;0x0A;0x20] in let full_ending = iter#is_start || (lax_back & on_space) in if full_ending then iter else if iter#compare soi <= 0 then raise Not_found else let prev = iter#backward_to_tag_toggle (Some Tags.Script.lax_end) in (if prev#has_tag Tags.Script.lax_end then ignore (prev#nocopy#backward_to_tag_toggle (Some Tags.Script.lax_end))); grab_safe_sentence_start prev soi let grab_sentence_end_from (start:GText.iter) = let stop = start#forward_to_tag_toggle (Some Tags.Script.lax_end) in stop#forward_char let get_sentence_bounds (iter:GText.iter) = let start = iter#backward_to_tag_toggle (Some Tags.Script.lax_end) in (if start#has_tag Tags.Script.lax_end then ignore ( start#nocopy#backward_to_tag_toggle (Some Tags.Script.lax_end))); let stop = start#forward_to_tag_toggle (Some Tags.Script.lax_end) in let stop = stop#forward_char in start,stop let end_tag_present end_iter = end_iter#backward_char#has_tag Tags.Script.lax_end let tag_on_insert = let skip_last = ref (ref true) in (* ref to the mutable flag created on last call *) fun buffer -> try let insert = buffer#get_iter_at_mark `INSERT in let start = grab_safe_sentence_start insert (buffer#get_iter_at_mark (`NAME "start_of_input")) in let stop = grab_sentence_end_from insert in let skip_curr = ref true in (* shall the callback be skipped ? by default yes*) (!skip_last) := true; (* skip the previously created callback *) skip_last := skip_curr; try split_slice_lax buffer start stop with Not_found -> skip_curr := false; ignore (Glib.Timeout.add ~ms:1500 ~callback:(fun () -> if not !skip_curr then ( try split_slice_lax buffer start buffer#end_iter with _ -> ()); false)) with Not_found -> let err_pos = buffer#get_iter_at_mark (`NAME "start_of_input") in buffer#apply_tag Tags.Script.error ~start:err_pos ~stop:err_pos#forward_char let force_retag buffer = try split_slice_lax buffer buffer#start_iter buffer#end_iter with _ -> () let toggle_proof_visibility (buffer:GText.buffer) (cursor:GText.iter) = (* move back twice if not into proof_decl, * once if into proof_decl and back_char into_proof_decl, * don't move if into proof_decl and back_char not into proof_decl *) if not (cursor#has_tag Tags.Script.proof_decl) then ignore (cursor#nocopy#backward_to_tag_toggle (Some Tags.Script.proof_decl)); if cursor#backward_char#has_tag Tags.Script.proof_decl then ignore (cursor#nocopy#backward_to_tag_toggle (Some Tags.Script.proof_decl)); let decl_start = cursor in let prf_end = decl_start#forward_to_tag_toggle (Some Tags.Script.qed) in let decl_end = grab_sentence_end_from decl_start in let prf_end = grab_sentence_end_from prf_end in let prf_end = prf_end#forward_char in if decl_start#has_tag Tags.Script.folded then ( buffer#remove_tag ~start:decl_start ~stop:decl_end Tags.Script.folded; buffer#remove_tag ~start:decl_end ~stop:prf_end Tags.Script.hidden) else ( buffer#apply_tag ~start:decl_start ~stop:decl_end Tags.Script.folded; buffer#apply_tag ~start:decl_end ~stop:prf_end Tags.Script.hidden) class analyzed_view (_script:Undo.undoable_view) (_pv:GText.view) (_mv:GText.view) _cs = object(self) val input_view = _script val input_buffer = _script#buffer val proof_view = _pv val proof_buffer = _pv#buffer val message_view = _mv val message_buffer = _mv#buffer val cmd_stack = _cs 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 val hidden_proofs = Hashtbl.create 32 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 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 flash_info f ~f:(input_channel b); let s = try_convert (Buffer.contents b) in input_buffer#set_text s; self#update_stats; input_buffer#place_cursor input_buffer#start_iter; input_buffer#set_modified false; pop_info (); flash_info "Buffer reverted"; force_retag 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,concl) = get_current_pm_goal () in List.iter (fun ((_,_,_,(s,_)) as _hyp) -> proof_buffer#insert (s^"\n")) hyps; proof_buffer#insert (String.make 38 '_' ^ "\n"); let (_,_,_,s) = concl in proof_buffer#insert ("thesis := \n "^s^"\n"); 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." val mutable full_goal_done = true method show_goals_full = if not full_goal_done then begin try proof_buffer#set_text ""; match Decl_mode.get_current_mode () with Decl_mode.Mode_none -> () | Decl_mode.Mode_tactic -> begin match Coq.get_current_goals () with [] -> proof_buffer#insert (Coq.print_no_goal()) | ((hyps,concl)::r) as s -> let last_shown_area = Tags.Proof.highlight 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 -> match GdkEvent.get_type ev with | `BUTTON_PRESS -> let ev = (GdkEvent.Button.cast ev) in if (GdkEvent.Button.button ev) = 3 then ( 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); true) else false | `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"; false | _ -> 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 show_goals = self#show_goals_full 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 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 Tags.Script.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 is_complete = not (Decl_mode.get_daimon_flag ()) in let msg = read_stdout () in sync display_output msg; Some (is_complete,r) end else begin let r = Coq.interp verbosely phrase in let is_complete = not (Decl_mode.get_daimon_flag ()) in let msg = read_stdout () in sync display_output msg; Some (is_complete,r) end with e -> if show_error then sync display_error e; None method find_phrase_starting_at (start:GText.iter) = try let start = grab_safe_sentence_start start self#get_start_of_input in let stop = grab_sentence_end_from start in if stop#backward_char#has_tag Tags.Script.lax_end then Some (start,stop) else None with Not_found -> 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 Tags.Script.to_process ~start ~stop; 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 Tags.Script.to_process ~start ~stop; input_view#set_editable true; pop_info (); end in let mark_processed reset_info is_complete (start,stop) = let b = input_buffer in b#move_mark ~where:stop (`NAME "start_of_input"); b#apply_tag (if is_complete then Tags.Script.processed else Tags.Script.unjustified) ~start ~stop; if (self#get_insert#compare) stop <= 0 then begin b#place_cursor stop; self#recenter_insert end; let ide_payload = { start = `MARK (b#create_mark start); stop = `MARK (b#create_mark stop); } in push_phrase cmd_stack reset_info ide_payload; 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 (is_complete,reset_info) -> sync (mark_processed reset_info is_complete) loc; true | None -> sync remove_tag loc; false) end method insert_this_phrase_on_success show_output show_msg localize coqphrase insertphrase = let mark_processed reset_info is_complete = 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 (if is_complete then Tags.Script.processed else Tags.Script.unjustified) ~start ~stop; if (self#get_insert#compare) stop <= 0 then input_buffer#place_cursor stop; let ide_payload = { start = `MARK (input_buffer#create_mark start); stop = `MARK (input_buffer#create_mark stop); } in push_phrase cmd_stack reset_info ide_payload; 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 reset_info 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 (is_complete,reset_info) -> sync (mark_processed reset_info) is_complete; 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 Tags.Script.to_process ~start ~stop; 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 Tags.Script.to_process ~start ~stop; 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 Tags.Script.processed ~start ~stop; input_buffer#remove_tag Tags.Script.unjustified ~start ~stop; input_buffer#delete_mark inf.start; input_buffer#delete_mark inf.stop; ) cmd_stack; Stack.clear cmd_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."; (* pop Coq commands until we reach iterator [i] *) let rec pop_cmds popped = if Stack.is_empty cmd_stack then popped else let (ide,coq) = Stack.pop cmd_stack in if i#compare (input_buffer#get_iter_at_mark ide.stop) < 0 then begin prerr_endline "popped command"; pop_cmds (coq::popped) end else begin Stack.push (ide,coq) cmd_stack; popped end in let seq = List.rev (pop_cmds []) in prerr_endline "Popped commands"; if 0 < List.length seq then begin try rewind seq cmd_stack; sync (fun _ -> let start = if Stack.is_empty cmd_stack then input_buffer#start_iter else input_buffer#get_iter_at_mark (fst (Stack.top cmd_stack)).stop in prerr_endline "Removing (long) processed tag..."; input_buffer#remove_tag Tags.Script.processed ~start ~stop:self#get_start_of_input; input_buffer#remove_tag Tags.Script.unjustified ~start ~stop:self#get_start_of_input; prerr_endline "Moving (long) start_of_input..."; input_buffer#move_mark ~where:start (`NAME "start_of_input"); full_goal_done <- false; 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 (ide_ri,_) = Stack.top cmd_stack in let start = input_buffer#get_iter_at_mark ide_ri.start in let update_input () = prerr_endline "Removing processed tag..."; input_buffer#remove_tag Tags.Script.processed ~start ~stop:(input_buffer#get_iter_at_mark ide_ri.stop); input_buffer#remove_tag Tags.Script.unjustified ~start ~stop:(input_buffer#get_iter_at_mark ide_ri.stop); prerr_endline "Moving start_of_input"; input_buffer#move_mark ~where:start (`NAME "start_of_input"); input_buffer#place_cursor start; self#recenter_insert; full_goal_done <- false; self#show_goals; self#clear_message in let _,coq = Stack.pop cmd_stack in rewind [coq] cmd_stack; sync update_input () with | Stack.Empty -> (* flash_info "Nothing to Undo"*)() ); pop_info (); Mutex.unlock coq_may_stop) else prerr_endline "undo_last_step 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 let _ = 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 in true else false | 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 (Option.get deact_id)*) (* XXX *) 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 (Option.get act_id); match 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 Tags.Script.processed ~start ~stop; input_buffer#remove_tag Tags.Script.unjustified ~start ~stop 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 = session_notebook#current_term.analyzed_view in let has_completed = v#complete_at_offset ((input_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#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 Tags.Script.error ~start:self#get_start_of_input ~stop; tag_on_insert input_buffer ) ); ignore (input_buffer#add_selection_clipboard cb); ignore (proof_buffer#add_selection_clipboard cb); ignore (message_buffer#add_selection_clipboard cb); self#electric_paren Tags.Script.paren; 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 Tags.Script.paren; | 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 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)) (**********************************************************************) (* session creation and primitive handling *) (**********************************************************************) let create_session () = let script = Undo.undoable_view ~buffer:(GText.buffer ~tag_table:Tags.Script.table ()) ~wrap_mode:`NONE () in let proof = GText.view ~buffer:(GText.buffer ~tag_table:Tags.Proof.table ()) ~editable:false ~wrap_mode:`CHAR () in let message = GText.view ~buffer:(GText.buffer ~tag_table:Tags.Message.table ()) ~editable:false ~wrap_mode:`WORD () in let basename = GMisc.label ~text:"*scratch*" () in let stack = Stack.create () in let legacy_av = new analyzed_view script proof message stack in let _ = script#buffer#create_mark ~name:"start_of_input" script#buffer#start_iter in let _ = proof#buffer#create_mark ~name:"end_of_conclusion" proof#buffer#start_iter in let _ = GtkBase.Widget.add_events proof#as_widget [`ENTER_NOTIFY;`POINTER_MOTION] in let _ = proof#event#connect#motion_notify ~callback: (fun e -> let win = match proof#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 = proof#window_to_buffer_coords ~tag:`WIDGET ~x ~y in let it = proof#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 proof#as_widget e it#as_iter)) tags; false) in script#misc#set_name "ScriptWindow"; script#buffer#place_cursor ~where:(script#buffer#start_iter); proof#misc#set_can_focus true; message#misc#set_can_focus true; script#misc#modify_font !current.text_font; proof#misc#modify_font !current.text_font; message#misc#modify_font !current.text_font; { tab_label=basename; filename=""; script=script; proof_view=proof; message_view=message; analyzed_view=legacy_av; command_stack=stack; encoding="" } (* XXX - to be used later let load_session session filename encs = session.encoding <- List.find (IdeIO.load filename session.script#buffer) encs; session.tab_label#set_text (Glib.Convert.filename_to_utf8 (Filename.basename filename)); session.filename <- filename; session.script#buffer#set_modified false let save_session session filename encs = session.encoding <- List.find (IdeIO.save session.script#buffer filename) encs; session.tab_label#set_text (Glib.Convert.filename_to_utf8 (Filename.basename filename)); session.filename <- filename; session.script#buffer#set_modified false let init_session session = session.script#buffer#set_modified false; session.script#clear_undo; session.script#buffer#place_cursor session.script#buffer#start_iter *) (*********************************************************************) (* functions called by the user interface *) (*********************************************************************) (* XXX - to be used later let do_open session filename = try load_session session filename ["UTF-8";"ISO-8859-1";"ISO-8859-15"]; init_session session; ignore (session_notebook#append_term session) with _ -> () let do_save session = try if session.script#buffer#modified then save_session session session.filename [session.encoding] with _ -> () let choose_open = let last_filename = ref "" in fun session -> let open_dialog = GWindow.file_chooser_dialog ~action:`OPEN ~title:"Open file" ~modal:true () in let enc_frame = GBin.frame ~label:"File encoding" ~packing:(open_dialog#vbox#pack ~fill:false) () in let enc_entry = GEdit.entry ~text:(String.concat " " ["UTF-8";"ISO-8859-1";"ISO-8859-15"]) ~packing:enc_frame#add () in let error_dialog = GWindow.message_dialog ~message_type:`ERROR ~modal:true ~buttons:GWindow.Buttons.ok ~message:"Invalid encoding, please indicate the encoding to use." () in let open_response = function | `OPEN -> begin match open_dialog#filename with | Some fn -> begin try load_session session fn (Util.split_string_at ' ' enc_entry#text); session.analyzed_view <- Some (new analyzed_view session); init_session session; session_notebook#goto_page (session_notebook#append_term session); last_filename := fn with | Not_found -> open_dialog#misc#hide (); error_dialog#show () | _ -> error_dialog#set_markup "Unknown error while loading file, aborting."; open_dialog#destroy (); error_dialog#destroy () end | None -> () end | `DELETE_EVENT -> open_dialog#destroy (); error_dialog#destroy () in let _ = open_dialog#connect#response open_response in let _ = error_dialog#connect#response (fun x -> error_dialog#misc#hide (); open_dialog#show ()) in let filter_any = GFile.filter ~name:"Any" ~patterns:["*"] () in let filter_coq = GFile.filter ~name:"Coq source" ~patterns:["*.v"] () in open_dialog#add_select_button_stock `OPEN `OPEN; open_dialog#add_button_stock `CANCEL `DELETE_EVENT; open_dialog#add_filter filter_any; open_dialog#add_filter filter_coq; ignore(open_dialog#set_filename !last_filename); open_dialog#show () let choose_save session = let save_dialog = GWindow.file_chooser_dialog ~action:`SAVE ~title:"Save file" ~modal:true () in let enc_frame = GBin.frame ~label:"File encoding" ~packing:(save_dialog#vbox#pack ~fill:false) () in let enc_entry = GEdit.entry ~text:(String.concat " " [session.encoding;"UTF-8";"ISO-8859-1";"ISO-8859-15"]) ~packing:enc_frame#add () in let error_dialog = GWindow.message_dialog ~message_type:`ERROR ~modal:true ~buttons:GWindow.Buttons.ok ~message:"Invalid encoding, please indicate the encoding to use." () in let save_response = function | `SAVE -> begin match save_dialog#filename with | Some fn -> begin try save_session session fn (Util.split_string_at ' ' enc_entry#text) with | Not_found -> save_dialog#misc#hide (); error_dialog#show () | _ -> error_dialog#set_markup "Unknown error while saving file, aborting."; save_dialog#destroy (); error_dialog#destroy () end | None -> () end | `DELETE_EVENT -> save_dialog#destroy (); error_dialog#destroy () in let _ = save_dialog#connect#response save_response in let _ = error_dialog#connect#response (fun x -> error_dialog#misc#hide (); save_dialog#show ()) in let filter_any = GFile.filter ~name:"Any" ~patterns:["*"] () in let filter_coq = GFile.filter ~name:"Coq source" ~patterns:["*.v"] () in save_dialog#add_select_button_stock `SAVE `SAVE; save_dialog#add_button_stock `CANCEL `DELETE_EVENT; save_dialog#add_filter filter_any; save_dialog#add_filter filter_coq; ignore(save_dialog#set_filename session.filename); save_dialog#show () *) (* Nota: using && here has the advantage of working both under win32 and unix. If someday we want the main command to be tried even if the "cd" has failed, then we should use " ; " under unix but " & " under win32 (cf. #2363). *) let local_cd file = "cd " ^ Filename.quote (Filename.dirname file) ^ " && " let do_print session = let av = session.analyzed_view in match av#filename with |None -> flash_info "Cannot print: this buffer has no name" |Some f_name -> begin let cmd = local_cd session.filename ^ !current.cmd_coqdoc ^ " --coqlib_path " ^ Envars.coqlib () ^ " -ps " ^ Filename.quote (Filename.basename f_name) ^ " | " ^ !current.cmd_print in let print_window = GWindow.window ~title:"Print" ~modal:true ~position:`CENTER ~wm_class:"CoqIDE" ~wm_name: "CoqIDE" () in let vbox_print = GPack.vbox ~spacing:10 ~border_width:10 ~packing:print_window#add () in let _ = GMisc.label ~justify:`LEFT ~text:"Print using the following command:" ~packing:vbox_print#add () in let print_entry = GEdit.entry ~text:cmd ~editable:true ~width_chars:80 ~packing:vbox_print#add () in let hbox_print = GPack.hbox ~spacing:10 ~packing:vbox_print#add () in let print_cancel_button = GButton.button ~stock:`CANCEL ~label:"Cancel" ~packing:hbox_print#add () in let print_button = GButton.button ~stock:`PRINT ~label:"Print" ~packing:hbox_print#add () in let callback_print () = let cmd = print_entry#text in let s,_ = run_command av#insert_message cmd in flash_info (cmd ^ if s = Unix.WEXITED 0 then " succeeded" else " failed"); print_window#destroy () in ignore (print_cancel_button#connect#clicked ~callback:print_window#destroy) ; ignore (print_button#connect#clicked ~callback:callback_print); print_window#misc#show () end 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.png" 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_file handler f = let f = absolute_filename f in try prerr_endline "Loading file starts"; if not (Util.list_fold_left_i (fun i found x -> if found then found else let {analyzed_view=av} = x in (match av#filename with | None -> false | Some fn -> if same_file f fn then (session_notebook#goto_page i; true) else false)) 0 false session_notebook#pages) then begin prerr_endline "Loading: must open"; let b = Buffer.create 1024 in prerr_endline "Loading: get raw content"; with_file handler f ~f:(input_channel b); prerr_endline "Loading: convert content"; let s = do_convert (Buffer.contents b) in prerr_endline "Loading: create view"; let session = create_session () in session.tab_label#set_text (Glib.Convert.filename_to_utf8 (Filename.basename f)); prerr_endline "Loading: adding view"; let index = session_notebook#append_term session in let av = session.analyzed_view in prerr_endline "Loading: set filename"; av#set_filename (Some f); prerr_endline "Loading: stats"; av#update_stats; let input_buffer = session.script#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); session_notebook#goto_page index; prerr_endline "Loading: highlight"; input_buffer#set_modified false; prerr_endline "Loading: clear undo"; session.script#clear_undo; prerr_endline "Loading: success" end with | e -> handler ("Load failed: "^(Printexc.to_string e)) in let load f = load_file flash_info f in let load_m = file_factory#add_item "_New" ~key:GdkKeysyms._N in let load_f () = match select_file_for_save ~title:"Create file" () with | None -> () | Some f -> load f in ignore (load_m#connect#activate (load_f)); let load_m = file_factory#add_item "_Open" ~key:GdkKeysyms._O in let load_f () = match select_file_for_open ~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 = session_notebook#current_term in try (match current.analyzed_view#filename with | None -> begin match select_file_for_save ~title:"Save file" () with | None -> () | Some f -> if current.analyzed_view#save_as f then begin current.tab_label#set_text (Filename.basename f); flash_info ("File " ^ f ^ " saved") end else warning ("Save Failed (check if " ^ f ^ " is writable)") end | Some f -> if 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 = session_notebook#current_term in try (match current.analyzed_view#filename with | None -> begin match select_file_for_save ~title:"Save file as" () with | None -> () | Some f -> if current.analyzed_view#save_as f then begin current.tab_label#set_text (Filename.basename f); flash_info "Saved" end else flash_info "Save Failed" end | Some f -> begin match select_file_for_save ~dir:(ref (Filename.dirname f)) ~filename:(Filename.basename f) ~title:"Save file as" () with | None -> () | Some f -> if current.analyzed_view#save_as f then begin current.tab_label#set_text (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); (* XXX *) (* File/Save All Menu *) let saveall_m = file_factory#add_item "Sa_ve all" in let saveall_f () = List.iter (function | {script = view ; analyzed_view = av} -> begin match av#filename with | None -> () | Some f -> ignore (av#save f) end ) session_notebook#pages in (* XXX *) let has_something_to_save () = List.exists (function | {script=view} -> view#buffer#modified ) session_notebook#pages in ignore (saveall_m#connect#activate saveall_f); (* XXX *) (* File/Revert Menu *) let revert_m = file_factory#add_item "_Revert all buffers" in let revert_f () = List.iter (function {analyzed_view = 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) ) session_notebook#pages 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 = !active_view in let act = session_notebook#current_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 _ = file_factory#add_item "_Print..." ~key:GdkKeysyms._P ~callback:(fun () -> do_print session_notebook#current_term) in (* File/Export to Menu *) let export_f kind () = let v = session_notebook#current_term in let av = 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" | "pdf" | "html" -> basef_we ^ "." ^ kind | _ -> assert false in let cmd = local_cd f ^ !current.cmd_coqdoc ^ " --coqlib_path " ^ Envars.coqlib () ^ " --" ^ kind ^ " -o " ^ (Filename.quote output) ^ " " ^ (Filename.quote 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 "_Pdf" ~callback:(export_f "pdf") 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 () -> force_retag session_notebook#current_term.script#buffer; session_notebook#current_term.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 (session_notebook#current_term.analyzed_view# without_auto_complete (fun () -> session_notebook#current_term.script#undo) ())))); ignore(edit_f#add_item "_Clear Undo Stack" (* ~key:GdkKeysyms._exclam *) ~callback: (fun () -> ignore session_notebook#current_term.script#clear_undo)); ignore(edit_f#add_separator ()); let get_active_view_for_cp () = let has_sel (i0,i1) = i0#compare i1 <> 0 in let current = session_notebook#current_term in if has_sel current.script#buffer#selection_bounds then current.script#as_view else if has_sel current.proof_view#buffer#selection_bounds then current.proof_view#as_view else current.message_view#as_view in ignore(edit_f#add_item "Cut" ~key:GdkKeysyms._X ~callback: (fun () -> GtkSignal.emit_unit (get_active_view_for_cp ()) GtkText.View.S.cut_clipboard )); ignore(edit_f#add_item "Copy" ~key:GdkKeysyms._C ~callback: (fun () -> GtkSignal.emit_unit (get_active_view_for_cp ()) GtkText.View.S.copy_clipboard)); ignore(edit_f#add_item "Paste" ~key:GdkKeysyms._V ~callback: (fun () -> try GtkSignal.emit_unit session_notebook#current_term.script#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 session_notebook#current_term.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 = session_notebook#current_term.script 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 Tags.Script.found ~start ~stop; last_found:=None; start,stop in (v,b,start,stop) in let do_replace () = let v = session_notebook#current_term.script 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 Tags.Script.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 = session_notebook#current_term.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 = session_notebook#current_term.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 = session_notebook#current_term.analyzed_view in match av#filename with | None -> warning "Call to external editor available only on named files" | Some f -> save_f (); let com = Flags.subst_command_placeholder !current.cmd_editor (Filename.quote f) in let _ = run_command av#insert_message com 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 *) (* XXX *) let auto_save_f () = List.iter (function {script = view ; analyzed_view = av} -> (try av#auto_save with _ -> ()) ) session_notebook#pages 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 ~apply:update_notebook_pos (); 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 = session_notebook#current_term in let analyzed_view = current.analyzed_view in if analyzed_view#is_active then begin prerr_endline ("view "^current.tab_label#text^"already active"); ignore (f analyzed_view) end else begin flash_info "New proof started"; prerr_endline ("activating view "^current.tab_label#text); activate_input session_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; add_to_menu_toolbar "_Hide" ~tooltip:"Hide proof" ~key:GdkKeysyms._h ~callback:(fun x -> let sess = session_notebook#current_term in toggle_proof_visibility sess.script#buffer sess.analyzed_view#get_insert) `MISSING_IMAGE; (* 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 = session_notebook#current_term in let analyzed_view = 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 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 {script = view } = session_notebook#current_term 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 {script = view } = session_notebook#current_term 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 {script = view } = session_notebook#current_term 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 } = session_notebook#current_term 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 "_About " ~key:GdkKeysyms._F5 ~callback:(fun () -> let term = get_current_word () in (Command_windows.command_window ())#new_command ~command:"About" ~term ()) in let _ = queries_factory#add_item "_Locate" ~callback:(fun () -> let term = get_current_word () in (Command_windows.command_window ())#new_command ~command:"Locate" ~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 (* Display menu *) let display_menu = factory#add_submenu "_Display" in let view_factory = new GMenu.factory display_menu ~accel_path:"/Display/" ~accel_group ~accel_modi:!current.modifier_for_display in let _ = ignore (view_factory#add_check_item "Display _implicit arguments" ~key:GdkKeysyms._i ~callback:(fun _ -> printing_state.printing_implicit <- not printing_state.printing_implicit; do_or_activate (fun a -> a#show_goals) ())) in let _ = ignore (view_factory#add_check_item "Display _coercions" ~key:GdkKeysyms._c ~callback:(fun _ -> printing_state.printing_coercions <- not printing_state.printing_coercions; do_or_activate (fun a -> a#show_goals) ())) in let _ = ignore (view_factory#add_check_item "Display raw _matching expressions" ~key:GdkKeysyms._m ~callback:(fun _ -> printing_state.printing_raw_matching <- not printing_state.printing_raw_matching; do_or_activate (fun a -> a#show_goals) ())) in let _ = ignore (view_factory#add_check_item "Deactivate _notations display" ~key:GdkKeysyms._n ~callback:(fun _ -> printing_state.printing_no_notation <- not printing_state.printing_no_notation; do_or_activate (fun a -> a#show_goals) ())) in let _ = ignore (view_factory#add_check_item "Display _all basic low-level contents" ~key:GdkKeysyms._a ~callback:(fun _ -> printing_state.printing_all <- not printing_state.printing_all; do_or_activate (fun a -> a#show_goals) ())) in let _ = ignore (view_factory#add_check_item "Display _existential variable instances" ~key:GdkKeysyms._e ~callback:(fun _ -> printing_state.printing_evar_instances <- not printing_state.printing_evar_instances; do_or_activate (fun a -> a#show_goals) ())) in let _ = ignore (view_factory#add_check_item "Display _universe levels" ~key:GdkKeysyms._u ~callback:(fun _ -> printing_state.printing_universes <- not printing_state.printing_universes; do_or_activate (fun a -> a#show_goals) ())) in let _ = ignore (view_factory#add_check_item "Display all _low-level contents" ~key:GdkKeysyms._l ~callback:(fun _ -> printing_state.printing_full_all <- not printing_state.printing_full_all; do_or_activate (fun a -> a#show_goals) ())) 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 = session_notebook#current_term in let av = v.analyzed_view in save_f (); match av#filename with | None -> flash_info "Active buffer has no name" | Some f -> let cmd = !current.cmd_coqc ^ " -I " ^ (Filename.quote (Filename.dirname f)) ^ " " ^ (Filename.quote f) in let s,res = run_command av#insert_message cmd in if s = Unix.WEXITED 0 then flash_info (f ^ " successfully compiled") else begin flash_info (f ^ " failed to compile"); activate_input session_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 = session_notebook#current_term in let av = v.analyzed_view in match av#filename with | None -> flash_info "Cannot make: this buffer has no name" | Some f -> let cmd = local_cd f ^ !current.cmd_make in (* save_f (); *) av#insert_message "Command output:\n"; let s,res = run_command av#insert_message cmd 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 = session_notebook#current_term in let av = v.analyzed_view in let input_buffer = v.script#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 Tags.Script.error ~start:starti ~stop:stopi; input_buffer#place_cursor starti; av#set_message error_msg; v.script#misc#grab_focus () with Not_found -> last_make_index := 0; let v = session_notebook#current_term in let av = 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 = session_notebook#current_term in let av = v.analyzed_view in match av#filename with | None -> flash_info "Cannot make makefile: this buffer has no name" | Some f -> let cmd = local_cd f ^ !current.cmd_coqmakefile in let s,res = run_command av#insert_message cmd 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_modi:[] ~accel_group in let _ = configuration_factory#add_item "Show/Hide _Query Pane" ~key:GdkKeysyms._Escape ~callback:(fun () -> if (Command_windows.command_window ())#frame#misc#visible then (Command_windows.command_window ())#frame#misc#hide () else (Command_windows.command_window ())#frame#misc#show ()) in let _ = configuration_factory#add_check_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 _View" ~callback: (do_if_not_computing "detach view" (fun () -> match session_notebook#current_term with | {script=v;analyzed_view=av} -> let w = GWindow.window ~show:true ~width:(!current.window_width*2/3) ~height:(!current.window_height*2/3) ~position:`CENTER ~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 = session_notebook#current_term.analyzed_view in browse av#insert_message (doc_url ())) in let _ = help_factory#add_item "Browse Coq _Library" ~callback: (fun () -> let av = session_notebook#current_term.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 = session_notebook#current_term.analyzed_view in av#help_for_keyword ()) in let _ = help_factory#add_separator () in let about_m = help_factory#add_item "_About" in (* End of menu *) (* The vertical Separator between Scripts and Goals *) let queries_pane = GPack.paned `VERTICAL ~packing:(vbox#pack ~expand:true ) () in queries_pane#pack1 ~shrink:false ~resize:true session_notebook#coerce; update_notebook_pos (); let nb = session_notebook in let command_object = Command_windows.command_window() in let queries_frame = command_object#frame in queries_pane#pack2 ~shrink:false ~resize:false (queries_frame#coerce); let lower_hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in lower_hbox#pack ~expand:true status#coerce; 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 in let end_search () = prerr_endline "End Search"; memo_search (); let v = session_notebook#current_term.script 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 = session_notebook#current_term.script 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 (session_notebook#current_term.script#buffer#create_mark (session_notebook#current_term.script#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 = session_notebook#current_term.script 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 = session_notebook#current_term.script 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); push_info "Ready"; (* 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 *) lower_hbox#pack pbar#coerce; pbar#set_text "CoqIde started"; (* XXX *) change_font := (fun fd -> List.iter (fun {script=view; proof_view=prf_v; message_view=msg_v} -> view#misc#modify_font fd; prf_v#misc#modify_font fd; msg_v#misc#modify_font fd ) session_notebook#pages; ); let about_full_string = "\nCoq is developed by the Coq Development Team\ \n(INRIA - CNRS - University Paris 11 and partners)\ \nWeb site: " ^ Coq_config.wwwcoq ^ "\nFeature wish or bug report: http://coq.inria.fr/bugs\ \n\ \nCredits for CoqIDE, the Integrated Development Environment for Coq:\ \n\ \nMain author : Benjamin Monate\ \nContributors : Jean-Christophe Filliâtre\ \n Pierre Letouzey, Claude Marché\ \n Bruno Barras, Pierre Corbineau\ \n Julien Narboux, Hugo Herbelin, ... \ \n\ \nVersion information\ \n-------------------\ \n" in let initial_about (b:GText.buffer) = let initial_string = "Welcome to CoqIDE, an Integrated Development Environment for Coq\n" in let coq_version = Coq.short_version () in b#insert ~iter:b#start_iter "\n\n"; if Glib.Utf8.validate ("You are running " ^ coq_version) then b#insert ~iter:b#start_iter ("You are running " ^ coq_version); if Glib.Utf8.validate initial_string then b#insert ~iter:b#start_iter initial_string; (try let image = lib_ide_file "coq.png" in let startup_image = GdkPixbuf.from_file image in b#insert ~iter:b#start_iter "\n\n"; b#insert_pixbuf ~iter:b#start_iter ~pixbuf:startup_image; b#insert ~iter:b#start_iter "\n\n\t\t " with _ -> ()) in let about (b:GText.buffer) = (try let image = lib_ide_file "coq.png" in let startup_image = GdkPixbuf.from_file image in b#insert ~iter:b#start_iter "\n\n"; b#insert_pixbuf ~iter:b#start_iter ~pixbuf:startup_image; b#insert ~iter:b#start_iter "\n\n\t\t " with _ -> ()); if Glib.Utf8.validate about_full_string then b#insert about_full_string; let coq_version = Coq.version () in if Glib.Utf8.validate coq_version then b#insert coq_version in w#add_accel_group accel_group; (* Remove default pango menu for textviews *) w#show (); ignore (about_m#connect#activate ~callback:(fun () -> let prf_v = session_notebook#current_term.proof_view in prf_v#buffer#set_text ""; about prf_v#buffer)); (* *) resize_window := (fun () -> w#resize ~width:!current.window_width ~height:!current.window_height); 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") ); if List.length files >=1 then begin List.iter (fun f -> if Sys.file_exists f then load f else let f = if Filename.check_suffix f ".v" then f else f^".v" in load_file (fun s -> print_endline s; exit 1) f) files; activate_input 0 end else begin let session = create_session () in let index = session_notebook#append_term session in activate_input index; end; initial_about session_notebook#current_term.proof_view#buffer; !show_toolbar !current.show_toolbar; session_notebook#current_term.script#misc#grab_focus () ;; (* 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 session_notebook#current_term.script#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]); 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 (); init_stdout (); 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." | e -> safe_prerr_endline ("CoqIde unexpected error:" ^ (Printexc.to_string e)); flush_all (); crash_save 127 done