Partial simplification of undo mechanism, relying only on Courtieu's

marks and no longer on old-fashioned reset to id.


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

3 files changed, 25 insertions, 79 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 2efbe20d38..7f27d3b9f0 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -355,63 +355,29 @@ let is_vernac_tactic_command com =
 let is_vernac_proof_ending_command com =
   List.mem ProofEndingCommand (attribute_of_vernac_command com)
 
-type undo_info = identifier list
+type undo_info = identifier list * int
 
-let undo_info () = Pfedit.get_all_proof_names ()
+let undo_info () = Pfedit.get_all_proof_names (), Pfedit.current_proof_depth()
 
-type reset_mark =
-  | ResetToId of Names.identifier     (* Relying on identifiers only *)
-  | ResetToState of Libnames.object_name (* Relying on states if any *)
+type reset_mark = Libnames.object_name
 
-type reset_status =
-  | NoReset
-  | ResetAtSegmentStart of Names.identifier
-  | ResetAtRegisteredObject of reset_mark
+type reset_info = reset_mark * undo_info * bool ref
 
-type reset_info = reset_status * undo_info * bool ref
-
-
-let reset_mark id = match Lib.has_top_frozen_state () with
-  | Some sp -> 
-      prerr_endline ("On top of state "^Libnames.string_of_path (fst sp));
-      ResetToState sp
-  | None -> ResetToId id
-
-let compute_reset_info = function 
-  | VernacBeginSection id 
-  | VernacDefineModule (_,id, _, _, _) 
-  | VernacDeclareModule (_,id, _, _)
-  | VernacDeclareModuleType (id, _, _) ->
-      ResetAtSegmentStart (snd id), undo_info(), ref true
-
-  | VernacDefinition (_, (_,id), DefineBody _, _)
-  | VernacAssumption (_,_ ,(_,((_,id)::_,_))::_)
-  | VernacInductive (_,_, (((_,(_,id)),_,_,_,_),_) :: _) ->
-      ResetAtRegisteredObject (reset_mark id), undo_info(), ref true
-
-  | com when is_vernac_proof_ending_command com -> NoReset, undo_info(), ref true
-  | VernacEndSegment _ -> NoReset, undo_info(), ref true
-
-  | com when is_vernac_tactic_command com -> NoReset, undo_info(), ref true
-  | _ ->
-      (match Lib.has_top_frozen_state () with
-      | Some sp -> 
-	  prerr_endline ("On top of state "^Libnames.string_of_path (fst sp));
-	  ResetAtRegisteredObject (ResetToState sp)
-      | None -> NoReset), undo_info(), ref true
+let compute_reset_info () =
+  (match Lib.has_top_frozen_state () with
+    | Some st -> 
+	prerr_endline ("On top of state "^Libnames.string_of_path (fst st));
+	st
+    | None -> 
+	failwith "FATAL ERROR: NO RESET"), undo_info(), ref true
 
 let reset_initial () = 
   prerr_endline "Reset initial called"; flush stderr;
   Vernacentries.abort_refine Lib.reset_initial ()
 
-let reset_to = function
-  | ResetToId id ->
-      prerr_endline ("Reset called with "^(string_of_id id));
-      Lib.reset_name (Util.dummy_loc,id)
-  | ResetToState sp ->
-      prerr_endline
-        ("Reset called with state "^(Libnames.string_of_path (fst sp)));
-      Lib.reset_to_state sp
+let reset_to st =
+  prerr_endline ("Reset called with state "^(Libnames.string_of_path (fst st)));
+  Lib.reset_to_state st
 
 let reset_to_mod id = 
   prerr_endline ("Reset called to Mod/Sect with "^(string_of_id id)); 
@@ -443,7 +409,7 @@ let interp_with_options verbosely options s =
 	if not (is_vernac_goal_printing_command vernac) then
 	  (* Verbose if in small step forward and not a tactic *)
 	  Flags.make_silent (not verbosely);
-	let reset_info = compute_reset_info vernac in
+	let reset_info = compute_reset_info () in
 	List.iter (fun (set_option,_) -> raw_interp set_option) options;
 	raw_interp s;
 	Flags.make_silent true;
diff --git a/ide/coq.mli b/ide/coq.mli
index 714cb58cd0..d9b27811e7 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -29,22 +29,15 @@ type printing_state = {
 
 val printing_state : printing_state
 
-type reset_mark =
-  | ResetToId of Names.identifier
-  | ResetToState of Libnames.object_name
+type reset_mark
 
-type reset_status =
-  | NoReset
-  | ResetAtSegmentStart of Names.identifier
-  | ResetAtRegisteredObject of reset_mark
-
-type undo_info = identifier list
+type undo_info = identifier list * int
 
 val undo_info : unit -> undo_info
 
-type reset_info = reset_status * undo_info * bool ref
+type reset_info = reset_mark * undo_info * bool ref
 
-val compute_reset_info : Vernacexpr.vernac_expr -> reset_info
+val compute_reset_info : unit -> reset_info
 val reset_initial : unit -> unit
 val reset_to : reset_mark -> unit
 val reset_to_mod : identifier -> unit
diff --git a/ide/coqide.ml b/ide/coqide.ml
index e67766f926..537da3e438 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -183,7 +183,6 @@ exception Size of int
 
 let update_on_end_of_segment cmd_stk id =
   let lookup_section = function 
-    | { reset_info = ResetAtSegmentStart id',_,_ } when id = id' -> raise Exit
     | { reset_info = _,_,r } -> r := false
   in
     try Stack.iter lookup_section cmd_stk with Exit -> ()
@@ -218,7 +217,6 @@ let repush_phrase cmd_stk reset_info x =
 type backtrack =
 | BacktrackToNextActiveMark
 | BacktrackToMark of reset_mark
-| BacktrackToModSec of Names.identifier
 | NoBacktrack
 
 let add_undo = function (n,a,b,p,l as x) -> if p = 0 then (n+1,a,b,p,l) else x
@@ -229,30 +227,20 @@ let add_qed q (n,a,b,p,l as x) =
   if q = 0 then x else (n,a,BacktrackToNextActiveMark,p+q,l)
 let add_backtrack (n,a,b,p,l) b' = (n,a,b',p,l)
 
-let update_proofs (n,a,b,p,cur_lems) prev_lems =
+let update_proofs (n,a,b,p,(cur_lems,ntacsteps)) (prev_lems,prev_ntacsteps) =
   let ncommon = List.length (Util.list_intersect cur_lems prev_lems) in
   let openproofs = List.length cur_lems - ncommon in
   let closedproofs = List.length prev_lems - ncommon in
-  let undos = (n,a,b,p,prev_lems) in
-  add_qed closedproofs (Util.iterate add_abort openproofs undos)
+  let undos = (n,a,b,p,(prev_lems,prev_ntacsteps)) in
+  let undos = add_qed closedproofs (Util.iterate add_abort openproofs undos) in
+  Util.iterate add_undo (ntacsteps - prev_ntacsteps) undos
 
 let pop_command cmd_stk undos t =
   let (state_info,undo_info,section_info) = t.reset_info in
   let undos =
     if !section_info then
       let undos = update_proofs undos undo_info in
-      match state_info with
-      | _ when is_vernac_tactic_command (snd t.ast) ->
-	  (* A tactic, active if not below a Qed *)
-          add_undo undos
-      | ResetAtRegisteredObject mark ->
-          add_backtrack undos (BacktrackToMark mark)
-      | ResetAtSegmentStart id ->
-          add_backtrack undos (BacktrackToModSec id)
-      | _ when is_vernac_state_preserving_command (snd t.ast) ->
-	  undos
-      | _ ->
-          add_backtrack undos BacktrackToNextActiveMark
+      add_backtrack undos (BacktrackToMark state_info)
     else
       begin 
         prerr_endline "In section";
@@ -282,7 +270,6 @@ let apply_tactic_undo n =
 
 let apply_reset = function
   | BacktrackToMark mark -> reset_to mark
-  | BacktrackToModSec id -> reset_to_mod id
   | NoBacktrack -> ()
   | BacktrackToNextActiveMark -> assert false
 
@@ -304,7 +291,7 @@ let rec apply_undos cmd_stk (n,a,b,p,l as undos) =
       begin
         let t = Stack.top cmd_stk in
         apply_undos cmd_stk (pop_command cmd_stk undos t);
-        let reset_info = Coq.compute_reset_info (snd t.ast) in
+        let reset_info = Coq.compute_reset_info () in
         interp_last t.ast;
         repush_phrase cmd_stk reset_info t
       end