New API for backtracking.

Aside the command stack, the only parameter is the number of step to go
back. Went back and forth without sync losses on tests-suite/ide/undo.v.

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

3 files changed, 152 insertions, 157 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index f27117c07..c2799931a 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -305,6 +305,8 @@ type annotated_vernac =
   | PureVernac of vernac_expr
  
 
+let comm_stack = Stack.create ()
+
 let parsable_of_string s =
   Pcoq.Gram.parsable (Stream.of_string s)
 
@@ -332,123 +334,67 @@ type reset_info = {
 }
 
 let compute_reset_info loc_ast = 
-  let status = match snd loc_ast with
-    | com when is_vernac_tactic_command com -> NoReset
-    | com when is_vernac_state_preserving_command com -> NoReset 
-    | com when is_vernac_proof_ending_command com -> NoReset
-    | VernacEndSegment _ -> NoReset
+  let status,_ = match snd loc_ast with
+    | com when is_vernac_tactic_command com ->
+        NoReset,None (*Some (Pfedit.get_current_proof_name (),Pfedit.current_proof_depth ()) *)
+    | com when is_vernac_state_preserving_command com -> NoReset,None
+    | com when is_vernac_proof_ending_command com -> NoReset,None
+    | VernacEndSegment _ -> NoReset,None
     | _ ->
         (match Lib.has_top_frozen_state () with
            | Some sp -> 
                prerr_endline ("On top of state "^Libnames.string_of_path (fst sp));
-               ResetAtMark sp
-           | None -> NoReset)
+               ResetAtMark sp,None
+           | None -> NoReset,None)
   in
   { status = status;
     proofs = Pfedit.get_all_proof_names ();
     loc_ast = loc_ast; 
   }
 
-let push_phrase cmd_stk reset_info ide_payload =
-  Stack.push (ide_payload,reset_info) cmd_stk
-
-type backtrack =
-  | BacktrackToNextActiveMark
-  | BacktrackToMark of Libnames.object_name
-  | NoBacktrack
-
-type undo_cmds = int * int * backtrack * int * identifier list
-
-let init_undo_cmds u =
-  (0,0,NoBacktrack,0,undo_info u)
-
-let add_undo = function (n,a,b,p,l as x) -> if p = 0 then (n+1,a,b,p,l) else x
-let add_abort = function
-  | (n,a,b,0,l) -> (0,a+1,b,0,l)
-  | (n,a,b,p,l) -> (n,a,b,p-1,l)
-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 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 eval_expr cmd_stk loc_ast ide_payload =
   let rewind_info = compute_reset_info loc_ast in
   Vernac.eval_expr loc_ast;
-  Stack.push (ide_payload,rewind_info) cmd_stk
+  Stack.push (ide_payload,rewind_info) cmd_stk;
+  Stack.length cmd_stk
 
 let rewind cmd_stk count =
-  let undo_ops = Queue.create () in
+  let undo_ops = Hashtbl.create count in
   let current_proofs = undo_info () in
   let rec do_rewind count reset_op prev_proofs =
     if (count <= 0) && (reset_op <> NoReset) &&
-       (Util.list_subtract prev_proofs current_proofs = []) then
+       (Util.list_subset prev_proofs current_proofs) then
       (* We backtracked at least what we wanted to, we have no proof to reopen,
        * and we don't need to find a reset mark *)
-      begin(*
-        apply_aborts (Util.list_subtract current_proofs prev_proofs);
-        apply_undos undo_ops;
-        apply_reset reset_op*)()
+      begin
+        List.iter
+          (fun id -> Pfedit.delete_proof (Util.dummy_loc,id))
+          (Util.list_subtract current_proofs prev_proofs);(*
+        Hashtbl.iter
+          (fun id depth ->
+             Pfedit.resume_proof (Util.dummy_loc,id);
+             Pfedit.undo_todepth depth)
+          undo_ops;
+        match reset_op with
+          | NoReset -> ()
+          | ResetToMark m -> Lib.reset_to_state sp
+          | ResetToNextMark -> assert false
+        *)()
       end
     else
       begin
         let ide,coq = Stack.pop cmd_stk in
-        if is_vernac_tactic_command (snd coq.loc_ast) then Queue.push () undo_ops;
+        if is_vernac_tactic_command (snd coq.loc_ast) then Hashtbl.add undo_ops () ();
         do_rewind (pred count) (if coq.status <> NoReset then coq.status else reset_op) coq.proofs;
         if count < 0 then begin
           (* we had to backtrack further to find a suitable anchor point,
            * replaying *)
-          eval_expr cmd_stk coq.loc_ast ide;
+          ignore (eval_expr cmd_stk coq.loc_ast ide);
         end
       end
   in
   do_rewind count NoReset current_proofs
 
-let pop_command cmd_stk undos =
-  let (_,t) = Stack.top cmd_stk in
-  let (state_info,undo_info) = t.status,t.proofs in
-  let undos = update_proofs undos undo_info in
-  ignore (Stack.pop cmd_stk);
-  match state_info with
-    | _ when is_vernac_tactic_command (snd t.loc_ast) ->
-        (* A tactic, active if not * below a Qed *)
-        add_undo undos
-    | ResetAtMark mark ->
-        add_backtrack undos (BacktrackToMark mark)
-    | _ when is_vernac_state_preserving_command (snd t.loc_ast) ->
-        undos
-    | _ ->
-        add_backtrack undos BacktrackToNextActiveMark
-
-(* appelle Pfedit.delete_current_proof a fois
-*  * utiliser Vernacentries.vernac_abort a la place ? *)
-let apply_aborts a =
-  if a <> 0 then prerr_endline ("Applying "^string_of_int a^" aborts");
-  try Util.repeat a Pfedit.delete_current_proof ()
-  with e -> prerr_endline "WARNING : found a closed environment"; raise e
-
-exception UndoStackExhausted
-
-(* appelle Pfedit.undo n fois
- * utiliser vernac_undo ? *)
-let apply_tactic_undo n =
-  if n<>0 then
-    (prerr_endline ("Applying "^string_of_int n^" undos");
-     try Pfedit.undo n with _ -> raise UndoStackExhausted)
-
-
-let apply_reset = function
-  | BacktrackToMark mark -> reset_to mark
-  | NoBacktrack -> ()
-  | BacktrackToNextActiveMark -> assert false
-
-
-
 
 module PrintOpt =
 struct
@@ -506,7 +452,7 @@ let interp_with_options verbosely s =
     Vernac.eval_expr (loc,vernac);
     Flags.make_silent true;
     prerr_endline ("...Done with interp of : "^s);
-    reset_info
+    reset_info(* ,Stack.length comm_stack *)
   with Vernac.End_of_input -> assert false
 
 let interp verbosely phrase =
@@ -556,28 +502,92 @@ let interp_last last =
     let s,_ = process_exn e in prerr_endline ("Replay during undo failed because: "^s);
     raise e
 
-let rec apply_undos cmd_stk (n,a,b,p,l as undos) =
-  if p = 0 & b <> BacktrackToNextActiveMark then
-    begin
-      apply_aborts a;
-      try
-        apply_tactic_undo n;
-        apply_reset b
-      with UndoStackExhausted ->
-        apply_undos cmd_stk (n,0,BacktrackToNextActiveMark,p,l)
-    end
-  else
-    (* re-synchronize Coq to the current state of the stack *)
-    if Stack.is_empty cmd_stk then
-      reset_initial ()
-    else
+let push_phrase cmd_stk reset_info ide_payload =
+  Stack.push (ide_payload,reset_info) cmd_stk
+
+type backtrack =
+  | BacktrackToNextActiveMark
+  | BacktrackToMark of Libnames.object_name
+  | NoBacktrack
+
+let add_undo = function (n,a,b,p,l as x) -> if p = 0 then (n+1,a,b,p,l) else x
+let add_abort = function
+  | (n,a,b,0,l) -> (0,a+1,b,0,l)
+  | (n,a,b,p,l) -> (n,a,b,p-1,l)
+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 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 pop_command cmd_stk undos =
+  let (_,t) = Stack.top cmd_stk in
+  let (state_info,undo_info) = t.status,t.proofs in
+  let undos = update_proofs undos undo_info in
+  ignore (Stack.pop cmd_stk);
+  match state_info with
+    | _ when is_vernac_tactic_command (snd t.loc_ast) ->
+        (* A tactic, active if not * below a Qed *)
+        add_undo undos
+    | ResetAtMark mark ->
+        add_backtrack undos (BacktrackToMark mark)
+    | _ when is_vernac_state_preserving_command (snd t.loc_ast) ->
+        undos
+    | _ ->
+        add_backtrack undos BacktrackToNextActiveMark
+
+(* appelle Pfedit.delete_current_proof a fois
+*  * utiliser Vernacentries.vernac_abort a la place ? *)
+let apply_aborts a =
+  if a <> 0 then prerr_endline ("Applying "^string_of_int a^" aborts");
+  try Util.repeat a Pfedit.delete_current_proof ()
+  with e -> prerr_endline "WARNING : found a closed environment"; raise e
+
+exception UndoStackExhausted
+
+(* appelle Pfedit.undo n fois
+ * utiliser vernac_undo ? *)
+let apply_tactic_undo n =
+  if n<>0 then
+    (prerr_endline ("Applying "^string_of_int n^" undos");
+     try Pfedit.undo n with _ -> raise UndoStackExhausted)
+
+
+let apply_reset = function
+  | BacktrackToMark mark -> reset_to mark
+  | NoBacktrack -> ()
+  | BacktrackToNextActiveMark -> assert false
+
+let old_rewind count cmd_stk =
+  let rec do_rewind count n_undo n_abort reset_op n_closed prev_proofs =
+    if (count <= 0) && (reset_op <> BacktrackToNextActiveMark) && (n_closed = 0) then
       begin
-        let (ide_ri,coq_ri) = Stack.top cmd_stk in
-        apply_undos cmd_stk (pop_command cmd_stk undos);
-        let reset_info = compute_reset_info coq_ri.loc_ast in
-        interp_last coq_ri.loc_ast;
-        push_phrase cmd_stk reset_info ide_ri
+        apply_aborts n_abort;
+        try
+          apply_tactic_undo n_undo;
+          apply_reset reset_op
+        with UndoStackExhausted ->
+          do_rewind 0 n_undo 0 BacktrackToNextActiveMark n_closed prev_proofs
       end
+    else
+      if Stack.is_empty cmd_stk then
+        reset_initial ()
+      else
+        begin
+          let ide,coq = Stack.top cmd_stk in
+          let (n_undo,n_abort,reset_op,n_closed,prev_proofs) =
+            pop_command cmd_stk (n_undo,n_abort,reset_op,n_closed,prev_proofs) in
+          do_rewind (pred count) n_undo n_abort reset_op n_closed prev_proofs;
+          if count <= 0 then ignore (eval_expr cmd_stk coq.loc_ast ide);
+        end
+  in
+  do_rewind count 0 0 NoBacktrack 0 (undo_info ());
+
 
 type  tried_tactic =
   | Interrupted
diff --git a/ide/coq.mli b/ide/coq.mli
index 27a0dfe45..e863288cd 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -54,10 +54,7 @@ val interp_and_replace : string ->
 
 val push_phrase : ('a * reset_info) Stack.t -> reset_info -> 'a -> unit
 
-type undo_cmds
-val init_undo_cmds : unit -> undo_cmds
-val pop_command : ('a * reset_info) Stack.t -> undo_cmds -> undo_cmds
-val apply_undos : ('a * reset_info) Stack.t -> undo_cmds -> unit
+val old_rewind : int -> ('a * reset_info) Stack.t -> unit
 
 val is_vernac_tactic_command : Vernacexpr.vernac_expr -> bool
 val is_vernac_state_preserving_command : Vernacexpr.vernac_expr -> bool
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 2055053a8..fafc28b06 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -104,7 +104,6 @@ type viewable_script =
      proof_view : GText.view;
      message_view : GText.view;
      analyzed_view : analyzed_views;
-     command_stack : (ide_info * Coq.reset_info) Stack.t;
     }
 
 
@@ -1174,50 +1173,41 @@ object(self)
   method backtrack_to_no_lock i =
     prerr_endline "Backtracking_to iter starts now.";
     (* pop Coq commands until we reach iterator [i] *)
-    let  rec pop_commands done_smthg undos =
-      if Stack.is_empty cmd_stack then
-        done_smthg, undos
-      else
-        let (ide_ri,_) = Stack.top cmd_stack in
-          if i#compare (input_buffer#get_iter_at_mark ide_ri.stop) < 0 then
-            begin
-              prerr_endline "Popped top command";
-              pop_commands true (pop_command cmd_stack undos)
-            end
-          else
-            done_smthg, undos
+    let itstk = Stack.copy cmd_stack in
+    let rec n_step n =
+      if Stack.is_empty itstk then n else
+        let ide_ri,_ = Stack.pop itstk in
+        if i#compare (input_buffer#get_iter_at_mark ide_ri.stop) < 0 then
+          n_step (succ n)
+        else
+          n
     in
-    let undos = init_undo_cmds () in
-    let done_smthg, undos = pop_commands false undos in
-      prerr_endline "Popped commands";
-      if done_smthg then
-        begin
-          try
-            apply_undos cmd_stack undos;
-            sync (fun _ ->
-                    let start =
-                      if Stack.is_empty cmd_stack then input_buffer#start_iter
-                      else input_buffer#get_iter_at_mark (fst (Stack.top cmd_stack)).stop in
-                      prerr_endline "Removing (long) processed tag...";
-                      input_buffer#remove_tag
-                        Tags.Script.processed
-                        ~start
-                        ~stop:self#get_start_of_input;
-                      input_buffer#remove_tag
-                        Tags.Script.unjustified
-                        ~start
-                        ~stop:self#get_start_of_input;
-                      prerr_endline "Moving (long) start_of_input...";
-                      input_buffer#move_mark ~where:start (`NAME "start_of_input");
-                      self#show_goals;
-                      clear_stdout ();
-                      self#clear_message)
-              ();
-          with _ ->
-            push_info "WARNING: undo failed badly -> Coq might be in an inconsistent state.
-                                                                     Please restart and report NOW.";
-        end
-      else prerr_endline "backtrack_to : discarded (...)"
+    begin
+      try
+        old_rewind (n_step 0) cmd_stack;
+        sync (fun _ ->
+                let start =
+                  if Stack.is_empty cmd_stack then input_buffer#start_iter
+                  else input_buffer#get_iter_at_mark (fst (Stack.top cmd_stack)).stop in
+                prerr_endline "Removing (long) processed tag...";
+                input_buffer#remove_tag
+                  Tags.Script.processed
+                  ~start
+                  ~stop:self#get_start_of_input;
+                input_buffer#remove_tag
+                  Tags.Script.unjustified
+                  ~start
+                  ~stop:self#get_start_of_input;
+                prerr_endline "Moving (long) start_of_input...";
+                input_buffer#move_mark ~where:start (`NAME "start_of_input");
+                self#show_goals;
+                clear_stdout ();
+                self#clear_message)
+          ();
+      with _ ->
+        push_info "WARNING: undo failed badly -> Coq might be in an inconsistent state.
+                                                                 Please restart and report NOW.";
+    end
 
   method backtrack_to i =
     if Mutex.try_lock coq_may_stop then
@@ -1257,9 +1247,8 @@ object(self)
             self#show_goals;
             self#clear_message
           in
-          let undo = pop_command cmd_stack (init_undo_cmds ()) in
-            apply_undos cmd_stack undo;
-            sync update_input ()
+          old_rewind 1 cmd_stack;
+          sync update_input ()
         with
           | Stack.Empty -> (* flash_info "Nothing to Undo"*)()
        );
@@ -1591,7 +1580,6 @@ let create_session () =
       proof_view=proof;
       message_view=message;
       analyzed_view=legacy_av;
-      command_stack=stack;
       encoding=""
     }