diff options
-rw-r--r-- | ide/coqide.ml | 22 | ||||
-rw-r--r-- | test-suite/ide/undo.v | 74 |
2 files changed, 87 insertions, 9 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 1e6892d0d..39e2aa756 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -159,7 +159,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 -> Names.identifier list -> unit + method backtrack_to_no_lock : GText.iter -> Names.identifier option -> unit method clear_message : unit method deactivate : unit -> unit method disconnected_keypress_handler : GdkEvent.Key.t -> bool @@ -1287,16 +1287,20 @@ object(self) | ResetAtDecl (id, {contents=true}) -> if was_refining then (prerr_endline ("Skipping "^Names.string_of_id id); - synchro [id]) + synchro (Some id)) else - reset_to (List.hd (oldest_decl_in_middle_of_proof@[id])) + 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, if any*) - List.iter reset_to oldest_decl_in_middle_of_proof + (* reset oldest decl found before theorem started what *) + (* also aborts the proof; explicitly aborts otherwise *) + if oldest_decl_in_middle_of_proof = None then + Pfedit.delete_current_proof () + else + reset_to (Option.get oldest_decl_in_middle_of_proof) else (prerr_endline ("Skipping "^Names.string_of_id id); - synchro [id]) + synchro (Some id)) | _ -> synchro oldest_decl_in_middle_of_proof end; @@ -1397,7 +1401,7 @@ Please restart and report NOW."; | {ast=_, (VernacSolve _ | VernacTime (VernacSolve _))} -> begin try Pfedit.undo 1; ignore (pop ()); sync update_input () - with _ -> self#backtrack_to_no_lock start [] + with _ -> self#backtrack_to_no_lock start None end | {reset_info=ResetAtSegmentStart (id, {contents=true})} -> @@ -1406,7 +1410,7 @@ Please restart and report NOW."; sync update_input () | {reset_info=ResetAtDecl (id, {contents=true})} -> if Pfedit.refining () then - self#backtrack_to_no_lock start [id] + self#backtrack_to_no_lock start (Some id) else (ignore (pop ()); sync update_input ()) | {reset_info=ResetAtDecl (id,{contents=false})} -> @@ -1423,7 +1427,7 @@ Please restart and report NOW."; ignore (pop ()); sync update_input () | _ -> - self#backtrack_to_no_lock start [] + self#backtrack_to_no_lock start None end; with | Size 0 -> (* !flash_info "Nothing to Undo"*)() diff --git a/test-suite/ide/undo.v b/test-suite/ide/undo.v new file mode 100644 index 000000000..98913ac4e --- /dev/null +++ b/test-suite/ide/undo.v @@ -0,0 +1,74 @@ +(* Here are a sequences of scripts to test interactively with undo and + replay in coqide proof sessions *) + +(* Undoing arbitrary commands, as first step *) + +Theorem a:True. +Set Printing All. +assert True by trivial. +trivial. +Qed. + +(* Undoing arbitrary commands, as non-first step *) + +Theorem a:True. +assert True by trivial. +Set Printing All. +assert True by trivial. +trivial. +Qed. + +(* Undoing declarations, as first step *) +(* was bugged in 8.1 *) + +Theorem a:True. +Inductive T : Type := I. +trivial. +Qed. + +(* Undoing declarations, as first step *) +(* new in 8.2 *) + +Theorem a:True. +Definition b:=O. +Definition c:=O. +assert True by trivial. +trivial. +Qed. + +(* Undoing declarations, as non-first step *) +(* new in 8.2 *) + +Theorem a:True. +assert True by trivial. +Definition b:=O. +Definition c:=O. +assert True by trivial. +trivial. +Qed. + +(* Undoing declarations, interleaved with proof steps *) +(* new in 8.2 *) + +Theorem a:True. +assert True by trivial. +Definition b:=O. +assert True by trivial. +Definition c:=O. +assert True by trivial. +trivial. +Qed. + +(* Undoing declarations, interleaved with proof steps and commands *) +(* new in 8.2 *) + +Theorem a:True. +assert True by trivial. +Definition b:=O. +Set Printing All. +assert True by trivial. +Focus. +Definition c:=O. +assert True by trivial. +trivial. +Qed. |