diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq.ml | 24 | ||||
| -rw-r--r-- | ide/coq.mli | 2 | ||||
| -rw-r--r-- | ide/coqide.ml | 193 | ||||
| -rw-r--r-- | ide/preferences.ml | 15 |
4 files changed, 109 insertions, 125 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index f45bd9f5c2..dc4594292d 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -172,7 +172,7 @@ let make_option_commands () = (if p.printing_coercions then [with_printing_coercions] else [])@ (if p.printing_raw_matching then [with_printing_raw_matching;with_printing_no_synth] else [])@ (if p.printing_no_notation then [with_printing_no_notation] else [])@ - (if p.printing_all then [with_printing_all] else [])@ + (if p.printing_all then [with_printing_all;with_printing_evar_instances;with_printing_universes] else [])@ (if p.printing_evar_instances then [with_printing_evar_instances] else [])@ (if p.printing_universes then [with_printing_universes] else []) @@ -353,7 +353,7 @@ type reset_mark = type reset_info = | NoReset | ResetAtSegmentStart of Names.identifier * bool ref - | ResetAtStatement of reset_mark * bool ref + | ResetAtStatement of bool ref | ResetAtRegisteredObject of reset_mark * bool ref let reset_mark id = match Lib.has_top_frozen_state () with @@ -371,13 +371,11 @@ let compute_reset_info = function | VernacAssumption (_,_ ,(_,((_,id)::_,_))::_) | VernacInductive (_, (((_,id),_,_,_),_) :: _) -> ResetAtRegisteredObject (reset_mark id, ref true) - - | VernacDefinition (_, (_,id), ProveBody _, _) - | VernacStartTheoremProof (_, [Some (_,id), _], _, _) -> - ResetAtStatement (reset_mark id, ref false) - | VernacEndProof _ | VernacExactProof _ | VernacEndSegment _ -> NoReset - | com -> if is_vernac_tactic_command com then NoReset else + | com when is_vernac_goal_starting_command com -> + ResetAtStatement (ref false) + | com when is_vernac_tactic_command com -> NoReset + | _ -> match Lib.has_top_frozen_state () with | Some sp -> ResetAtRegisteredObject (ResetToState sp, ref true) | None -> NoReset @@ -389,15 +387,15 @@ let reset_initial () = let reset_to = function | ResetToId id -> prerr_endline ("Reset called with "^(string_of_id id)); - Vernacentries.abort_refine Lib.reset_name (Util.dummy_loc,id) + Lib.reset_name (Util.dummy_loc,id) | ResetToState sp -> prerr_endline ("Reset called with state "^(Libnames.string_of_path (fst sp))); - Vernacentries.abort_refine Lib.reset_to_state sp + Lib.reset_to_state sp let reset_to_mod id = prerr_endline ("Reset called to Mod/Sect with "^(string_of_id id)); - Vernacentries.abort_refine Lib.reset_mod (Util.dummy_loc,id) + Lib.reset_mod (Util.dummy_loc,id) let raw_interp s = Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s)) @@ -410,14 +408,12 @@ let interp_with_options verbosely options s = match pe with | None -> assert false | Some((loc,vernac) as last) -> - if is_vernac_goal_starting_command vernac & is_in_proof_mode () then - user_error_loc loc (str "CoqIDE do not support nested goals"); if is_vernac_debug_command vernac then user_error_loc loc (str "Debug mode not available within CoqIDE"); if is_vernac_navigation_command vernac then user_error_loc loc (str "Use CoqIDE navigation instead"); if is_vernac_known_option_command vernac then - user_error_loc loc (str "Use CoqIDE buttons instead"); + user_error_loc loc (str "Use CoqIDE display menu instead"); if is_vernac_query_command vernac then !flash_info "Warning: query commands should not be inserted in scripts"; diff --git a/ide/coq.mli b/ide/coq.mli index 930687eae7..cec86ab78b 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -35,7 +35,7 @@ type reset_mark = type reset_info = | NoReset | ResetAtSegmentStart of Names.identifier * bool ref - | ResetAtStatement of reset_mark * bool ref + | ResetAtStatement of bool ref | ResetAtRegisteredObject of reset_mark * bool ref val compute_reset_info : Vernacexpr.vernac_expr -> reset_info diff --git a/ide/coqide.ml b/ide/coqide.ml index a0ea025239..6ac5c779b2 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -160,7 +160,7 @@ object('self) 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 -> reset_mark option -> 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 @@ -507,7 +507,7 @@ let update_on_end_of_proof () = | { reset_info = ResetAtRegisteredObject (_, r) } -> prerr_endline "Toggling Frozen State info to false"; r := false - | { reset_info = ResetAtStatement (_, r) } when not !r -> + | { reset_info = ResetAtStatement r } when not !r -> prerr_endline "Toggling Reset info to true"; r := true; raise Exit | { ast = _, (VernacAbort _ | VernacAbortAll | VernacGoal _) } -> raise Exit @@ -519,7 +519,7 @@ let update_on_end_of_segment id = let lookup_section = function | { reset_info = ResetAtSegmentStart (id', r) } when id = id' -> raise Exit | { reset_info = ResetAtSegmentStart (_, r) } -> r := false - | { reset_info = ResetAtStatement (_, r) } -> r := false + | { reset_info = ResetAtStatement r } -> r := false | { reset_info = ResetAtRegisteredObject (_, r) } -> r := false | _ -> () in @@ -550,6 +550,66 @@ let repush_phrase reset_info x = end; push x +type backtrack = +| BacktrackToNextActiveMark +| BacktrackToMark of reset_mark +| BacktrackToModSec of Names.identifier +| NoBacktrack + +let add_undo (n,a,b) = (n+1,a,b) +let add_abort (n,a,b) = (n,a+1,b) +let add_backtrack (n,a,b) b' = (n,a,b') + +let pop_command undos t = + let undos = + match t with + | {ast=(_,com)} when is_vernac_tactic_command com -> + add_undo undos + | {reset_info=ResetAtRegisteredObject (mark,{contents=true})} -> + add_backtrack undos (BacktrackToMark mark) + | {reset_info=ResetAtSegmentStart (id, {contents=true})} -> + add_backtrack undos (BacktrackToModSec id) + | {reset_info=ResetAtStatement {contents=false}} -> + prerr_endline ("Statement " ^ if Pfedit.refining () then "proof" else "none"); + if Pfedit.refining () then add_abort undos + else add_backtrack undos BacktrackToNextActiveMark + | {ast=(_,com)} -> + if is_vernac_state_preserving_command com then undos + else add_backtrack undos BacktrackToNextActiveMark in + ignore (pop ()); + undos + +let rec apply_backtrack = function + | BacktrackToMark mark -> reset_to mark + | NoBacktrack -> () + | BacktrackToModSec id -> reset_to_mod id + | BacktrackToNextActiveMark -> + (* re-synchronize Coq to the current state of the stack *) + if is_empty () then + Coq.reset_initial () + else + begin + let t = top () in + let (_,_,b) = pop_command (0,0,BacktrackToNextActiveMark) t in + apply_backtrack 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) = + (* Undos *) + if n<>0 then + (prerr_endline ("Applying "^string_of_int n^" undos"); + try Pfedit.undo n + with _ -> apply_undos (n,a,BacktrackToNextActiveMark)); + (* Aborts *) + if a <> 0 then prerr_endline ("Applying "^string_of_int a^" aborts"); + (try Util.repeat a Pfedit.delete_current_proof () + with e -> + begin prerr_endline "WARNING : found a closed environment"; raise e end); + (* Reset *) + apply_backtrack b (* For electric handlers *) exception Found @@ -1275,71 +1335,28 @@ object(self) Coq.reset_initial () (* backtrack Coq to the phrase preceding iterator [i] *) - method backtrack_to_no_lock i oldest_id_to_reset = + method backtrack_to_no_lock i = prerr_endline "Backtracking_to iter starts now."; - let was_refining = Pfedit.refining () in - (* re-synchronize Coq to the current state of the stack *) - let rec synchro oldest_decl_in_middle_of_proof inproof = - if is_empty () then - Coq.reset_initial () - else begin - let t = pop () in - begin match t.reset_info with - | ResetAtSegmentStart (id, {contents=true}) -> - reset_to_mod id - | ResetAtRegisteredObject (mark, {contents=true}) -> - if inproof then synchro (Some mark) inproof - else reset_to mark - | ResetAtStatement (mark, {contents=true}) -> - assert (not inproof); - reset_to (Option.default mark oldest_decl_in_middle_of_proof) - | ResetAtStatement (mark, {contents=false}) -> - if inproof then - if oldest_decl_in_middle_of_proof = None then - match mark with - | ResetToId _ -> synchro None false - | ResetToState _ -> reset_to mark - else - (* reset oldest decl found before theorem started what *) - (* resets back just before the proof was started *) - reset_to (Option.get oldest_decl_in_middle_of_proof) - else - synchro (Some mark) inproof - | _ -> - synchro oldest_decl_in_middle_of_proof inproof - end; - let reset_info = Coq.compute_reset_info (snd t.ast) in - interp_last t.ast; - repush_phrase reset_info 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 + if i#compare (input_buffer#get_iter_at_mark t.stop) < 0 then + begin prerr_endline "Popped top command"; - ignore (pop ()); - let undos = - if is_vernac_tactic_command (snd t.ast) then add_undo undos - else None in - pop_commands true undos - end else - done_smthg, undos + pop_commands true (pop_command undos t) + end + else + done_smthg, undos in - let done_smthg, undos = pop_commands false (Some 0) in + let done_smthg, undos = pop_commands false (0,0,NoBacktrack) in prerr_endline "Popped commands"; if done_smthg then - begin - try - (match undos with - | None -> synchro oldest_id_to_reset was_refining - | Some n -> try Pfedit.undo n with _ -> - synchro oldest_id_to_reset was_refining); + begin + try + apply_undos undos; sync (fun _ -> let start = if is_empty () then input_buffer#start_iter @@ -1368,7 +1385,7 @@ 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 None; Mutex.unlock coq_may_stop; + self#backtrack_to_no_lock i; Mutex.unlock coq_may_stop; !pop_info ()) else prerr_endline "backtrack_to : discarded (lock is busy)" @@ -1403,38 +1420,9 @@ Please restart and report NOW."; self#show_goals; self#clear_message in - begin match last_command with - | {ast=_,com} when is_vernac_tactic_command com -> - begin - try Pfedit.undo 1; ignore (pop ()); sync update_input () - with _ -> self#backtrack_to_no_lock start None - end - - | {reset_info=ResetAtRegisteredObject (mark,{contents=true})} -> - if Pfedit.refining () then - self#backtrack_to_no_lock start (Some mark) - else - (ignore (pop ()); reset_to mark; sync update_input ()) - | {reset_info=ResetAtSegmentStart (id, {contents=true})} -> - ignore (pop ()); - reset_to_mod id; - sync update_input () - | {reset_info=ResetAtStatement (_, {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_vernac_state_preserving_command a -> - ignore (pop ()); - sync update_input () - | _ -> - self#backtrack_to_no_lock start None - end; + let undo = pop_command (0,0,NoBacktrack) last_command in + apply_undos undo; + sync update_input () with | Size 0 -> (* !flash_info "Nothing to Undo"*)() ); @@ -2887,40 +2875,39 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); in let _ = ignore (view_factory#add_check_item - "Toggle printing of _implicit arguments" + "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 - "Toggle printing of _coercions" + "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 - "Toggle printing of raw _matching expressions" + "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 - "Toggle deactivation of _notations" + "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 - "Toggle _full low-level printing" - ~key:GdkKeysyms._f - ~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 - "Toggle printing of _existential variable instances" + "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 - "Toggle printing of _universe levels" + "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._a + ~callback:(fun _ -> printing_state.printing_all <- not printing_state.printing_all; do_or_activate (fun a -> a#show_goals) ())) in (* Unicode *) (* @@ -3073,7 +3060,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); let configuration_menu = factory#add_submenu "_Windows" in let configuration_factory = new GMenu.factory configuration_menu ~accel_path:"<CoqIde MenuBar>/Windows" ~accel_group in - let _ = + let _ = configuration_factory#add_check_item "Show/Hide _Query Pane" (* diff --git a/ide/preferences.ml b/ide/preferences.ml index 802a0c1fe1..253c567881 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -453,10 +453,14 @@ let configure ?(apply=(fun () -> ())) () = (if !current.encoding_use_utf8 then "UTF-8" else if !current.encoding_use_locale then "LOCALE" else !current.encoding_manual) in + let help_string = + "Press a set of modifiers and an extra key together (needs then a restart to apply!)" + in let modifier_for_tactics = modifiers ~allow:!current.modifiers_valid ~f:(fun l -> !current.modifier_for_tactics <- l) + ~help:help_string "Modifiers for Tactics Menu" !current.modifier_for_tactics in @@ -464,6 +468,7 @@ let configure ?(apply=(fun () -> ())) () = modifiers ~allow:!current.modifiers_valid ~f:(fun l -> !current.modifier_for_templates <- l) + ~help:help_string "Modifiers for Templates Menu" !current.modifier_for_templates in @@ -471,6 +476,7 @@ let configure ?(apply=(fun () -> ())) () = modifiers ~allow:!current.modifiers_valid ~f:(fun l -> !current.modifier_for_navigation <- l) + ~help:help_string "Modifiers for Navigation Menu" !current.modifier_for_navigation in @@ -478,6 +484,7 @@ let configure ?(apply=(fun () -> ())) () = modifiers ~allow:!current.modifiers_valid ~f:(fun l -> !current.modifier_for_display <- l) + ~help:help_string "Modifiers for Display Menu" !current.modifier_for_display in @@ -487,12 +494,6 @@ let configure ?(apply=(fun () -> ())) () = "Allowed modifiers" !current.modifiers_valid in - let mod_msg = - string - "Needs restart to apply!" - ~editable:false - "" - in let cmd_editor = let predefined = [ "emacs %s"; "vi %s"; "NOTEPAD %s" ] in combo @@ -570,7 +571,7 @@ let configure ?(apply=(fun () -> ())) () = [automatic_tactics]); Section("Shortcuts", [modifiers_valid; modifier_for_tactics; - modifier_for_templates; modifier_for_display; modifier_for_navigation;mod_msg]); + modifier_for_templates; modifier_for_display; modifier_for_navigation]); Section("Misc", misc)] in |