diff options
| -rw-r--r-- | CHANGES | 4 | ||||
| -rw-r--r-- | ide/coq.ml | 4 | ||||
| -rw-r--r-- | ide/coqide.ml | 27 | ||||
| -rw-r--r-- | test-suite/ide/undo.v | 30 |
4 files changed, 34 insertions, 31 deletions
@@ -274,8 +274,10 @@ Setoid rewriting Tools -- New stand-alone .vo files verifier.a +- New stand-alone .vo files verifier "coqchk". - CoqIDE font defaults to monospace so as indentation to be meaningful. +- CoqIDE supports Definition/Parameter/Inductive in middle of a proof. +- Undoing non-tactic commands in CoqIDE works faster. Miscellaneous diff --git a/ide/coq.ml b/ide/coq.ml index 41a6abad4..4e0150918 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -231,8 +231,8 @@ let rec attribute_of_vernac_command = function | VernacUndoTo _ -> [NavigationCommand] | VernacBacktrack _ -> [NavigationCommand] - | VernacFocus _ -> [] - | VernacUnfocus -> [] + | VernacFocus _ -> [SolveCommand] + | VernacUnfocus -> [SolveCommand] | VernacGo _ -> [] | VernacShow _ -> [OtherStatePreservingCommand] | VernacCheckGuard -> [OtherStatePreservingCommand] diff --git a/ide/coqide.ml b/ide/coqide.ml index 39e2aa756..4420fcceb 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1276,7 +1276,7 @@ object(self) 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 = + let rec synchro oldest_decl_in_middle_of_proof inproof = if is_empty () then Coq.reset_initial () else begin @@ -1285,24 +1285,24 @@ object(self) | ResetAtSegmentStart (id, {contents=true}) -> reset_to_mod id | ResetAtDecl (id, {contents=true}) -> - if was_refining then + if inproof then (prerr_endline ("Skipping "^Names.string_of_id id); - synchro (Some id)) + synchro (Some id) inproof) else reset_to (Option.default id oldest_decl_in_middle_of_proof) | ResetAtDecl (id, {contents=false}) -> - if was_refining then - (* reset oldest decl found before theorem started what *) - (* also aborts the proof; explicitly aborts otherwise *) + if inproof then if oldest_decl_in_middle_of_proof = None then - Pfedit.delete_current_proof () + synchro None false 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 (prerr_endline ("Skipping "^Names.string_of_id id); - synchro (Some id)) + synchro (Some id) inproof) | _ -> - synchro oldest_decl_in_middle_of_proof + synchro oldest_decl_in_middle_of_proof inproof end; interp_last t.ast; repush_phrase t @@ -1332,8 +1332,9 @@ object(self) begin try (match undos with - | None -> synchro oldest_id_to_reset - | Some n -> try Pfedit.undo n with _ -> synchro oldest_id_to_reset); + | None -> synchro oldest_id_to_reset was_refining + | Some n -> try Pfedit.undo n with _ -> + synchro oldest_id_to_reset was_refining); sync (fun _ -> let start = if is_empty () then input_buffer#start_iter @@ -1362,7 +1363,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 []; Mutex.unlock coq_may_stop; + self#backtrack_to_no_lock i None; Mutex.unlock coq_may_stop; !pop_info ()) else prerr_endline "backtrack_to : discarded (lock is busy)" @@ -1398,7 +1399,7 @@ Please restart and report NOW."; self#clear_message in begin match last_command with - | {ast=_, (VernacSolve _ | VernacTime (VernacSolve _))} -> + | {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 diff --git a/test-suite/ide/undo.v b/test-suite/ide/undo.v index 98913ac4e..a76817a87 100644 --- a/test-suite/ide/undo.v +++ b/test-suite/ide/undo.v @@ -3,7 +3,7 @@ (* Undoing arbitrary commands, as first step *) -Theorem a:True. +Theorem a : O=O. Set Printing All. assert True by trivial. trivial. @@ -11,7 +11,7 @@ Qed. (* Undoing arbitrary commands, as non-first step *) -Theorem a:True. +Theorem b : O=O. assert True by trivial. Set Printing All. assert True by trivial. @@ -21,7 +21,7 @@ Qed. (* Undoing declarations, as first step *) (* was bugged in 8.1 *) -Theorem a:True. +Theorem c : O=O. Inductive T : Type := I. trivial. Qed. @@ -29,9 +29,9 @@ Qed. (* Undoing declarations, as first step *) (* new in 8.2 *) -Theorem a:True. -Definition b:=O. -Definition c:=O. +Theorem d : O=O. +Definition e := O. +Definition f := O. assert True by trivial. trivial. Qed. @@ -39,10 +39,10 @@ Qed. (* Undoing declarations, as non-first step *) (* new in 8.2 *) -Theorem a:True. +Theorem h : O=O. assert True by trivial. -Definition b:=O. -Definition c:=O. +Definition i := O. +Definition j := O. assert True by trivial. trivial. Qed. @@ -50,11 +50,11 @@ Qed. (* Undoing declarations, interleaved with proof steps *) (* new in 8.2 *) -Theorem a:True. +Theorem k : O=O. assert True by trivial. -Definition b:=O. +Definition l := O. assert True by trivial. -Definition c:=O. +Definition m := O. assert True by trivial. trivial. Qed. @@ -62,13 +62,13 @@ Qed. (* Undoing declarations, interleaved with proof steps and commands *) (* new in 8.2 *) -Theorem a:True. +Theorem n : O=O. assert True by trivial. -Definition b:=O. +Definition o := O. Set Printing All. assert True by trivial. Focus. -Definition c:=O. +Definition p := O. assert True by trivial. trivial. Qed. |