From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- ide/coqide.ml | 695 +++++++++++++++++++++++++++++++++++++--------------------- 1 file changed, 449 insertions(+), 246 deletions(-) (limited to 'ide/coqide.ml') diff --git a/ide/coqide.ml b/ide/coqide.ml index 6cee46a6..12716197 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1,3 +1,4 @@ + (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* failwith "Internal error in out_some" | Some f -> f - let cb_ = ref None -let cb () = ((out_some !cb_):GData.clipboard) +let cb () = ((Option.get !cb_):GData.clipboard) let last_cb_content = ref "" - + let (message_view:GText.view option ref) = ref None let (proof_view:GText.view option ref) = ref None let (_notebook:GPack.notebook option ref) = ref None -let notebook () = out_some !_notebook +let notebook () = Option.get !_notebook + +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 + (notebook ())#set_tab_pos pos (* Tabs contain the name of the edited file and 2 status informations: Saved state + Focused proof buffer *) @@ -89,7 +97,7 @@ module Vector = struct type 'a t = ('a option) array ref let create () = ref [||] let length t = Array.length !t - let get t i = out_some (Array.get !t i) + let get t i = Option.get (Array.get !t i) let set t i v = Array.set !t i (Some v) let remove t i = Array.set !t i None let append t e = t := Array.append !t [|Some e|]; (Array.length !t)-1 @@ -101,7 +109,7 @@ module Vector = struct let exists f t = let l = Array.length !t in let rec test i = - (i < l) && (((!t.(i) <> None) && f (out_some !t.(i))) || test (i+1)) + (i < l) && (((!t.(i) <> None) && f (Option.get !t.(i))) || test (i+1)) in test 0 end @@ -175,7 +183,8 @@ object('self) method reset_initial : unit method send_to_coq : bool -> bool -> string -> - bool -> bool -> bool -> (bool*(Util.loc * Vernacexpr.vernac_expr)) option + bool -> bool -> bool -> + (bool*(reset_info*(Util.loc * Vernacexpr.vernac_expr))) option method set_message : string -> unit method show_pm_goal : unit method show_goals : unit @@ -300,7 +309,7 @@ let get_input_view i = let active_view = ref None -let get_active_view () = Vector.get input_views (out_some !active_view) +let get_active_view () = Vector.get input_views (Option.get !active_view) let set_active_view i = (match !active_view with None -> () | Some i -> @@ -451,8 +460,8 @@ let rec complete input_buffer w (offset:int) = end let get_current_word () = - let av = out_some ((get_current_view ()).analyzed_view) in - match GtkBase.Clipboard.wait_for_text (cb ())#as_clipboard with + let av = Option.get ((get_current_view ()).analyzed_view) in + match (cb ())#text with | None -> prerr_endline "None selected"; let it = av#get_insert in @@ -481,7 +490,7 @@ let with_file name ~f = type info = {start:GText.mark; stop:GText.mark; ast:Util.loc * Vernacexpr.vernac_expr; - reset_info:Coq.reset_info; + reset_info:Coq.reset_info } exception Size of int @@ -491,60 +500,118 @@ let pop () = try Stack.pop processed_stack with Stack.Empty -> raise (Size 0) let top () = try Stack.top processed_stack with Stack.Empty -> raise (Size 0) let is_empty () = Stack.is_empty processed_stack - (* push a new Coq phrase *) -let update_on_end_of_proof id = - let lookup_lemma = function - | { ast = _, ( VernacDefinition (_, _, ProveBody _, _) - | VernacDeclareTacticDefinition _ - | VernacStartTheoremProof _) ; - reset_info = Reset (_, r) } -> - if not !r then begin - prerr_endline "Toggling Reset info to true"; - r := true; raise Exit end - else begin - prerr_endline "Toggling Changing Reset id"; - r := false - end - | { ast = _, (VernacAbort _ | VernacAbortAll | VernacGoal _) } -> raise Exit - | _ -> () - in - try Stack.iter lookup_lemma processed_stack with Exit -> () - let update_on_end_of_segment id = let lookup_section = function - | { ast = _, ( VernacBeginSection id' - | VernacDefineModule (_,id',_,_,None) - | VernacDeclareModule (_,id',_,_) - | VernacDeclareModuleType (id',_,None)); - reset_info = Reset (_, r) } - when id = id' -> raise Exit - | { reset_info = Reset (_, r) } -> r := false - | _ -> () + | { reset_info = ResetAtSegmentStart id',_,_ } when id = id' -> raise Exit + | { reset_info = _,_,r } -> r := false in try Stack.iter lookup_section processed_stack with Exit -> () -let push_phrase start_of_phrase_mark end_of_phrase_mark ast = +let push_phrase reset_info start_of_phrase_mark end_of_phrase_mark ast = let x = {start = start_of_phrase_mark; stop = end_of_phrase_mark; ast = ast; - reset_info = Coq.compute_reset_info (snd ast) - } - in - push x; + reset_info = reset_info + } in + begin match snd ast with - | VernacEndProof (Proved (_, None)) -> update_on_end_of_proof () - | VernacEndSegment id -> update_on_end_of_segment id - | _ -> () + | VernacEndSegment (_,id) -> + prerr_endline "Updating on end of segment 1"; + update_on_end_of_segment id + | _ -> () + end; + push x -let repush_phrase x = - let x = { x with reset_info = Coq.compute_reset_info (snd x.ast) } in - push x; + +let repush_phrase reset_info x = + let x = { x with reset_info = reset_info } in + begin match snd x.ast with - | VernacEndProof (Proved (_, None)) -> update_on_end_of_proof () - | VernacEndSegment id -> update_on_end_of_segment id + | VernacEndSegment (_,id) -> + prerr_endline "Updating on end of segment 2"; + update_on_end_of_segment id | _ -> () + end; + push x + +type backtrack = +| BacktrackToNextActiveMark +| BacktrackToMark of reset_mark +| BacktrackToModSec of Names.identifier +| NoBacktrack + +let add_undo = function (n,a,b,p,l as x) -> if p = 0 then (n+1,a,b,p,l) else x +let add_abort = function (n,a,b,0,l) -> (0,a+1,b,0,l) | (n,a,b,p,l) -> (n,a,b,p-1,l) +let add_qed q (n,a,b,p,l) = (n,a,b,p+q,l) +let add_backtrack (n,a,b,p,l) b' = (n,a,b',p,l) + +let update_proofs (n,a,b,p,cur_lems) prev_lems = + let ncommon = List.length (Util.list_intersect cur_lems prev_lems) in + let openproofs = List.length cur_lems - ncommon in + let closedproofs = List.length prev_lems - ncommon in + let undos = (n,a,b,p,prev_lems) in + add_qed closedproofs (Util.iterate add_abort openproofs undos) + +let pop_command undos t = + let (state_info,undo_info,section_info) = t.reset_info in + let undos = + if !section_info then + let undos = update_proofs undos undo_info in + match state_info with + | _ when is_vernac_tactic_command (snd t.ast) -> + (* A tactic, active if not below a Qed *) + add_undo undos + | ResetAtRegisteredObject mark -> + add_backtrack undos (BacktrackToMark mark) + | ResetAtSegmentStart id -> + add_backtrack undos (BacktrackToModSec id) + | _ when is_vernac_state_preserving_command (snd t.ast) -> + undos + | _ -> + add_backtrack undos BacktrackToNextActiveMark + else + begin + prerr_endline "In section"; + (* An object inside a closed section *) + add_backtrack undos BacktrackToNextActiveMark + end in + ignore (pop ()); + undos + +let rec apply_backtrack l = function + | 0, BacktrackToMark mark -> reset_to mark + | 0, NoBacktrack -> () + | 0, BacktrackToModSec id -> reset_to_mod id + | p, _ -> + (* re-synchronize Coq to the current state of the stack *) + if is_empty () then + Coq.reset_initial () + else + begin + let t = top () in + let undos = (0,0,BacktrackToNextActiveMark,p,l) in + let (_,_,b,p,l) = pop_command undos t in + apply_backtrack l (p,b); + let reset_info = Coq.compute_reset_info (snd t.ast) in + interp_last t.ast; + repush_phrase reset_info t + end + +let rec apply_undos (n,a,b,p,l) = + (* Aborts *) + if a <> 0 then prerr_endline ("Applying "^string_of_int a^" aborts"); + (try Util.repeat a Pfedit.delete_current_proof () + with e -> prerr_endline "WARNING : found a closed environment"; raise e); + (* Undos *) + if n<>0 then + (prerr_endline ("Applying "^string_of_int n^" undos"); + try Pfedit.undo n + with _ -> (* Undo stack exhausted *) + apply_backtrack l (p,BacktrackToNextActiveMark)); + (* Reset *) + apply_backtrack l (p,b) (* For electric handlers *) exception Found @@ -556,11 +623,11 @@ let activate_input i = (match !active_view with | None -> () | Some n -> - let a_v = out_some (Vector.get input_views n).analyzed_view in + let a_v = Option.get (Vector.get input_views n).analyzed_view in a_v#deactivate (); a_v#reset_initial ); - let activate_function = (out_some (Vector.get input_views i).analyzed_view)#activate in + let activate_function = (Option.get (Vector.get input_views i).analyzed_view)#activate in activate_function (); set_active_view i @@ -575,13 +642,13 @@ let warning msg = class analyzed_view index = let {view = input_view_} as current_all_ = get_input_view index in - let proof_view_ = out_some !proof_view in - let message_view_ = out_some !message_view in + let proof_view_ = Option.get !proof_view in + let message_view_ = Option.get !message_view in object(self) val current_all = current_all_ val input_view = current_all_.view - val proof_view = out_some !proof_view - val message_view = out_some !message_view + val proof_view = Option.get !proof_view + val message_view = Option.get !message_view val input_buffer = input_view_#buffer val proof_buffer = proof_view_#buffer val message_buffer = message_view_#buffer @@ -794,17 +861,15 @@ object(self) proof_buffer#insert (Printf.sprintf " *** Declarative Mode ***\n"); try - let (hyps,metas) = get_current_pm_goal () in + 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"); - List.iter - (fun (_,_,m) -> - proof_buffer#insert (m^"\n")) - metas; + 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)) @@ -1000,7 +1065,7 @@ object(self) self#insert_message s; message_view#misc#draw None; if localize then - (match Util.option_map Util.unloc loc with + (match Option.map Util.unloc loc with | None -> () | Some (start,stop) -> let convert_pos = byte_offset_to_char_offset phrase in @@ -1140,7 +1205,7 @@ object(self) input_view#set_editable true; !pop_info (); end in - let mark_processed complete (start,stop) ast = + let mark_processed reset_info complete (start,stop) ast = let b = input_buffer in b#move_mark ~where:stop (`NAME "start_of_input"); b#apply_tag_by_name @@ -1152,7 +1217,8 @@ object(self) end; let start_of_phrase_mark = `MARK (b#create_mark start) in let end_of_phrase_mark = `MARK (b#create_mark stop) in - push_phrase + push_phrase + reset_info start_of_phrase_mark end_of_phrase_mark ast; if display_goals then self#show_goals; @@ -1162,14 +1228,14 @@ object(self) None -> false | Some (loc,phrase) -> (match self#send_to_coq verbosely false phrase true true true with - | Some (complete,ast) -> - sync (mark_processed complete) loc ast; true + | Some (complete,(reset_info,ast)) -> + sync (mark_processed reset_info complete) loc ast; true | None -> sync remove_tag loc; false) end method insert_this_phrase_on_success show_output show_msg localize coqphrase insertphrase = - let mark_processed complete ast = + let mark_processed reset_info complete ast = let stop = self#get_start_of_input in if stop#starts_line then input_buffer#insert ~iter:stop insertphrase @@ -1182,7 +1248,7 @@ object(self) input_buffer#place_cursor stop; let start_of_phrase_mark = `MARK (input_buffer#create_mark start) in let end_of_phrase_mark = `MARK (input_buffer#create_mark stop) in - push_phrase start_of_phrase_mark end_of_phrase_mark ast; + push_phrase reset_info start_of_phrase_mark end_of_phrase_mark ast; self#show_goals; (*Auto insert save on success... try (match Coq.get_current_goals () with @@ -1203,13 +1269,15 @@ object(self) `MARK (input_buffer#create_mark start) in let end_of_phrase_mark = `MARK (input_buffer#create_mark stop) in - push_phrase start_of_phrase_mark end_of_phrase_mark ast + 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 (complete,ast) -> sync (mark_processed complete) ast; true + | Some (complete,(reset_info,ast)) -> + sync (mark_processed reset_info complete) ast; true | None -> sync (fun _ -> self#insert_message ("Unsuccessfully tried: "^coqphrase)) @@ -1268,53 +1336,30 @@ object(self) self#clear_message)(); Coq.reset_initial () - (* backtrack Coq to the phrase preceding iterator [i] *) method backtrack_to_no_lock i = prerr_endline "Backtracking_to iter starts now."; - (* re-synchronize Coq to the current state of the stack *) - let rec synchro () = - if is_empty () then - Coq.reset_initial () - else begin - let t = pop () in - begin match t.reset_info with - | Reset (id, ({contents=true} as v)) -> v:=false; - (match snd t.ast with - | VernacBeginSection _ | VernacDefineModule _ - | VernacDeclareModule _ | VernacDeclareModuleType _ - | VernacEndSegment _ - -> reset_to_mod id - | _ -> reset_to id) - | _ -> synchro () - end; - interp_last t.ast; - repush_phrase t - end - in - let add_undo t = match t with | Some n -> Some (succ n) | None -> None - in - (* pop Coq commands until we reach iterator [i] *) + (* pop Coq commands until we reach iterator [i] *) let rec pop_commands done_smthg undos = if is_empty () then done_smthg, undos else let t = top () in - if i#compare (input_buffer#get_iter_at_mark t.stop) < 0 then begin - ignore (pop ()); - let undos = if is_tactic (snd t.ast) then add_undo undos else None in - pop_commands true undos - end else - done_smthg, undos + if i#compare (input_buffer#get_iter_at_mark t.stop) < 0 then + begin + prerr_endline "Popped top command"; + pop_commands true (pop_command undos t) + end + else + done_smthg, undos in - let done_smthg, undos = pop_commands false (Some 0) in + let undos = (0,0,NoBacktrack,0,undo_info()) in + let done_smthg, undos = pop_commands false undos in prerr_endline "Popped commands"; if done_smthg then - begin - try - (match undos with - | None -> synchro () - | Some n -> try Pfedit.undo n with _ -> synchro ()); + begin + try + apply_undos undos; sync (fun _ -> let start = if is_empty () then input_buffer#start_iter @@ -1342,7 +1387,8 @@ Please restart and report NOW."; 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; + (!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)" @@ -1377,41 +1423,9 @@ Please restart and report NOW."; self#show_goals; self#clear_message in - begin match last_command with - | {ast=_, (VernacSolve _ | VernacTime (VernacSolve _))} -> - begin - try Pfedit.undo 1; ignore (pop ()); sync update_input () - with _ -> self#backtrack_to_no_lock start - end - | {ast=_,t;reset_info=Reset (id, {contents=true})} -> - ignore (pop ()); - (match t with - | VernacBeginSection _ | VernacDefineModule _ - | VernacDeclareModule _ | VernacDeclareModuleType _ - | VernacEndSegment _ - -> reset_to_mod id - | _ -> reset_to id); - sync update_input () - | { ast = _, ( VernacStartTheoremProof _ - | VernacGoal _ - | VernacDeclareTacticDefinition _ - | VernacDefinition (_,_,ProveBody _,_)); - reset_info=Reset(id,{contents=false})} -> - ignore (pop ()); - (try - Pfedit.delete_current_proof () - with e -> - begin - prerr_endline "WARNING : found a closed environment"; - raise e - end); - sync update_input () - | { ast = (_, a) } when is_state_preserving a -> - ignore (pop ()); - sync update_input () - | _ -> - self#backtrack_to_no_lock start - end; + let undo = pop_command (0,0,NoBacktrack,0,undo_info()) last_command in + apply_undos undo; + sync update_input () with | Size 0 -> (* !flash_info "Nothing to Undo"*)() ); @@ -1533,7 +1547,7 @@ Please restart and report NOW."; deact_id <- Some (input_view#event#connect#key_press self#disconnected_keypress_handler); prerr_endline "CONNECTED inactive : "; - print_id (out_some deact_id) + print_id (Option.get deact_id) method activate () = is_active <- true; @@ -1545,9 +1559,9 @@ Please restart and report NOW."; act_id <- Some (input_view#event#connect#key_press self#active_keypress_handler); prerr_endline "CONNECTED active : "; - print_id (out_some act_id); + print_id (Option.get act_id); match - (out_some ((Vector.get input_views index).analyzed_view)) #filename + (Option.get ((Vector.get input_views index).analyzed_view)) #filename with | None -> () | Some f -> let dir = Filename.dirname f in @@ -1645,7 +1659,7 @@ Please restart and report NOW."; if auto_complete_on && String.length s = 1 && s <> " " && s <> "\n" then - let v = out_some (get_current_view ()).analyzed_view + let v = Option.get (get_current_view ()).analyzed_view in let has_completed = v#complete_at_offset @@ -1662,7 +1676,7 @@ Please restart and report NOW."; (fun () -> if input_buffer#modified then set_tab_image index - ~icon:(match (out_some (current_all.analyzed_view))#filename with + ~icon:(match (Option.get (current_all.analyzed_view))#filename with | None -> `SAVE_AS | Some _ -> `SAVE ) @@ -1899,10 +1913,19 @@ let main files = | Vector.Found i -> set_current_view i | e -> !flash_info ("Load failed: "^(Printexc.to_string e)) in - let load_m = file_factory#add_item "_Open/Create" + 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 ~title:"Load file" () with + match select_file_for_open ~title:"Load file" () with | None -> () | Some f -> load f in @@ -1916,20 +1939,20 @@ let main files = let save_f () = let current = get_current_view () in try - (match (out_some current.analyzed_view)#filename with + (match (Option.get current.analyzed_view)#filename with | None -> - begin match GToolbox.select_file ~title:"Save file" () + begin match select_file_for_save ~title:"Save file" () with | None -> () | Some f -> - if (out_some current.analyzed_view)#save_as f then begin + if (Option.get current.analyzed_view)#save_as f then begin set_current_tab_label (Filename.basename f); !flash_info ("File " ^ f ^ " saved") end else warning ("Save Failed (check if " ^ f ^ " is writable)") end | Some f -> - if (out_some current.analyzed_view)#save f then + if (Option.get current.analyzed_view)#save f then !flash_info ("File " ^ f ^ " saved") else warning ("Save Failed (check if " ^ f ^ " is writable)") @@ -1944,27 +1967,27 @@ let main files = in let saveas_f () = let current = get_current_view () in - try (match (out_some current.analyzed_view)#filename with + try (match (Option.get current.analyzed_view)#filename with | None -> - begin match GToolbox.select_file ~title:"Save file as" () + begin match select_file_for_save ~title:"Save file as" () with | None -> () | Some f -> - if (out_some current.analyzed_view)#save_as f then begin + if (Option.get current.analyzed_view)#save_as f then begin set_current_tab_label (Filename.basename f); !flash_info "Saved" end else !flash_info "Save Failed" end | Some f -> - begin match GToolbox.select_file + begin match select_file_for_save ~dir:(ref (Filename.dirname f)) ~filename:(Filename.basename f) ~title:"Save file as" () with | None -> () | Some f -> - if (out_some current.analyzed_view)#save_as f then begin + if (Option.get current.analyzed_view)#save_as f then begin set_current_tab_label (Filename.basename f); !flash_info "Saved" end else !flash_info "Save Failed" @@ -1974,7 +1997,7 @@ let main files = ignore (saveas_m#connect#activate saveas_f); (* File/Save All Menu *) - let saveall_m = file_factory#add_item "Sa_ve All" in + let saveall_m = file_factory#add_item "Sa_ve all" in let saveall_f () = Vector.iter (function @@ -1997,7 +2020,7 @@ let main files = ignore (saveall_m#connect#activate saveall_f); (* File/Revert Menu *) - let revert_m = file_factory#add_item "_Revert All Buffers" in + let revert_m = file_factory#add_item "_Revert all buffers" in let revert_f () = Vector.iter (function @@ -2018,9 +2041,9 @@ let main files = (* File/Close Menu *) let close_m = - file_factory#add_item "_Close Buffer" ~key:GdkKeysyms._W in + file_factory#add_item "_Close buffer" ~key:GdkKeysyms._W in let close_f () = - let v = out_some !active_view in + let v = Option.get !active_view in let act = get_current_view_page () in if v = act then !flash_info "Cannot close an active view" else remove_current_view_page () @@ -2030,7 +2053,7 @@ let main files = (* File/Print Menu *) let print_f () = let v = get_current_view () in - let av = out_some v.analyzed_view in + let av = Option.get v.analyzed_view in match av#filename with | None -> !flash_info "Cannot print: this buffer has no name" @@ -2040,17 +2063,48 @@ let main files = !current.cmd_coqdoc ^ " -ps " ^ Filename.quote (Filename.basename f) ^ " | " ^ !current.cmd_print in - let s,_ = run_command av#insert_message cmd in - !flash_info (cmd ^ if s = Unix.WEXITED 0 then " succeeded" else " failed") + let print_window = GWindow.window + ~title:"Print" + ~modal:true + ~position:`CENTER + ~wm_class:"CodIDE" + ~wm_name: "CodIDE" () 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(); in - let _ = file_factory#add_item "_Print" + let _ = file_factory#add_item "_Print..." ~key:GdkKeysyms._P ~callback:print_f in (* File/Export to Menu *) let export_f kind () = let v = get_current_view () in - let av = out_some v.analyzed_view in + let av = Option.get v.analyzed_view in match av#filename with | None -> !flash_info "Cannot print: this buffer has no name" @@ -2060,11 +2114,11 @@ let main files = let basef_we = try Filename.chop_extension basef with _ -> basef in match kind with | "latex" -> basef_we ^ ".tex" - | "dvi" | "ps" | "html" -> basef_we ^ "." ^ kind + | "dvi" | "ps" | "pdf" | "html" -> basef_we ^ "." ^ kind | _ -> assert false in let cmd = - "cd " ^ (Filename.quote (Filename.dirname f)) ^ "; " ^ + "cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^ !current.cmd_coqdoc ^ " --" ^ kind ^ " -o " ^ (Filename.quote output) ^ " " ^ (Filename.quote basef) in let s,_ = run_command av#insert_message cmd in @@ -2085,6 +2139,9 @@ let main files = 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 @@ -2095,7 +2152,7 @@ let main files = (fun () -> Highlight.highlight_all (get_current_view()).view#buffer; - (out_some (get_current_view()).analyzed_view)#recenter_insert)); + (Option.get (get_current_view()).analyzed_view)#recenter_insert)); (* File/Quit Menu *) let quit_f () = @@ -2129,7 +2186,7 @@ let main files = ignore(edit_f#add_item "_Undo" ~key:GdkKeysyms._u ~callback: (do_if_not_computing "undo" (fun () -> - ignore ((out_some ((get_current_view()).analyzed_view))# + ignore ((Option.get ((get_current_view()).analyzed_view))# without_auto_complete (fun () -> (get_current_view()).view#undo) ())))); ignore(edit_f#add_item "_Clear Undo Stack" @@ -2203,13 +2260,15 @@ let main files = ~packing: (find_box#attach ~left:1 ~top:1 ~expand:`X) () in - let _ = + (* let _ = GButton.check_button ~label:"case sensitive" ~active:true ~packing: (find_box#attach ~left:1 ~top:2) () - in + + in + *) (* let find_backwards_check = GButton.check_button @@ -2385,7 +2444,7 @@ let main files = ~callback: (do_if_not_computing (fun b -> - let v = out_some (get_current_view ()).analyzed_view + let v = Option.get (get_current_view ()).analyzed_view in v#complete_at_offset ((v#view#buffer#get_iter `SEL_BOUND)#offset) @@ -2397,7 +2456,7 @@ let main files = ignore(edit_f#add_item "Complete Word" ~key:GdkKeysyms._slash ~callback: (fun () -> ignore ( - let av = out_some ((get_current_view()).analyzed_view) in + let av = Option.get ((get_current_view()).analyzed_view) in av#complete_at_offset (av#get_insert)#offset ))); @@ -2406,13 +2465,13 @@ let main files = let _ = edit_f#add_item "External editor" ~callback: (fun () -> - let av = out_some ((get_current_view()).analyzed_view) in + let av = Option.get ((get_current_view()).analyzed_view) in match av#filename with | None -> () | Some f -> save_f (); - let l,r = !current.cmd_editor in - let _ = run_command av#insert_message (l ^ (Filename.quote f) ^ r) in + 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 @@ -2454,7 +2513,7 @@ let main files = let _ = edit_f#add_item "_Preferences" - ~callback:(fun () -> configure ();reset_revert_timer ()) + ~callback:(fun () -> configure ~apply:update_notebook_pos (); reset_revert_timer ()) in (* let save_prefs_m = @@ -2472,7 +2531,7 @@ let main files = in let do_or_activate f () = let current = get_current_view () in - let analyzed_view = out_some current.analyzed_view in + let analyzed_view = Option.get current.analyzed_view in if analyzed_view#is_active then ignore (f analyzed_view) else @@ -2496,7 +2555,7 @@ let main files = end; ignore (toolbar#insert_button ~tooltip - ~text:tooltip +(* ~text:tooltip*) ~icon:(stock_to_widget ~size:`LARGE_TOOLBAR icon) ~callback ()) @@ -2544,8 +2603,7 @@ let main files = ~tooltip:"Interrupt computations" ~key:GdkKeysyms._Break ~callback:break - `STOP - ; + `STOP; (* Tactics Menu *) let tactics_menu = factory#add_submenu "_Try Tactics" in @@ -2557,7 +2615,7 @@ let main files = in let do_if_active_raw f () = let current = get_current_view () in - let analyzed_view = out_some current.analyzed_view in + let analyzed_view = Option.get current.analyzed_view in if analyzed_view#is_active then ignore (f analyzed_view) in let do_if_active f = @@ -2628,6 +2686,8 @@ let main files = )) ()); + + ignore (tactics_factory#add_item "" ~key:GdkKeysyms._dollar ~callback:(do_if_active (fun a -> a#tactic_wizard @@ -2830,6 +2890,14 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); ~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 @@ -2839,6 +2907,84 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); ()) 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 + + (* Unicode *) +(* + let unicode_menu = factory#add_submenu "_Unicode" in + let unicode_factory = new GMenu.factory unicode_menu + ~accel_path:"/Unicode/" + ~accel_group + ~accel_modi:[] + in + let logic_symbols_menu = unicode_factory#add_submenu "Math operators" in + let logic_factory = new GMenu.factory logic_symbols_menu + ~accel_path:"/Unicode/Math operators" + ~accel_group + ~accel_modi:[] + in + let new_unicode_item s = ignore ( + logic_factory#add_item s + ~callback:(fun () -> + let v = get_current_view () in + ignore (v.view#buffer#insert_interactive s))) + in + + for i = 0x2200 to 0x22FF do + List.iter new_unicode_item [Glib.Utf8.from_unichar i]; + + done; + +*) + + (* Externals *) let externals_menu = factory#add_submenu "_Compile" in let externals_factory = new GMenu.factory externals_menu @@ -2850,7 +2996,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); (* Command/Compile Menu *) let compile_f () = let v = get_current_view () in - let av = out_some v.analyzed_view in + let av = Option.get v.analyzed_view in save_f (); match av#filename with | None -> @@ -2877,21 +3023,22 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); (* Command/Make Menu *) let make_f () = let v = get_current_view () in - let av = out_some v.analyzed_view in + let av = Option.get v.analyzed_view in match av#filename with | None -> - !flash_info "Cannot print: this buffer has no name" + !flash_info "Cannot make: this buffer has no name" | Some f -> let cmd = "cd " ^ Filename.quote (Filename.dirname 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") + + (* + 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 @@ -2905,7 +3052,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); let file,line,start,stop,error_msg = search_next_error () in load file; let v = get_current_view () in - let av = out_some v.analyzed_view in + let av = Option.get v.analyzed_view in let input_buffer = v.view#buffer in (* let init = input_buffer#start_iter in @@ -2931,7 +3078,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); with Not_found -> last_make_index := 0; let v = get_current_view () in - let av = out_some v.analyzed_view in + let av = Option.get v.analyzed_view in av#set_message "No more errors.\n" in let _ = @@ -2943,7 +3090,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); (* Command/CoqMakefile Menu*) let coq_makefile_f () = let v = get_current_view () in - let av = out_some v.analyzed_view in + let av = Option.get v.analyzed_view in match av#filename with | None -> !flash_info "Cannot make makefile: this buffer has no name" @@ -2958,20 +3105,24 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); in (* Windows Menu *) let configuration_menu = factory#add_submenu "_Windows" in - let configuration_factory = new GMenu.factory configuration_menu ~accel_path:"/Windows" ~accel_group + let configuration_factory = new GMenu.factory configuration_menu + ~accel_path:"/Windows" + ~accel_modi:[] + ~accel_group in - let _ = + let _ = configuration_factory#add_item - "Show _Query Window" - (* - ~key:GdkKeysyms._F12 - *) - ~callback:(Command_windows.command_window ())#window#present + "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_item + configuration_factory#add_check_item "Show/Hide _Toolbar" - ~callback:(fun () -> + ~callback:(fun _ -> !current.show_toolbar <- not !current.show_toolbar; !show_toolbar !current.show_toolbar) in @@ -2983,8 +3134,15 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); let nb = notebook () in if nb#misc#toplevel#get_oid=w#coerce#get_oid then begin - let nw = GWindow.window ~show:true () in - let parent = out_some nb#misc#parent in + let nw = GWindow.window + ~width:(!current.window_width*2/3) + ~height:(!current.window_height*2/3) + ~position:`CENTER + ~wm_name:"CoqIde" + ~wm_class:"CoqIde" + ~title:"Script" + ~show:true () in + let parent = Option.get nb#misc#parent in ignore (nw#connect#destroy ~callback: (fun () -> nb#misc#reparent parent)); @@ -2993,6 +3151,33 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); end ))) in +(* let _ = configuration_factory#add_item + "Detach _Command Pane" + ~callback: + (do_if_not_computing "detach command pane" (sync + (fun () -> + let command_object = Command_windows.command_window() in + let queries_frame = command_object#frame in + if queries_frame#misc#toplevel#get_oid=w#coerce#get_oid then + begin + let nw = GWindow.window + ~width:(!current.window_width*2/3) + ~height:(!current.window_height*2/3) + ~wm_name:"CoqIde" + ~wm_class:"CoqIde" + ~position:`CENTER + ~title:"Queries" + ~show:true () in + let parent = Option.get queries_frame#misc#parent in + ignore (nw#connect#destroy + ~callback: + (fun () -> queries_frame#misc#reparent parent)); + queries_frame#misc#show(); + queries_frame#misc#reparent nw#coerce + end + ))) + in +*) let _ = configuration_factory#add_item "Detach _View" @@ -3002,8 +3187,9 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); match get_current_view () with | {view=v;analyzed_view=Some av} -> let w = GWindow.window ~show:true - ~width:(!current.window_width/2) - ~height:(!current.window_height) + ~width:(!current.window_width*2/3) + ~height:(!current.window_height*2/3) + ~position:`CENTER ~title:(match av#filename with | None -> "*Unnamed*" | Some f -> f) @@ -3037,17 +3223,17 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); let _ = help_factory#add_item "Browse Coq _Manual" ~callback: (fun () -> - let av = out_some ((get_current_view ()).analyzed_view) in + let av = Option.get ((get_current_view ()).analyzed_view) in browse av#insert_message (!current.doc_url ^ "main.html")) in let _ = help_factory#add_item "Browse Coq _Library" ~callback: (fun () -> - let av = out_some ((get_current_view ()).analyzed_view) in + let av = Option.get ((get_current_view ()).analyzed_view) in browse av#insert_message !current.library_url) in let _ = help_factory#add_item "Help for _keyword" ~key:GdkKeysyms._F1 ~callback:(fun () -> - let av = out_some ((get_current_view ()).analyzed_view) in + let av = Option.get ((get_current_view ()).analyzed_view) in av#help_for_keyword ()) in let _ = help_factory#add_separator () in @@ -3055,19 +3241,20 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); let faq_m = help_factory#add_item "_FAQ" in *) let about_m = help_factory#add_item "_About" in - (* End of menu *) (* The vertical Separator between Scripts and Goals *) - let hb = GPack.paned `HORIZONTAL ~border_width:5 ~packing:vbox#add () in + let queries_pane = GPack.paned `VERTICAL ~packing:(vbox#pack ~expand:true ) () in + let hb = GPack.paned `HORIZONTAL ~border_width:5 ~packing:(queries_pane#pack1 ~shrink:false ~resize:true) () in let fr_notebook = GBin.frame ~shadow_type:`IN ~packing:hb#add1 () in _notebook := Some (GPack.notebook ~border_width:2 ~show_border:false ~scrollable:true ~packing:fr_notebook#add ()); + update_notebook_pos (); let nb = notebook () in let hb2 = GPack.paned `VERTICAL ~packing:hb#add2 () in let fr_a = GBin.frame ~shadow_type:`IN ~packing:hb2#add () in - let fr_b = GBin.frame ~shadow_type:`IN ~packing:hb2#add () in + let fr_b = GBin.frame ~shadow_type:`IN ~packing:hb2#add () in let sw2 = GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC @@ -3076,6 +3263,9 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:(fr_b#add) () 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 let status_bar = GMisc.statusbar ~packing:(lower_hbox#pack ~expand:true) () in @@ -3312,32 +3502,46 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); (fun {view=view} -> view#misc#modify_font fd) input_views; ); - let about (b:GText.buffer) = - (try - let image = lib_ide_file "coq.png" in - let startup_image = GdkPixbuf.from_file image in - b#insert_pixbuf ~iter:b#start_iter - ~pixbuf:startup_image; - b#insert ~iter:b#start_iter "\t\t"; - with _ -> ()); - let about_string = - "\nCoqIDE: an Integrated Development Environment for Coq\n\ + let about_full_string = + "\nCoq is developed by the Coq Development Team\ + \n(INRIA - CNRS - University Paris 11 and partners)\ + \nWeb site: http://coq.inria.fr\ + \nFeature wish or bug report: http://logical.saclay.inria.fr/coq-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\ - \nFeature wish or bug report: use Web interface\n\ - \n\thttp://logical.futurs.inria.fr/coq-bugs\n\ + \n Pierre Letouzey, Claude Marché\ + \n Bruno Barras, Pierre Corbineau\ + \n Julien Narboux, Hugo Herbelin, ... \ + \n\ \nVersion information\ - \n-------------------\n" - in - if Glib.Utf8.validate about_string - then b#insert about_string; - let coq_version = Coq.version () in - if Glib.Utf8.validate coq_version - then b#insert coq_version; - + \n-------------------\ + \n" + in + let initial_about (b:GText.buffer) = + (try + let image = lib_ide_file "coq.png" in + let startup_image = GdkPixbuf.from_file image in + b#insert_pixbuf ~iter:b#start_iter ~pixbuf:startup_image; + b#insert ~iter:b#start_iter "\t\t " + with _ -> ()); + let coq_version = Coq.short_version () in + b#insert ~iter:b#start_iter "\n\n"; + if Glib.Utf8.validate coq_version then b#insert ~iter:b#start_iter coq_version; + b#insert ~iter:b#start_iter "\n " in - about tv2#buffer; + + let about (b:GText.buffer) = + 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 + initial_about tv2#buffer; w#add_accel_group accel_group; (* Remove default pango menu for textviews *) ignore (tv2#event#connect#button_press ~callback: @@ -3395,7 +3599,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); (fun _ -> if !current.contextual_menus_on_goal then begin - let w = (out_some (get_active_view ()).analyzed_view) in + let w = (Option.get (get_active_view ()).analyzed_view) in !push_info "Computing advanced goal's menus"; prerr_endline "Entering Goal Window. Computing Menus...."; w#show_goals_full; @@ -3468,6 +3672,7 @@ let start () = else failwith ("Coqide internal error: " ^ msg))); Command_windows.main (); Blaster_window.main 9; + init_stdout (); main files; if !Coq_config.with_geoproof then ignore (Thread.create check_for_geoproof_input ()); while true do @@ -3480,5 +3685,3 @@ let start () = flush stderr; crash_save 127 done - - -- cgit v1.2.3