Coqide: new backtracking code, based on the Backtrack command

 This approach, inspired by ProofGeneral, is *much* simplier than earlier,
 and should be more robust (I hope! feedback of testers is welcome).

 Coqide still continues to send orders like "Rewind 5" for undoing 5 phrases.
 A stack on the coqtop side (in Ide_slave) convert this phrase count to
 labels in the sense of Backtrack, and to abort + depth informations
 concerning proofs.

 We avoid re-entering finished proofs during Rewind by some extra backtracking
 until before these proofs. The amount of extra backtracking is then answered
 by coqtop to coqide. Now:
  - for go_to_insert (the "goto" button), unlike PG, coqide replays
    the extra backtracked zone.
  - for undo_last_step (the "back" button), coqide now leaves the extra
    backtracked zone undone, just like PG. This happens typically when
    undoing a Qed, and this should be the only visible semantical change
    of this patch.

 Two points to check with Pierre C:
  - such a coqtop-side stack mapping labels to opened proofs might be
    interesting to PG, instead of passing lots of info via the prompt and
    computing stuff in emacs.
  - Unlike PG, we allow re-entering inside a module / section, while
    PG retracts to the start of it. Coqide seems to work fine this way, to
    check.

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

9 files changed, 192 insertions, 196 deletions

diff --git a/ide/coq.mli b/ide/coq.mli
index 685bfcac3..047a26587 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -47,7 +47,7 @@ val interrupter : (int -> unit) ref
 
 val interp :
   coqtop -> ?raw:bool -> ?verbose:bool -> string -> string Ide_intf.value
-val rewind : coqtop -> int -> unit Ide_intf.value
+val rewind : coqtop -> int -> int Ide_intf.value
 val status : coqtop -> string Ide_intf.value
 val goals : coqtop -> Ide_intf.goals Ide_intf.value
 val inloadpath : coqtop -> string -> bool Ide_intf.value
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 7a714b1d0..e6968c51c 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1096,6 +1096,41 @@ object(self)
       Mutex.unlock resetting
     end
 
+  (* Internal method for dialoging with coqtop about a backtrack.
+     The ide's cmd_stack has already been cleared up to the desired point.
+     The [finish] function is used to handle minor differences between
+     [go_to_insert] and [undo_last_step] *)
+
+  method private do_backtrack finish n =
+    (* pop n more commands if coqtop has said so (e.g. for undoing a proof) *)
+    let rec n_pop n =
+      if n = 0 then ()
+      else
+	let phrase = Stack.pop cmd_stack in
+	let stop = input_buffer#get_iter_at_mark phrase.stop in
+        if stop#backward_char#has_tag Tags.Script.comment
+	  then n_pop n
+	  else n_pop (pred n)
+    in
+    match Coq.rewind !mycoqtop n with
+      | Ide_intf.Good n ->
+	n_pop n;
+        sync (fun _ ->
+          let start =
+            if Stack.is_empty cmd_stack then input_buffer#start_iter
+            else input_buffer#get_iter_at_mark (Stack.top cmd_stack).stop in
+	  let stop = self#get_start_of_input in
+          input_buffer#remove_tag Tags.Script.processed ~start ~stop;
+          input_buffer#remove_tag Tags.Script.unjustified ~start ~stop;
+          input_buffer#move_mark ~where:start (`NAME "start_of_input");
+          self#show_goals;
+          self#clear_message;
+          finish start) ()
+      | Ide_intf.Fail (l,str) ->
+        sync self#set_message
+          ("Error while backtracking :\n" ^ str ^ "\n" ^
+	   "CoqIDE and coqtop may be out of sync, you may want to use Restart.")
+
   (* backtrack Coq to the phrase preceding iterator [i] *)
   method backtrack_to_no_lock i =
     prerr_endline "Backtracking_to iter starts now.";
@@ -1103,42 +1138,21 @@ object(self)
     (* pop Coq commands until we reach iterator [i] *)
     let rec n_step n =
       if Stack.is_empty cmd_stack then n else
-        let ide_ri = Stack.pop cmd_stack in
-	let stop = input_buffer#get_iter_at_mark ide_ri.stop in
-        if i#compare stop < 0 then
+        let phrase = Stack.top cmd_stack in
+	let stop = input_buffer#get_iter_at_mark phrase.stop in
+        if i#compare stop >= 0 then n
+	else begin
+	  ignore (Stack.pop cmd_stack);
           if stop#backward_char#has_tag Tags.Script.comment
 	  then n_step n
 	  else n_step (succ n)
-        else
-          (Stack.push ide_ri cmd_stack; n)
+	end
     in
     begin
       try
-        match Coq.rewind !mycoqtop (n_step 0) with
-          | Ide_intf.Fail (l,str) ->
-            sync self#set_message
-              ("Error while backtracking :\n" ^ str ^ "\n" ^
-	       "CoqIDE and coqtop may be out of sync," ^
-	       "you may want to use Restart.")
-          | Ide_intf.Good () ->
-            sync (fun _ ->
-              let start =
-                if Stack.is_empty cmd_stack then input_buffer#start_iter
-                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
-                ~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;
-              self#clear_message)
-              ();
+	self#do_backtrack (fun _ -> ()) (n_step 0);
+	(* We may have backtracked too much: let's replay *)
+	self#process_until_iter_or_error i
       with _ ->
         push_info
 	  ("WARNING: undo failed badly.\n" ^
@@ -1164,24 +1178,17 @@ object(self)
     if Mutex.try_lock coq_may_stop then
       (push_info "Undoing last step...";
        (try
-          let ide_ri = Stack.pop cmd_stack in
-          let start = input_buffer#get_iter_at_mark ide_ri.start in
-	  let stop = input_buffer#get_iter_at_mark ide_ri.stop in
-          let update_input () =
-            prerr_endline "Removing processed tag...";
-            input_buffer#remove_tag Tags.Script.processed ~start ~stop;
-            input_buffer#remove_tag Tags.Script.unjustified ~start ~stop;
-            prerr_endline "Moving start_of_input";
-            input_buffer#move_mark ~where:start (`NAME "start_of_input");
-            input_buffer#place_cursor ~where:start;
-            self#recenter_insert;
-            self#show_goals;
-            self#clear_message
-          in
-            if not (stop#backward_char#has_tag Tags.Script.comment) then ignore (Coq.rewind !mycoqtop 1);
-            sync update_input ()
-        with
-          | Stack.Empty -> (* flash_info "Nothing to Undo"*)()
+          let phrase = Stack.pop cmd_stack in
+	  let stop = input_buffer#get_iter_at_mark phrase.stop in
+	  let count =
+	    if stop#backward_char#has_tag Tags.Script.comment then 0 else 1
+	  in
+	  let finish where =
+	    input_buffer#place_cursor ~where;
+	    self#recenter_insert;
+	  in
+	  self#do_backtrack finish count
+        with Stack.Empty -> ()
        );
        pop_info ();
        Mutex.unlock coq_may_stop)
diff --git a/library/lib.ml b/library/lib.ml
index f6b25e201..cfaea3b66 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -553,13 +553,6 @@ let recache_context ctx =
 
 let is_frozen_state = function (_,FrozenState _) -> true | _ -> false
 
-let has_top_frozen_state () =
-  let rec aux = function
-  | (sp, FrozenState _)::_ -> Some sp
-  | (sp, Leaf o)::t when object_tag o = "DOT" -> aux t
-  | _ -> None
-  in aux !lib_stk
-
 let set_lib_stk new_lib_stk =
   lib_stk := new_lib_stk;
   recalc_path_prefix ();
@@ -579,14 +572,6 @@ let reset_to_gen test =
 
 let reset_to sp = reset_to_gen (fun x -> fst x = sp)
 
-let reset_to_state sp =
-  let (_,eq,before) = split_lib sp in
-  (* if eq a frozen state, we'll reset to it *)
-  match eq with
-  | [_,FrozenState f] -> lib_stk := eq@before; recalc_path_prefix (); unfreeze_summaries f
-  | _ -> error "Not a frozen state"
-
-
 (* LEM: TODO
  * We will need to muck with frozen states in after, too!
  * Not only FrozenState, but also those embedded in Opened(Section|Module)
@@ -677,7 +662,9 @@ let rec back_stk n stk =
     | _::tail -> back_stk n tail
     | [] -> error "Reached begin of command history"
 
-let back n = reset_to (back_stk n !lib_stk)
+let back n =
+  reset_to (back_stk n !lib_stk);
+  set_command_label (current_command_label () - n - 1)
 
 (* State and initialization. *)
 
diff --git a/library/lib.mli b/library/lib.mli
index 419f91317..0d6eb34b8 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -157,9 +157,6 @@ val reset_to : Libnames.object_name -> unit
 val reset_name : Names.identifier Util.located -> unit
 val remove_name : Names.identifier Util.located -> unit
 val reset_mod : Names.identifier Util.located -> unit
-val reset_to_state : Libnames.object_name -> unit
-
-val has_top_frozen_state : unit -> Libnames.object_name option
 
 (** [back n] resets to the place corresponding to the {% $ %}n{% $ %}-th call of
    [mark_end_of_command] (counting backwards) *)
diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml
index 5374b06df..8bd1df7a4 100644
--- a/toplevel/ide_intf.ml
+++ b/toplevel/ide_intf.ml
@@ -28,7 +28,7 @@ type 'a call =
   | MkCases of string
 
 let interp (r,b,s) : string call = Interp (r,b,s)
-let rewind i : unit call = Rewind i
+let rewind i : int call = Rewind i
 let goals : goals call = Goals
 let status : string call = Status
 let inloadpath s : bool call = InLoadPath s
@@ -44,7 +44,7 @@ type 'a value =
 
 type handler = {
   interp : raw * verbose * string -> string;
-  rewind : int -> unit;
+  rewind : int -> int;
   goals : unit -> goals;
   status : unit -> string;
   inloadpath : string -> bool;
@@ -90,7 +90,7 @@ let pr_bool b = if b then "true" else "false"
 let pr_full_value call value =
   match call with
     | Interp _ -> pr_value_gen pr_string (Obj.magic value)
-    | Rewind i -> pr_value value
+    | Rewind i -> pr_value_gen string_of_int (Obj.magic value)
     | Goals -> pr_value value (* TODO *)
     | Status -> pr_value_gen pr_string (Obj.magic value)
     | InLoadPath s -> pr_value_gen pr_bool (Obj.magic value)
diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli
index 211b34e13..b13f10afa 100644
--- a/toplevel/ide_intf.mli
+++ b/toplevel/ide_intf.mli
@@ -30,8 +30,13 @@ type verbose = bool
       to be fetch by a separated [current_goals]). *)
 val interp : raw * verbose * string -> string call
 
-(** Backtracking by a certain number of phrases. *)
-val rewind : int -> unit call
+(** Backtracking by at least a certain number of phrases.
+    No finished proofs will be re-opened. Instead,
+    we continue backtracking until before these proofs,
+    and answer the amount of extra backtracking performed.
+    Backtracking by more than the number of phrases already
+    interpreted successfully (and not yet undone) will fail. *)
+val rewind : int -> int call
 
 (** Fetching the list of current goals *)
 val goals : goals call
@@ -60,7 +65,7 @@ type 'a value =
 
 type handler = {
   interp : raw * verbose * string -> string;
-  rewind : int -> unit;
+  rewind : int -> int;
   goals : unit -> goals;
   status : unit -> string;
   inloadpath : string -> bool;
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 616cd5b09..a9bab9465 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -14,6 +14,18 @@ open Pp
 open Printer
 open Namegen
 
+(** Ide_slave : an implementation of [Ide_intf], i.e. mainly an interp
+    function and a rewind function. This specialized loop is triggered
+    when the -ideslave option is passed to Coqtop. Currently CoqIDE is
+    the only one using this mode, but we try here to be as generic as
+    possible, so this may change in the future... *)
+
+
+(** Comment the next line for displaying some more debug messages *)
+
+let prerr_endline _ = ()
+
+
 (** Signal handling: we postpone ^C during input and output phases,
     but make it directly raise a Sys.Break during evaluation of the request. *)
 
@@ -23,7 +35,8 @@ let init_signal_handler () =
   let f _ = if !catch_break then raise Sys.Break else Util.interrupt := true in
   Sys.set_signal Sys.sigint (Sys.Signal_handle f)
 
-let prerr_endline _ = ()
+
+(** Redirection of standard output to a printable buffer *)
 
 let orig_stdout = ref stdout
 
@@ -46,6 +59,9 @@ let init_stdout,read_stdout =
              let r = Buffer.contents out_buff in
              Buffer.clear out_buff; r)
 
+
+(** Categories of commands *)
+
 let coqide_known_option table = List.mem table [
   ["Printing";"Implicit"];
   ["Printing";"Coercions"];
@@ -125,7 +141,11 @@ let rec attribute_of_vernac_command = function
   | VernacRemoveLoadPath _ -> []
   | VernacAddMLPath _ -> []
   | VernacDeclareMLModule _ -> []
-  | VernacChdir _ -> [OtherStatePreservingCommand]
+  | VernacChdir o ->
+    (* TODO: [Chdir d] is currently not undo-able (not stored in coq state).
+       But if we register [Chdir] in the state, loading [initial.coq] will
+       wrongly cd to the compile-time directory at each coqtop launch. *)
+    if o = None then [QueryCommand] else []
 
   (* State management *)
   | VernacWriteState _ -> []
@@ -225,43 +245,28 @@ let is_vernac_tactic_command com =
 let is_vernac_proof_ending_command com =
   List.mem ProofEndingCommand (attribute_of_vernac_command com)
 
-type reset_status =
-  | NoReset
-  | ResetToNextMark
-  | ResetAtMark of Libnames.object_name
 
-type reset_info = {
-  status : reset_status;
-  proofs : identifier list;
-  cur_prf : (identifier * int) option;
-  loc_ast : Util.loc * Vernacexpr.vernac_expr;
-}
+(** Command history stack
+
+    We maintain a stack of the past states of the system. Each
+    successfully interpreted command adds a [reset_info] element
+    to this stack, storing what were the (label / open proofs /
+    current proof depth) just _before_ the interpretation of this
+    command. A label is just an integer (cf. BackTo and Bactrack
+    vernac commands).
+*)
+
+type reset_info = { label : int; proofs : identifier list; depth : int }
 
 let com_stk = Stack.create ()
 
-let reinit () =
-  Vernacentries.abort_refine Lib.reset_initial ();
-  Stack.clear com_stk
-
-let compute_reset_info loc_ast =
-  let status,cur_prf = match snd loc_ast with
-    | com when is_vernac_tactic_command com ->
-        NoReset,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 -> ResetToNextMark,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
-           | None -> prerr_endline "No top state"; (NoReset,None))
-  in
-  { status = status;
+let compute_reset_info () =
+  { label = Lib.current_command_label ();
     proofs = Pfedit.get_all_proof_names ();
-    cur_prf = cur_prf;
-    loc_ast = loc_ast;
-  }
+    depth = max 0 (Pfedit.current_proof_depth ()) }
+
+
+(** Interpretation (cf. [Ide_intf.interp]) *)
 
 (** Check whether a command is forbidden by CoqIDE *)
 
@@ -281,82 +286,71 @@ let coqide_cmd_checks (loc,ast) =
 let raw_eval_expr = Vernac.eval_expr
 
 let eval_expr loc_ast =
-  let rewind_info = compute_reset_info loc_ast in
+  let rewind_info = compute_reset_info () in
   raw_eval_expr loc_ast;
   Stack.push rewind_info com_stk
 
 let interp (raw,verbosely,s) =
-  prerr_endline "Starting interp...";
-  prerr_endline s;
+  if not raw then (prerr_endline "Starting interp..."; prerr_endline s);
   let pa = Pcoq.Gram.parsable (Stream.of_string s) in
   let loc_ast = Vernac.parse_sentence (pa,None) in
   if not raw then coqide_cmd_checks loc_ast;
-  (* Verbose if command is not a tactic and IDE said to be verbose
-     (i.e. we're in small step forward mode) *)
+  (* We run tactics silently, since we will query the goal state later.
+     Otherwise, we honor the IDE verbosity flag. *)
   Flags.make_silent
     (is_vernac_goal_printing_command (snd loc_ast) || not verbosely);
   if raw then raw_eval_expr loc_ast else eval_expr loc_ast;
   Flags.make_silent true;
-  prerr_endline ("...Done with interp of : "^s);
+  if not raw then prerr_endline ("...Done with interp of : "^s);
   read_stdout ()
 
+
+(** Backtracking (cf. [Ide_intf.rewind]).
+    We now rely on the [Backtrack] command just as ProofGeneral. *)
+
 let rewind count =
-  let undo_ops = Hashtbl.create 31 in
-  let current_proofs = Pfedit.get_all_proof_names () in
-  let rec do_rewind count reset_op prev_proofs curprf =
-    if (count <= 0) && (reset_op <> ResetToNextMark) &&
-       (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
-        Hashtbl.iter
-          (fun id depth ->
-             if List.mem id prev_proofs then begin
-               Pfedit.suspend_proof ();
-               Pfedit.resume_proof (Util.dummy_loc,id);
-               Pfedit.undo_todepth depth
-             end)
-          undo_ops;
-        prerr_endline "OK for undos";
-        Option.iter (fun id -> if List.mem id prev_proofs then
-                       Pfedit.suspend_proof ();
-                       Pfedit.resume_proof (Util.dummy_loc,id)) curprf;
-        prerr_endline "OK for focusing";
-        List.iter
-          (fun id -> Pfedit.delete_proof (Util.dummy_loc,id))
-          (Util.list_subtract current_proofs prev_proofs);
-        prerr_endline "OK for aborts";
-        (match reset_op with
-           | NoReset -> prerr_endline "No Reset"
-           | ResetAtMark m -> (prerr_endline ("Reset at "^(Libnames.string_of_path (fst m))); Lib.reset_to_state m)
-           | ResetToNextMark -> assert false);
-        prerr_endline "OK for reset"
-          end
-        else
-          begin
-            prerr_endline "pop";
-            let coq = Stack.pop com_stk in
-            let curprf =
-              Option.map
-                (fun (curprf,depth) ->
-                   (if Hashtbl.mem undo_ops curprf then Hashtbl.replace else Hashtbl.add)
-                     undo_ops curprf depth;
-                   curprf)
-                coq.cur_prf in
-            do_rewind (pred count)
-              (if coq.status <> NoReset then coq.status else reset_op) coq.proofs curprf;
-            if count <= 0 then begin
-              (* we had to backtrack further to find a suitable
-               * anchor point, replaying *)
-              prerr_endline "push";
-              ignore (eval_expr coq.loc_ast);
-            end
-          end
-  in
-  do_rewind count NoReset current_proofs None
+  if count = 0 then 0
+  else
+    let current_proofs = Pfedit.get_all_proof_names ()
+    in
+    (* 1) First, let's pop the history stack exactly [count] times.
+       NB: Normally, the IDE will not rewind by more than the numbers
+       of already interpreted commands, hence no risk of [Stack.Empty].
+    *)
+    let initial_target =
+      for i = 1 to count - 1 do ignore (Stack.pop com_stk) done;
+      Stack.pop com_stk
+    in
+    (* 2) Backtrack by enough additional steps to avoid re-opening proofs.
+       Typically, when a Qed has been crossed, we backtrack to the proof start.
+       NB: We cannot reach the empty stack, since the oldest [reset_info]
+       in the history cannot have opened proofs.
+    *)
+    let already_opened p = List.mem p current_proofs in
+    let rec extra_back n target =
+      if List.for_all already_opened target.proofs then n,target
+      else extra_back (n+1) (Stack.pop com_stk)
+    in
+    let extra_count, target = extra_back 0 initial_target
+    in
+    (* 3) Now that [target.proofs] is a subset of the opened proofs before
+       the rewind, we simply abort the extra proofs (if any).
+       NB: It is critical here that proofs are nested in a regular way
+       (i.e. no Resume or Suspend, as enforced above). This way, we can simply
+       count the extra proofs to abort instead of taking care of their names.
+    *)
+    let naborts = List.length current_proofs - List.length target.proofs
+    in
+    (* 4) We are now ready to call [Backtrack] *)
+    prerr_endline ("Rewind to state "^string_of_int target.label^
+		   ", proof depth "^string_of_int target.depth^
+		   ", num of aborts "^string_of_int naborts);
+    Vernacentries.vernac_backtrack target.label target.depth naborts;
+    Lib.mark_end_of_command (); (* We've short-circuited Vernac.eval_expr *)
+    extra_count
 
-let inloadpath dir =
-  Library.is_in_load_paths (System.physical_path_of_string dir)
+
+(** Goal display *)
 
 let string_of_ppcmds c =
   Pp.msg_with Format.str_formatter c;
@@ -452,6 +446,12 @@ let goals () =
   with Proof_global.NoCurrentProof ->
     Ide_intf.Message "" (* quick hack to have a clean message screen *)
 
+
+(** Other API calls *)
+
+let inloadpath dir =
+  Library.is_in_load_paths (System.physical_path_of_string dir)
+
 let status () =
   (** We remove the initial part of the current [dir_path]
       (usually Top in an interactive session, cf "coqtop -top"),
@@ -469,29 +469,21 @@ let status () =
   in
   "Ready"^path^proof
 
-let explain_exn e =
-  let toploc,exc =
-    match e with
-      | Loc.Exc_located (loc, inner) ->
-	let l = if loc = dummy_loc then None else Some (Util.unloc loc) in
-	l,inner
-      | Error_in_file (s, _, inner) -> None,inner
-      | _ -> None,e
-  in
-  toploc,(Errors.print exc)
+
+(** Grouping all call handlers together + error handling *)
 
 let eval_call c =
-  (* If the messages of last command are still there, we remove them *)
-  ignore (read_stdout ());
   let rec handle_exn e =
     catch_break := false;
+    let pr_exn e = string_of_ppcmds (Errors.print e) in
     match e with
-      | Vernac.DuringCommandInterp (loc,inner) -> handle_exn inner
       | Vernacexpr.Drop -> None, "Drop is not allowed by coqide!"
       | Vernacexpr.Quit -> None, "Quit is not allowed by coqide!"
-      | e ->
-	let (l,pp) = explain_exn e in
-	l, string_of_ppcmds pp
+      | Vernac.DuringCommandInterp (_,inner) -> handle_exn inner
+      | Error_in_file (_,_,inner) -> None, pr_exn inner
+      | Loc.Exc_located (loc, inner) when loc = dummy_loc -> None, pr_exn inner
+      | Loc.Exc_located (loc, inner) -> Some (Util.unloc loc), pr_exn inner
+      | e -> None, pr_exn e
   in
   let interruptible f x =
     catch_break := true;
@@ -508,23 +500,29 @@ let eval_call c =
     Ide_intf.inloadpath = interruptible inloadpath;
     Ide_intf.mkcases = interruptible Vernacentries.make_cases }
   in
+  (* If the messages of last command are still there, we remove them *)
+  ignore (read_stdout ());
   Ide_intf.abstract_eval_call handler handle_exn c
 
-let pr_debug s =
-  if !Flags.debug then begin
-    Printf.eprintf "[pid %d] %s\n" (Unix.getpid ()) s; flush stderr
-  end
 
-(** Exceptions during eval_call should be converted into Ide_intf.Fail
-    messages by explain_exn above. Otherwise, we die badly, after having
+(** The main loop *)
+
+(** Exceptions during eval_call should be converted into [Ide_intf.Fail]
+    messages by [handle_exn] above. Otherwise, we die badly, after having
     tried to send a last message to the ide: trying to recover from errors
     with the current protocol would most probably bring desynchronisation
     between coqtop and ide. With marshalling, reading an answer to
     a different request could hang the ide... *)
 
+let pr_debug s =
+  if !Flags.debug then Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s
+
 let loop () =
   init_signal_handler ();
   catch_break := false;
+  (* ensure we have a command separator object (DOT) so that the first
+     command can be reseted. *)
+  Lib.mark_end_of_command();
   try
     while true do
       let q = (Marshal.from_channel: in_channel -> 'a Ide_intf.call) stdin in
diff --git a/toplevel/ide_slave.mli b/toplevel/ide_slave.mli
index 272616ae3..13dff280a 100644
--- a/toplevel/ide_slave.mli
+++ b/toplevel/ide_slave.mli
@@ -6,12 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** Specialize loop of Coqtop for interaction with CoqIde *)
-
-val reinit : unit -> unit
+(** [Ide_slave] : an implementation of [Ide_intf], i.e. mainly an interp
+    function and a rewind function. This specialized loop is triggered
+    when the -ideslave option is passed to Coqtop. Currently CoqIDE is
+    the only one using this mode, but we try here to be as generic as
+    possible, so this may change in the future... *)
 
 val init_stdout : unit -> unit
 
-val eval_call : 'a Ide_intf.call -> 'a Ide_intf.value
-
 val loop : unit -> unit
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 02cfa8534..814676575 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -53,6 +53,8 @@ val interp : Vernacexpr.vernac_expr -> unit
 
 val vernac_reset_name : identifier Util.located -> unit
 
+val vernac_backtrack : int -> int -> int -> unit
+
 (* Print subgoals when the verbose flag is on. Meant to be used inside
     vernac commands from plugins. *)
 val print_subgoals : unit -> unit