Introducing a dual stack setup

The first stack lives in coqide and tracks the tagging and locking, the
second lives in coq and tracks the commands.

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

3 files changed, 61 insertions, 92 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index c2799931a2..cb4ce46569 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -304,14 +304,24 @@ type annotated_vernac =
   | ControlVernac of vernac_expr * string (* navigation, debug, process control, print opts *)
   | PureVernac of vernac_expr
  
+type reset_status =
+  | NoReset
+  | ResetAtMark of Libnames.object_name
+
+type reset_info = {
+  status : reset_status;
+  proofs : identifier list;
+  loc_ast : Util.loc * Vernacexpr.vernac_expr;
+}
 
-let comm_stack = Stack.create ()
+let com_stk = Stack.create ()
 
 let parsable_of_string s =
   Pcoq.Gram.parsable (Stream.of_string s)
 
 let reset_initial () =
   prerr_endline "Reset initial called"; flush stderr;
+  Stack.clear com_stk;
   Vernacentries.abort_refine Lib.reset_initial ()
 
 let reset_to sp =
@@ -319,20 +329,8 @@ let reset_to sp =
         ("Reset called with state "^(Libnames.string_of_path (fst sp)));
       Lib.reset_to_state sp
 
-type undo_info = identifier list
-
 let undo_info () = Pfedit.get_all_proof_names ()
 
-type reset_status =
-  | NoReset
-  | ResetAtMark of Libnames.object_name
-
-type reset_info = {
-  status : reset_status;
-  proofs : identifier list;
-  loc_ast : Util.loc * Vernacexpr.vernac_expr;
-}
-
 let compute_reset_info loc_ast = 
   let status,_ = match snd loc_ast with
     | com when is_vernac_tactic_command com ->
@@ -352,12 +350,39 @@ let compute_reset_info loc_ast =
     loc_ast = loc_ast; 
   }
 
-let eval_expr cmd_stk loc_ast ide_payload =
+let eval_expr cmd_stk loc_ast =
   let rewind_info = compute_reset_info loc_ast in
   Vernac.eval_expr loc_ast;
-  Stack.push (ide_payload,rewind_info) cmd_stk;
+  Stack.push ((),rewind_info) cmd_stk;
   Stack.length cmd_stk
 
+let interp_with_options verbosely s =
+  prerr_endline "Starting interp...";
+  prerr_endline s;
+  let pa = parsable_of_string s in
+  try
+    let (loc,vernac) = Vernac.parse_sentence (pa,None) in
+  (* Temporary hack to make coqide.byte work (WTF???) - now with less screen
+  * pollution *)
+    Pervasives.prerr_string " \r"; Pervasives.flush stderr;
+    if is_vernac_debug_command vernac then
+      user_error_loc loc (str "Debug mode not available within CoqIDE");
+    if is_vernac_navigation_command vernac then
+      user_error_loc loc (str "Use CoqIDE navigation instead");
+    if is_vernac_known_option_command vernac then
+      user_error_loc loc (str "Use CoqIDE display menu instead");
+    if is_vernac_query_command vernac then
+      flash_info
+        "Warning: query commands should not be inserted in scripts";
+    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 stack_depth = eval_expr com_stk (loc,vernac) in
+    Flags.make_silent true;
+    prerr_endline ("...Done with interp of : "^s);
+    stack_depth
+  with Vernac.End_of_input -> assert false
+
 let rewind cmd_stk count =
   let undo_ops = Hashtbl.create count in
   let current_proofs = undo_info () in
@@ -383,13 +408,13 @@ let rewind cmd_stk count =
       end
     else
       begin
-        let ide,coq = Stack.pop cmd_stk in
+        let _,coq = Stack.pop cmd_stk in
         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 *)
-          ignore (eval_expr cmd_stk coq.loc_ast ide);
+          ignore (eval_expr cmd_stk coq.loc_ast);
         end
       end
   in
@@ -427,33 +452,6 @@ let forbid_vernac blacklist (loc,vernac) =
   List.map (fun (test,err) -> if test vernac then err loc
  *)
 
-let interp_with_options verbosely s =
-  prerr_endline "Starting interp...";
-  prerr_endline s;
-  let pa = parsable_of_string s in
-  try
-    let (loc,vernac) = Vernac.parse_sentence (pa,None) in
-  (* Temporary hack to make coqide.byte work (WTF???) - now with less screen
-  * pollution *)
-    Pervasives.prerr_string " \r"; Pervasives.flush stderr;
-    if is_vernac_debug_command vernac then
-      user_error_loc loc (str "Debug mode not available within CoqIDE");
-    if is_vernac_navigation_command vernac then
-      user_error_loc loc (str "Use CoqIDE navigation instead");
-    if is_vernac_known_option_command vernac then
-      user_error_loc loc (str "Use CoqIDE display menu instead");
-    if is_vernac_query_command vernac then
-      flash_info
-        "Warning: query commands should not be inserted in scripts";
-    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 (loc,vernac) in
-    Vernac.eval_expr (loc,vernac);
-    Flags.make_silent true;
-    prerr_endline ("...Done with interp of : "^s);
-    reset_info(* ,Stack.length comm_stack *)
-  with Vernac.End_of_input -> assert false
 
 let interp verbosely phrase =
   interp_with_options verbosely phrase
@@ -495,16 +493,6 @@ let print_toplevel_error exc =
 
 let process_exn e = let s,loc= print_toplevel_error e in (msgnl s,loc)
 
-let interp_last last =
-  prerr_string "*";
-  try Vernac.eval_expr last
-  with e ->
-    let s,_ = process_exn e in prerr_endline ("Replay during undo failed because: "^s);
-    raise e
-
-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
@@ -563,7 +551,8 @@ let apply_reset = function
   | NoBacktrack -> ()
   | BacktrackToNextActiveMark -> assert false
 
-let old_rewind count cmd_stk =
+let old_rewind count =
+  let cmd_stk = com_stk in
   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
@@ -583,7 +572,7 @@ let old_rewind count cmd_stk =
           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);
+          if count <= 0 then ignore (eval_expr cmd_stk coq.loc_ast);
         end
   in
   do_rewind count 0 0 NoBacktrack 0 (undo_info ());
diff --git a/ide/coq.mli b/ide/coq.mli
index e863288cd1..f571c176ab 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -31,30 +31,14 @@ sig
 end
 
 
-type reset_status
-
-type undo_info
-
-val undo_info : unit -> undo_info
-
-type reset_info = {
- status : reset_status;
- proofs : undo_info;
- loc_ast : Util.loc * Vernacexpr.vernac_expr;
-}
-
-val compute_reset_info : Util.loc * Vernacexpr.vernac_expr -> reset_info
 val reset_initial : unit -> unit
 
 val init : unit -> string list
-val interp : bool -> string -> reset_info
-val interp_last : Util.loc * Vernacexpr.vernac_expr -> unit
+val interp : bool -> string -> int
 val interp_and_replace : string ->
-      reset_info * string
-
-val push_phrase : ('a * reset_info) Stack.t -> reset_info -> 'a -> unit
+  int * string
 
-val old_rewind : int -> ('a * reset_info) Stack.t -> unit
+val old_rewind : int -> 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 fafc28b067..4153a7c018 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -34,7 +34,7 @@ object('self)
   val message_view : GText.view
   val proof_buffer : GText.buffer
   val proof_view : GText.view
-  val cmd_stack : (ide_info * Coq.reset_info) Stack.t
+  val cmd_stack : ide_info Stack.t
   val mutable is_active : bool
   val mutable read_only : bool
   val mutable filename : string option
@@ -85,7 +85,7 @@ object('self)
   method send_to_coq :
     bool -> bool -> string ->
     bool -> bool -> bool ->
-    (bool*reset_info) option
+    (bool*int) option
   method set_message : string -> unit
   method show_pm_goal : unit
   method show_goals : unit
@@ -1050,10 +1050,7 @@ object(self)
            end;
          let ide_payload = { start = `MARK (b#create_mark start);
                              stop = `MARK (b#create_mark stop); } in
-         push_phrase
-           cmd_stack
-           reset_info
-           ide_payload;
+         Stack.push ide_payload cmd_stack;
          if display_goals then self#show_goals;
          remove_tag (start,stop) in
     begin
@@ -1081,8 +1078,8 @@ object(self)
                input_buffer#place_cursor stop;
              let ide_payload = { start = `MARK (input_buffer#create_mark start);
                                  stop = `MARK (input_buffer#create_mark stop); } in
-               push_phrase cmd_stack reset_info ide_payload;
-               self#show_goals;
+             Stack.push ide_payload cmd_stack;
+             self#show_goals;
       (*Auto insert save on success...
        try (match Coq.get_current_goals () with
        | [] ->
@@ -1155,7 +1152,7 @@ object(self)
   method reset_initial =
     sync (fun _ ->
             Stack.iter
-              (function (inf,_) ->
+              (function inf ->
                  let start = input_buffer#get_iter_at_mark inf.start in
                  let stop = input_buffer#get_iter_at_mark inf.stop in
                    input_buffer#move_mark ~where:start (`NAME "start_of_input");
@@ -1173,22 +1170,21 @@ object(self)
   method backtrack_to_no_lock i =
     prerr_endline "Backtracking_to iter starts now.";
     (* pop Coq commands until we reach iterator [i] *)
-    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 Stack.is_empty cmd_stack then n else
+        let ide_ri = Stack.pop cmd_stack in
         if i#compare (input_buffer#get_iter_at_mark ide_ri.stop) < 0 then
           n_step (succ n)
         else
-          n
+          (Stack.push ide_ri cmd_stack; n)
     in
     begin
       try
-        old_rewind (n_step 0) cmd_stack;
+        old_rewind (n_step 0);
         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
+                  else input_buffer#get_iter_at_mark (Stack.top cmd_stack).stop in
                 prerr_endline "Removing (long) processed tag...";
                 input_buffer#remove_tag
                   Tags.Script.processed
@@ -1226,7 +1222,7 @@ object(self)
     if Mutex.try_lock coq_may_stop then
       (push_info "Undoing last step...";
        (try
-          let (ide_ri,_) = Stack.top cmd_stack in
+          let ide_ri = Stack.pop cmd_stack in
           let start = input_buffer#get_iter_at_mark ide_ri.start in
           let update_input () =
             prerr_endline "Removing processed tag...";
@@ -1247,7 +1243,7 @@ object(self)
             self#show_goals;
             self#clear_message
           in
-          old_rewind 1 cmd_stack;
+          old_rewind 1;
           sync update_input ()
         with
           | Stack.Empty -> (* flash_info "Nothing to Undo"*)()