Réorganisation des points d'appui du undo de CoqIDE (type reset_info).

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

3 files changed, 24 insertions, 42 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index dce435087..889e4bff5 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -347,9 +347,9 @@ type reset_mark =
 
 type reset_info =
   | NoReset
-  | ResetAtDecl of reset_mark * bool ref
   | ResetAtSegmentStart of Names.identifier * bool ref 
-  | ResetAtFrozenState of Libnames.object_name * bool ref
+  | ResetAtStatement of reset_mark * bool ref
+  | ResetAtRegisteredObject of reset_mark * bool ref
 
 let reset_mark id = match Lib.has_top_frozen_state () with
   | Some sp -> ResetToState sp
@@ -365,15 +365,15 @@ let compute_reset_info = function
   | VernacDefinition (_, (_,id), DefineBody _, _)
   | VernacAssumption (_,_ ,(_,((_,id)::_,_))::_)
   | VernacInductive (_, (((_,id),_,_,_),_) :: _) ->
-      ResetAtDecl (reset_mark id, ref true)
+      ResetAtRegisteredObject (reset_mark id, ref true)
 
   | VernacDefinition (_, (_,id), ProveBody _, _)
   | VernacStartTheoremProof (_, [Some (_,id), _], _, _) ->
-      ResetAtDecl (reset_mark id, ref false)
+      ResetAtStatement (reset_mark id, ref false)
 
   | VernacEndProof _ | VernacEndSegment _ -> NoReset
   | _ -> match Lib.has_top_frozen_state () with
-      | Some sp -> ResetAtFrozenState (sp, ref true)
+      | Some sp -> ResetAtRegisteredObject (ResetToState sp, ref true)
       | None -> NoReset
 
 let reset_initial () = 
diff --git a/ide/coq.mli b/ide/coq.mli
index cbc763df8..1d5a1f2e6 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -33,9 +33,9 @@ type reset_mark =
 
 type reset_info =
   | NoReset
-  | ResetAtDecl of reset_mark * bool ref
   | ResetAtSegmentStart of Names.identifier * bool ref 
-  | ResetAtFrozenState of Libnames.object_name * bool ref
+  | ResetAtStatement of reset_mark * bool ref
+  | ResetAtRegisteredObject of reset_mark * bool ref
 
 val compute_reset_info : Vernacexpr.vernac_expr -> reset_info
 val reset_initial : unit -> unit
diff --git a/ide/coqide.ml b/ide/coqide.ml
index c3d10a898..a29a2519d 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -503,18 +503,12 @@ let is_empty () = Stack.is_empty processed_stack
 
 let update_on_end_of_proof () =
   let lookup_lemma = function
-    | { reset_info = ResetAtFrozenState (_, r) } -> 
+    | { reset_info = ResetAtRegisteredObject (_, r) } -> 
 	prerr_endline "Toggling Frozen State info to false";
 	r := false
-    | { reset_info = ResetAtDecl (_, r) } ->
-	if not !r then begin
-	    prerr_endline "Toggling Reset info to true";
-	    r := true; raise Exit end
-	else begin
-	  (* Hide the Definition done since last started proof *)
-	    prerr_endline "Toggling Changing Reset id"; 
-	    r := false
-	  end
+    | { reset_info = ResetAtStatement (_, r) } when not !r ->
+	prerr_endline "Toggling Reset info to true";
+	r := true; raise Exit
     | { ast = _, (VernacAbort _ | VernacAbortAll | VernacGoal _) } -> raise Exit
     | _ -> ()
   in
@@ -524,8 +518,8 @@ 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 = ResetAtDecl (_, r) } -> r := false
-    | { reset_info = ResetAtFrozenState (_, r) } -> r := false
+    | { reset_info = ResetAtStatement (_, r) } -> r := false
+    | { reset_info = ResetAtRegisteredObject (_, r) } -> r := false
     | _ -> ()
   in
     try Stack.iter lookup_section processed_stack with Exit -> ()
@@ -1292,18 +1286,13 @@ object(self)
 	    begin match t.reset_info with
 	      | ResetAtSegmentStart (id, {contents=true}) ->
 		  reset_to_mod id
-	      | ResetAtFrozenState (sp, {contents=true}) ->
-		  if inproof then
-		    synchro (Some (ResetToState sp)) inproof
-		  else
-		    reset_to (ResetToState sp)
-	      | ResetAtDecl (mark, {contents=true}) ->
-		  if inproof then
-		    synchro (Some mark) inproof
-		  else
-		    reset_to
-		      (Option.default mark oldest_decl_in_middle_of_proof)
-	      | ResetAtDecl (mark, {contents=false}) ->
+	      | 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
@@ -1420,23 +1409,16 @@ Please restart and report NOW.";
 		      with _ -> self#backtrack_to_no_lock start None
 		    end
 
-		| {reset_info=ResetAtFrozenState (sp, {contents=true})} ->
+		| {reset_info=ResetAtRegisteredObject (mark,{contents=true})} ->
 		    if Pfedit.refining () then
-		      self#backtrack_to_no_lock start (Some (ResetToState sp))
+		      self#backtrack_to_no_lock start (Some mark)
 		    else
-		      (ignore (pop ());
-		       reset_to (ResetToState sp);
-		       sync update_input ())
+		      (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=ResetAtDecl (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=ResetAtDecl (_, {contents=false})} ->
+		| {reset_info=ResetAtStatement (_, {contents=false})} ->
 		    ignore (pop ());
 		    (try 
 			 Pfedit.delete_current_proof ()