Fixed coqide bug #1856 that was introduced in revision 10915.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10950 85f007b7-540e-0410-9357-904b9bb8a0f7

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.