A unified backtrack mechanism, with a basic "Show Script" as side-effect

 Migrate the backtracking code from ide_slave.ml into a new backtrack.ml.
 In particular the history stack of commands that used to be there is now
 non-coqide-specific.

 ** Adapted commands **

 - "Show Script": a basic functional version is restored (and the printing
 of scripts at Qed in coqtop). No indentation, one Coq command per line,
 based on the vernac_expr asts recorded in the history stack, printed via
 Ppvernac.

 - "Back n" : now mimics the backtrack of coqide: it goes n steps back
 (both commands and proofs), and maybe more if needed to avoid re-entering
 a proof (it outputs a warning in this case).

 - "BackTo n" : still try to go back to state n, but it also handles the
 proof state, and it may end on some state n' <= n if needed to avoid
 re-entering a proof. Ideally, it could someday be used by ProofGeneral
 instead of the complex Backtrack command.

 ** Compatible commands **

 - "Backtrack" is left intact from compatibility with current ProofGeneral.
 We simply re-synchronize the command history stack after each Backtrack.

 - "Undo" is kept as a standard command, not a backtracking one, a bit like
 "Focus". Same for "Restart" and "Abort". All of these are now accepted
 in coqide (Undo simply triggers a warning).

 - Undocumented command "Undo To n" (counting from start of proof instead of
 from end) also keep its semantics, it is simply made compatible with
 the new stack mechanism.

 ** New restrictions **

 We now forbid backtracking commands (Reset* / Back*) inside files
 when Load'ing or compiling, or inside VernacList/VernacTime/VernacFail.
 Too much work dealing with these situation that nobody uses.

 ** Internal details **

 Internally, the command stack differs a bit from what was in Ide_slave
 earlier (which was inspired by lisp code in ProofGeneral). We now tag
 commands that are unreachable by a backtrack, due to some proof being
 finished, aborted, restarted, or partly Undo'ed. This induce a bit of
 bookkeeping during Qed/Abort/Restart/Undo, but then the backtracking code
 is straightforward: we simply search backward the first reachable state
 starting from the desired place. We don't depend anymore on the proof
 names (apart in the last proof block), It's more robust this way
 (think of re-entering a M.foo from an outside proof foo).

 Many internal clarifications in Lib, Vernac, etc. For instance
 "Reset Initial" is now just a BackTo 1, while "Reset foo" now calls
 (Lib.label_before_name "foo"), and performs a BackTo to the corresponding
 label.

 Concerning Coqide, we directly suppress the regular printing of goals
 via a flag in Vernacentries. This avoid relying on a classification
 of commands in Ide_slave as earlier.

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

18 files changed, 780 insertions, 435 deletions

diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll
index f0f1afb74..314e15e3e 100644
--- a/ide/coq_lex.mll
+++ b/ide/coq_lex.mll
@@ -24,7 +24,7 @@
     let one_word_commands =
       [ "Add" ; "Check"; "Eval"; "Extraction" ;
 	"Load" ; "Undo"; "Goal";
-	"Proof" ; "Print";"Save" ;
+	"Proof" ; "Print";"Save" ; "Restart";
 	"End" ; "Section"; "Chapter"; "Transparent"; "Opaque"; "Comments" ]
     in
     let one_word_declarations =
diff --git a/library/lib.ml b/library/lib.ml
index 54087ce1c..40a427e49 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -573,44 +573,16 @@ let reset_to_gen test =
 
 let reset_to sp = reset_to_gen (fun x -> fst x = sp)
 
-let reset_name (loc,id) =
-  let (sp,_) =
-    try
-      find_entry_p (fun (sp,_) -> let (_,spi) = repr_path (fst sp) in id = spi)
-    with Not_found ->
-      user_err_loc (loc,"reset_name",pr_id id ++ str ": no such entry")
-  in
-  reset_to sp
-
-let is_mod_node = function
-  | OpenedModule _ | OpenedSection _
-  | ClosedModule _ | ClosedSection _  -> true
-  | Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE"
-	|| t = "MODULE ALIAS"
-  | _ -> false
-
-(* Reset on a module or section name in order to bypass constants with
-   the same name *)
-
-let reset_mod (loc,id) =
-  let (_,before) =
-    try
-      find_split_p (fun (sp,node) ->
-                    let (_,spi) = repr_path (fst sp) in id = spi
-                    && is_mod_node node)
-    with Not_found ->
-      user_err_loc (loc,"reset_mod",pr_id id ++ str ": no such entry")
-  in
-  set_lib_stk before
+let first_command_label = 1
 
-let mark_end_of_command, current_command_label, set_command_label =
-  let n = ref 0 in
+let mark_end_of_command, current_command_label, reset_command_label =
+  let n = ref (first_command_label-1) in
   (fun () ->
     match !lib_stk with
         (_,Leaf o)::_ when object_tag o = "DOT" -> ()
       | _ -> incr n;add_anonymous_leaf (inLabel !n)),
   (fun () -> !n),
-  (fun x -> n:=x)
+  (fun x -> n:=x;add_anonymous_leaf (inLabel x))
 
 let is_label_n n x =
   match x with
@@ -623,21 +595,21 @@ let is_label_n n x =
 let reset_label n =
   if n >= current_command_label () then
     error "Cannot backtrack to the current label or a future one";
-  let res = reset_to_gen (is_label_n n) in
+  reset_to_gen (is_label_n n);
   (* forget state numbers after n only if reset succeeded *)
-  set_command_label (n-1);
-  res
+  reset_command_label n
 
-let rec back_stk n stk =
-  match stk with
-      (sp,Leaf o)::tail when object_tag o = "DOT" ->
-        if n=0 then sp else back_stk (n-1) tail
-    | _::tail -> back_stk n tail
-    | [] -> error "Reached begin of command history"
+(** Search the last label registered before defining [id] *)
 
-let back n =
-  reset_to (back_stk n !lib_stk);
-  set_command_label (current_command_label () - n - 1)
+let label_before_name (loc,id) =
+  let found = ref false in
+  let search = function
+    | (_,Leaf o) when !found && object_tag o = "DOT" -> true
+    | (sp,_) -> (if id = snd (repr_path (fst sp)) then found := true); false
+  in
+  match find_entry_p search with
+    | (_,Leaf o) -> outLabel o
+    | _ -> raise Not_found
 
 (* State and initialization. *)
 
@@ -657,29 +629,6 @@ let init () =
   path_prefix := initial_prefix;
   init_summaries()
 
-(* Initial state. *)
-
-let initial_state = ref None
-
-let declare_initial_state () =
-  let name = add_anonymous_entry (FrozenState (freeze_summaries())) in
-  initial_state := Some name
-
-let reset_initial () =
-  match !initial_state with
-    | None ->
-        error "Resetting to the initial state is possible only interactively"
-    | Some sp ->
-  	begin match split_lib sp with
-	  | (_,[_,FrozenState fs as hd],before) ->
-	      lib_stk := hd::before;
-	      recalc_path_prefix ();
-			set_command_label 0;
-	      unfreeze_summaries fs
-	  | _ -> assert false
-	end
-
-
 (* Misc *)
 
 let mp_of_global ref =
diff --git a/library/lib.mli b/library/lib.mli
index df931f060..781ecfe32 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -62,17 +62,6 @@ val add_leaves : Names.identifier -> Libobject.obj list -> Libnames.object_name
 
 val add_frozen_state : unit -> unit
 
-(** Adds a "dummy" entry in lib_stk with a unique new label number. *)
-val mark_end_of_command : unit -> unit
-
-(** Returns the current label number *)
-val current_command_label : unit -> int
-
-(** [reset_label n] resets [lib_stk] to the label n registered by
-   [mark_end_of_command()]. It forgets the label and anything
-   registered after it. The label should be strictly in the past. *)
-val reset_label : int -> unit
-
 (** {6 ... } *)
 (** The function [contents_after] returns the current library segment,
   starting from a given section path. If not given, the entire segment
@@ -151,15 +140,28 @@ val remove_section_part : Libnames.global_reference -> Names.dir_path
 val open_section : Names.identifier -> unit
 val close_section : unit -> unit
 
-(** {6 Backtracking (undo). } *)
+(** {6 Backtracking } *)
 
-val reset_to : Libnames.object_name -> unit
-val reset_name : Names.identifier Pp.located -> unit
-val reset_mod : Names.identifier Pp.located -> unit
+(** NB: The next commands are low-level ones, do not use them directly
+    otherwise the command history stack in [Backtrack] will be out-of-sync.
+    Also note that [reset_initial] is now [reset_label first_command_label] *)
 
-(** [back n] resets to the place corresponding to the {% $ %}n{% $ %}-th call of
-   [mark_end_of_command] (counting backwards) *)
-val back : int -> unit
+(** Adds a "dummy" entry in lib_stk with a unique new label number. *)
+val mark_end_of_command : unit -> unit
+
+(** Returns the current label number *)
+val current_command_label : unit -> int
+
+(** The first label number *)
+val first_command_label : int
+
+(** [reset_label n] resets [lib_stk] to the label n registered by
+   [mark_end_of_command()]. It forgets anything registered after
+   this label. The label should be strictly in the past. *)
+val reset_label : int -> unit
+
+(** search the label registered immediately before adding some definition *)
+val label_before_name : Names.identifier Pp.located -> int
 
 (** {6 We can get and set the state of the operations (used in [States]). } *)
 
@@ -170,10 +172,6 @@ val unfreeze : frozen -> unit
 
 val init : unit -> unit
 
-val declare_initial_state : unit -> unit
-val reset_initial : unit -> unit
-
-
 (** XML output hooks *)
 val set_xml_open_section : (Names.identifier -> unit) -> unit
 val set_xml_close_section : (Names.identifier -> unit) -> unit
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index a9b162819..e4695792b 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1143,7 +1143,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 
       mk_correct_id f_id
     in
-     ignore(try Vernacentries.vernac_reset_name (Pp.dummy_loc,first_lemma_id) with _ -> ());
+    (try Backtrack.reset_name (Pp.dummy_loc,first_lemma_id) with _ -> ());
     raise e
 
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 872d3be4a..7613c6765 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1471,6 +1471,7 @@ let (com_eqn : int -> identifier ->
 
 let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq
     generate_induction_principle using_lemmas : unit =
+  let previous_label = Lib.current_command_label () in
   let function_type = interp_constr Evd.empty (Global.env()) type_of_f in
   let env = push_named (function_name,None,function_type) (Global.env()) in
   (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type);  *)
@@ -1522,7 +1523,6 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
 	  then pperrnl (str "Cannot create equation Lemma " ++ Errors.print e)
 	  else anomaly "Cannot create equation Lemma"
 	  ;
-(* 	  ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ()); *)
 	  true
 	end
     in
@@ -1554,9 +1554,8 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
       hook 
   with e ->
     begin
-      ignore(try Vernacentries.vernac_reset_name (Pp.dummy_loc,functional_id) with _ -> ());
-(*       anomaly "Cannot create termination Lemma" *)
+      (try ignore (Backtrack.backto previous_label) with _ -> ());
+      (*       anomaly "Cannot create termination Lemma" *)
       raise e
     end
 
-
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
new file mode 100644
index 000000000..a8d69bdcf
--- /dev/null
+++ b/plugins/subtac/subtac.ml
@@ -0,0 +1,227 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Compat
+open Global
+open Pp
+open Errors
+open Util
+open Names
+open Sign
+open Evd
+open Term
+open Termops
+open Namegen
+open Reductionops
+open Environ
+open Type_errors
+open Typeops
+open Libnames
+open Classops
+open List
+open Recordops
+open Evarutil
+open Pretype_errors
+open Glob_term
+open Evarconv
+open Pattern
+open Vernacexpr
+
+open Subtac_coercion
+open Subtac_utils
+open Coqlib
+open Printer
+open Subtac_errors
+open Eterm
+
+let require_library dirpath =
+  let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string dirpath)) in
+    Library.require_library [qualid] None
+
+open Pp
+open Ppconstr
+open Decl_kinds
+open Tacinterp
+open Tacexpr
+
+let solve_tccs_in_type env id isevars evm c typ =
+  if not (Evd.is_empty evm) then
+    let stmt_id = Nameops.add_suffix id "_stmt" in
+    let obls, _, c', t' = eterm_obligations env stmt_id !isevars evm 0 ~status:Expand c typ in
+      match Subtac_obligations.add_definition stmt_id ~term:c' typ obls with
+      | Subtac_obligations.Defined cst -> constant_value (Global.env())
+	  (match cst with ConstRef kn -> kn | _ -> assert false)
+      | _ ->
+	  errorlabstrm "start_proof"
+	    (str "The statement obligations could not be resolved automatically, " ++ spc () ++
+		str "write a statement definition first.")
+  else
+    let _ = Typeops.infer_type env c in c
+
+
+let start_proof_com env isevars sopt kind (bl,t) hook =
+  let id = match sopt with
+    | Some (loc,id) ->
+        (* We check existence here: it's a bit late at Qed time *)
+        if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
+          user_err_loc (loc,"start_proof",pr_id id ++ str " already exists");
+        id
+    | None ->
+	next_global_ident_away (id_of_string "Unnamed_thm")
+	  (Pfedit.get_all_proof_names ())
+  in
+  let evm, c, typ, imps =
+    Subtac_pretyping.subtac_process ~is_type:true env isevars id [] (Topconstr.prod_constr_expr t bl) None
+  in
+  let c = solve_tccs_in_type env id isevars evm c typ in
+    Lemmas.start_proof id kind c (fun loc gr ->
+      Impargs.declare_manual_implicits (loc = Local) gr ~enriching:true [imps];
+      hook loc gr)
+
+let start_proof_and_print env isevars idopt k t hook =
+  start_proof_com env isevars idopt k t hook;
+  Vernacentries.print_subgoals ()
+
+let _ = Detyping.set_detype_anonymous (fun loc n -> GVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n)))
+
+let assumption_message id =
+  Flags.if_verbose message ((string_of_id id) ^ " is assumed")
+
+let declare_assumptions env isevars idl is_coe k bl c nl =
+  if not (Pfedit.refining ()) then
+    let id = snd (List.hd idl) in
+    let evm, c, typ, imps =
+      Subtac_pretyping.subtac_process env isevars id [] (Topconstr.prod_constr_expr c bl) None
+    in
+    let c = solve_tccs_in_type env id isevars evm c typ in
+      List.iter (Command.declare_assumption is_coe k c imps false nl) idl
+  else
+    errorlabstrm "Command.Assumption"
+	(str "Cannot declare an assumption while in proof editing mode.")
+
+let dump_constraint ty ((loc, n), _, _) =
+  match n with
+    | Name id -> Dumpglob.dump_definition (loc, id) false ty
+    | Anonymous -> ()
+
+let dump_variable lid = ()
+
+let vernac_assumption env isevars kind l nl =
+  let global = fst kind = Global in
+    List.iter (fun (is_coe,(idl,c)) ->
+      if Dumpglob.dump () then
+	List.iter (fun lid ->
+	  if global then Dumpglob.dump_definition lid (not global) "ax"
+	  else dump_variable lid) idl;
+      declare_assumptions env isevars idl is_coe kind [] c nl) l
+
+let check_fresh (loc,id) =
+  if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
+    user_err_loc (loc,"",pr_id id ++ str " already exists")
+
+let subtac (loc, command) =
+  check_required_library ["Coq";"Init";"Datatypes"];
+  check_required_library ["Coq";"Init";"Specif"];
+  let env = Global.env () in
+  let isevars = ref (create_evar_defs Evd.empty) in
+  try
+  match command with
+  | VernacDefinition (defkind, (_, id as lid), expr, hook) ->
+      check_fresh lid;
+      Dumpglob.dump_definition lid false "def";
+      (match expr with
+      | ProveBody (bl, t) ->
+	  start_proof_and_print env isevars (Some lid) (Global, DefinitionBody Definition) (bl,t)
+	    (fun _ _ -> ())
+      | DefineBody (bl, _, c, tycon) ->
+	  ignore(Subtac_pretyping.subtac_proof defkind hook env isevars id bl c tycon))
+  | VernacFixpoint l ->
+      List.iter (fun ((lid, _, _, _, _), _) ->
+	check_fresh lid;
+	Dumpglob.dump_definition lid false "fix") l;
+      let _ = trace (str "Building fixpoint") in
+	ignore(Subtac_command.build_recursive l)
+
+  | VernacStartTheoremProof (thkind, [Some id, (bl,t,guard)], lettop, hook) ->
+      if guard <> None then
+        error "Do not support building theorems as a fixpoint.";
+      Dumpglob.dump_definition id false "prf";
+      if not(Pfedit.refining ()) then
+	if lettop then
+	  errorlabstrm "Subtac_command.StartProof"
+	    (str "Let declarations can only be used in proof editing mode");
+      if Lib.is_modtype () then
+	errorlabstrm "Subtac_command.StartProof"
+	  (str "Proof editing mode not supported in module types");
+      check_fresh id;
+      start_proof_and_print env isevars (Some id) (Global, Proof thkind) (bl,t) hook
+
+  | VernacAssumption (stre,nl,l) ->
+      vernac_assumption env isevars stre l nl
+
+  | VernacInstance (abst, glob, sup, is, props, pri) ->
+      dump_constraint "inst" is;
+      if abst then
+	error "Declare Instance not supported here.";
+      ignore(Subtac_classes.new_instance ~global:glob sup is props pri)
+
+  | VernacCoFixpoint l ->
+      if Dumpglob.dump () then
+	List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "cofix") l;
+      ignore(Subtac_command.build_corecursive l)
+
+  (*| VernacEndProof e ->
+    subtac_end_proof e*)
+
+  | _ -> user_err_loc (loc,"", str ("Invalid Program command"))
+  with
+  | Typing_error e ->
+      msg_warning (str "Type error in Program tactic:");
+      let cmds =
+	(match e with
+	| NonFunctionalApp (loc, x, mux, e) ->
+	    str "non functional application of term " ++
+	      e ++ str " to function " ++ x ++ str " of (mu) type " ++ mux
+	| NonSigma (loc, t) ->
+	    str "Term is not of Sigma type: " ++ t
+	| NonConvertible (loc, x, y) ->
+	    str "Unconvertible terms:" ++ spc () ++
+	      x ++ spc () ++ str "and" ++ spc () ++ y
+	| IllSorted (loc, t) ->
+	    str "Term is ill-sorted:" ++ spc () ++ t
+	)
+      in msg_warning cmds
+
+  | Subtyping_error e ->
+      msg_warning (str "(Program tactic) Subtyping error:");
+      let cmds =
+	match e with
+	| UncoercibleInferType (loc, x, y) ->
+	    str "Uncoercible terms:" ++ spc ()
+	    ++ x ++ spc () ++ str "and" ++ spc () ++ y
+	| UncoercibleInferTerm (loc, x, y, tx, ty) ->
+	    str "Uncoercible terms:" ++ spc ()
+	    ++ tx ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ x
+	    ++ str "and" ++ spc() ++ ty ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ y
+	| UncoercibleRewrite (x, y) ->
+	    str "Uncoercible terms:" ++ spc ()
+	    ++ x ++ spc () ++ str "and" ++ spc () ++ y
+      in msg_warning cmds
+
+  | Cases.PatternMatchingError (env, exn) as e -> raise e
+
+  | Type_errors.TypeError (env, exn) as e -> raise e
+
+  | Pretype_errors.PretypeError (env, _, exn) as e -> raise e
+
+  | (Loc.Exc_located (loc, Proof_type.LtacLocated (_,e')) |
+     Loc.Exc_located (loc, e') as e) -> raise e
+
+  | e ->
+      (*       msg_warning (str "Uncaught exception: " ++ Errors.print e); *)
+      raise e
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index ceed54696..a271fb336 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -126,7 +126,9 @@ val current_proof_statement :
 
 val get_current_proof_name : unit -> identifier
 
-(** [get_all_proof_names ()] returns the list of all pending proof names *)
+(** [get_all_proof_names ()] returns the list of all pending proof names.
+    The first name is the current proof, the other names may come in
+    any order. *)
 
 val get_all_proof_names : unit -> identifier list
 
diff --git a/toplevel/backtrack.ml b/toplevel/backtrack.ml
new file mode 100644
index 000000000..a84550a5d
--- /dev/null
+++ b/toplevel/backtrack.ml
@@ -0,0 +1,225 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open Vernacexpr
+
+(** Command history stack
+
+    We maintain a stack of the past states of the system. Each
+    successfully interpreted command adds an [info] element
+    to this stack, storing what were the (label / current proof / ...)
+    just _after_ the interpretation of this command.
+
+    - A label is just an integer, starting from Lib.first_command_label
+      initially, and incremented at each new successful command.
+    - If some proofs are opened, we have their number in [nproofs],
+      the name of the current proof in [prfname], the current depth in
+      [prfdepth].
+    - Otherwise, [nproofs = 0], [prfname = None], [prfdepth = 0]
+    - The text of the command is stored (for Show Script currently).
+    - A command can be tagged later as non-"reachable" when the current proof
+      at the time of this command has been ended by Qed/Abort/Restart,
+      meaning we can't backtrack there.
+*)
+
+type info = {
+  label : int;
+  nproofs : int;
+  prfname : identifier option;
+  prfdepth : int;
+  cmd : vernac_expr;
+  mutable reachable : bool;
+}
+
+let history : info Stack.t = Stack.create ()
+
+(** For debug purpose, a dump of the history *)
+
+let dump_history () =
+  let l = ref [] in
+  Stack.iter (fun i -> l:=i::!l) history;
+  !l
+
+(** Basic manipulation of the command history stack *)
+
+exception Invalid
+
+let pop () = ignore (Stack.pop history)
+
+let npop n =
+ (* Since our history stack always contains an initial entry,
+    it's invalid to try to completely empty it *)
+ if n < 0 || n >= Stack.length history then raise Invalid
+ else for i = 1 to n do pop () done
+
+let top () =
+  try Stack.top history with Stack.Empty -> raise Invalid
+
+(** Search the history stack for a suitable location. We perform first
+    a non-destructive search: in case of search failure, the stack is
+    unchanged. *)
+
+exception Found of info
+
+let search test =
+  try
+    Stack.iter (fun i -> if test i then raise (Found i)) history;
+    raise Invalid
+  with Found i ->
+    while i != Stack.top history do pop () done
+
+(** Register the end of a command and store the current state *)
+
+let mark_command ast =
+  Lib.add_frozen_state();
+  Lib.mark_end_of_command();
+  Stack.push
+    { label = Lib.current_command_label ();
+      nproofs = List.length (Pfedit.get_all_proof_names ());
+      prfname = (try Some (Pfedit.get_current_proof_name ()) with _ -> None);
+      prfdepth = max 0 (Pfedit.current_proof_depth ());
+      reachable = true;
+      cmd = ast }
+    history
+
+(** Backtrack by aborting [naborts] proofs, then setting proof-depth back to
+    [pnum] and finally going to state number [snum]. *)
+
+let raw_backtrack snum pnum naborts =
+  for i = 1 to naborts do Pfedit.delete_current_proof () done;
+  Pfedit.undo_todepth pnum;
+  Lib.reset_label snum
+
+(** Re-sync the state of the system (label, proofs) with the top
+    of the history stack. We may end on some earlier state to avoid
+    re-opening proofs. This function will return the final label
+    and the number of extra backtracking steps performed. *)
+
+let sync nb_opened_proofs =
+  (* 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 first entry in the
+     stack has no opened proofs and is tagged as reachable.
+  *)
+  let extra = ref 0 in
+  while not (top()).reachable do incr extra; pop () done;
+  let target = top ()
+  in
+  (* Now the opened proofs at target is a subset of the opened proofs before
+     the backtrack, we simply abort the extra proofs (if any).
+     NB: It is critical here that proofs are nested in a regular way
+     (i.e. no more Resume or Suspend commands as earlier). This way, we can
+     simply count the extra proofs to abort instead of taking care of their
+     names.
+  *)
+  let naborts = nb_opened_proofs - target.nproofs in
+  (* We are now ready to do a low-level backtrack *)
+  raw_backtrack target.label target.prfdepth naborts;
+  (target.label, !extra)
+
+(** Backtracking by a certain number of (non-state-preserving) commands.
+    This is used by Coqide.
+    It may actually undo more commands than asked : for instance instead
+    of jumping back in the middle of a finished proof, we jump back before
+    this proof. The number of extra backtracked command is returned at
+    the end. *)
+
+let back count =
+  if count = 0 then 0
+  else
+    let nb_opened_proofs = List.length (Pfedit.get_all_proof_names ()) in
+    npop count;
+    snd (sync nb_opened_proofs)
+
+(** Backtracking to a certain state number, and reset proofs accordingly.
+    We may end on some earlier state if needed to avoid re-opening proofs.
+    Return the final state number. *)
+
+let backto snum =
+  if snum = Lib.current_command_label () then snum
+  else
+    let nb_opened_proofs = List.length (Pfedit.get_all_proof_names ()) in
+    search (fun i -> i.label = snum);
+    fst (sync nb_opened_proofs)
+
+(** Old [Backtrack] code with corresponding update of the history stack.
+    [Backtrack] is now deprecated (in favor of [BackTo]) but is kept for
+    compatibility with ProofGeneral. It's completely up to ProofGeneral
+    to decide where to go and how to adapt proofs. Note that the choices
+    of ProofGeneral are currently not always perfect (for instance when
+    backtracking an Undo). *)
+
+let backtrack snum pnum naborts =
+  raw_backtrack snum pnum naborts;
+  search (fun i -> i.label = snum)
+
+(** [reset_initial] resets the system and clears the command history
+    stack, only pushing back the initial entry. It should be equivalent
+    to [backto Lib.first_command_label], but sligthly more efficient. *)
+
+let reset_initial () =
+  let init_label = Lib.first_command_label in
+  if Lib.current_command_label () = init_label then ()
+  else begin
+    if Pfedit.refining() then Pfedit.delete_all_proofs ();
+    Lib.reset_label init_label;
+    Stack.clear history;
+    Stack.push
+      { label = init_label;
+	nproofs = 0;
+	prfname = None;
+	prfdepth = 0;
+	reachable = true;
+	cmd = VernacNop }
+      history
+  end
+
+(** Reset to the last known state just before defining [id] *)
+
+let reset_name id =
+  let lbl =
+    try Lib.label_before_name id with Not_found -> raise Invalid
+  in
+  ignore (backto lbl)
+
+(** When a proof is ended (via either Qed/Admitted/Restart/Abort),
+    old proof steps should be marked differently to avoid jumping back
+    to them:
+     - either this proof isn't there anymore in the proof engine
+     - either it's there but it's a more recent attempt after a Restart,
+       so we shouldn't mix the two.
+    We also mark as unreachable the proof steps cancelled via a Undo. *)
+
+let mark_unreachable ?(after=0) prf_lst =
+  let fix i = match i.prfname with
+    | None -> raise Not_found (* stop hacking the history outside of proofs *)
+    | Some p ->
+      if List.mem p prf_lst && i.prfdepth > after
+      then i.reachable <- false
+  in
+  try Stack.iter fix history with Not_found -> ()
+
+(** Parse the history stack for printing the script of a proof *)
+
+let get_script prf =
+  let script = ref [] in
+  let select i = match i.prfname with
+    | None -> raise Not_found
+    | Some p when p=prf && i.reachable -> script := i :: !script
+    | _ -> ()
+  in
+  (try Stack.iter select history with Not_found -> ());
+  (* Get rid of intermediate commands which don't grow the depth *)
+  let rec filter n = function
+    | [] -> []
+    | {prfdepth=d; cmd=c}::l when n < d -> c :: filter d l
+    | {prfdepth=d}::l -> filter d l
+  in
+  (* initial proof depth (after entering the lemma statement) is 1 *)
+  filter 1 !script
diff --git a/toplevel/backtrack.mli b/toplevel/backtrack.mli
new file mode 100644
index 000000000..f6c69d890
--- /dev/null
+++ b/toplevel/backtrack.mli
@@ -0,0 +1,93 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Command history stack
+
+    We maintain a stack of the past states of the system after each
+    (non-state-preserving) interpreted commands
+*)
+
+(** [mark_command ast] marks the end of a command:
+    - it stores a frozen state and a end of command in the Lib stack,
+    - it stores the current state information in the command history
+    stack *)
+
+val mark_command : Vernacexpr.vernac_expr -> unit
+
+(** The [Invalid] exception is raised when one of the following function
+    tries to empty the history stack, or reach an unknown states, etc.
+    The stack is preserved in these cases. *)
+
+exception Invalid
+
+(** Nota Bene: it is critical for the following functions that proofs
+    are nested in a regular way (i.e. no more Resume or Suspend commands
+    as earlier). *)
+
+(** Backtracking by a certain number of (non-state-preserving) commands.
+    This is used by Coqide.
+    It may actually undo more commands than asked : for instance instead
+    of jumping back in the middle of a finished proof, we jump back before
+    this proof. The number of extra backtracked command is returned at
+    the end. *)
+
+val back : int -> int
+
+(** Backtracking to a certain state number, and reset proofs accordingly.
+    We may end on some earlier state if needed to avoid re-opening proofs.
+    Return the state number on which we finally end. *)
+
+val backto : int -> int
+
+(** Old [Backtrack] code with corresponding update of the history stack.
+    [Backtrack] is now deprecated (in favor of [BackTo]) but is kept for
+    compatibility with ProofGeneral. It's completely up to ProofGeneral
+    to decide where to go and how to adapt proofs. Note that the choices
+    of ProofGeneral are currently not always perfect (for instance when
+    backtracking an Undo). *)
+
+val backtrack : int -> int -> int -> unit
+
+(** [reset_initial] resets the system and clears the command history
+    stack, only pushing back the initial entry. It should be equivalent
+    to [backto Lib.first_command_label], but sligthly more efficient. *)
+
+val reset_initial : unit -> unit
+
+(** Reset to the last known state just before defining [id] *)
+
+val reset_name : Names.identifier Pp.located -> unit
+
+(** When a proof is ended (via either Qed/Admitted/Restart/Abort),
+    old proof steps should be marked differently to avoid jumping back
+    to them:
+     - either this proof isn't there anymore in the proof engine
+     - either a proof with the same name is there, but it's a more recent
+       attempt after a Restart/Abort, we shouldn't mix the two.
+    We also mark as unreachable the proof steps cancelled via a Undo.
+*)
+
+val mark_unreachable : ?after:int -> Names.identifier list -> unit
+
+(** Parse the history stack for printing the script of a proof *)
+
+val get_script : Names.identifier -> Vernacexpr.vernac_expr list
+
+
+(** For debug purpose, a dump of the history *)
+
+type info = {
+  label : int;
+  nproofs : int;
+  prfname : Names.identifier option;
+  prfdepth : int;
+  cmd : Vernacexpr.vernac_expr;
+  mutable reachable : bool;
+}
+
+val dump_history : unit -> info list
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index d17d07300..bf5c84e64 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -248,10 +248,13 @@ let parse_args arglist =
     | "-compat" :: []       -> usage ()
 
     | "-vm" :: rem -> use_vm := true; parse rem
-    | "-emacs" :: rem -> Flags.print_emacs := true; Pp.make_pp_emacs(); parse rem
+    | "-emacs" :: rem ->
+	Flags.print_emacs := true; Pp.make_pp_emacs();
+	Vernacentries.qed_display_script := false;
+	parse rem
     | "-emacs-U" :: rem ->
 	warning "Obsolete option \"-emacs-U\", use -emacs instead.";	
-	Flags.print_emacs := true; Pp.make_pp_emacs(); parse rem
+	parse ("-emacs" :: rem)
 
     | "-unicode" :: rem -> add_require "Utf8_core"; parse rem
 
@@ -351,7 +354,8 @@ let init arglist =
        Pp.ppnl (with_option raw_print Prettyp.print_full_pure_context ());
      Profile.print_profile ();
      exit 0);
-  Lib.declare_initial_state ()
+  (* We initialize the command history stack with a first entry *)
+  Backtrack.mark_command Vernacexpr.VernacNop
 
 let init_toplevel = init
 
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index bc024e641..f8bf9fccb 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -21,12 +21,6 @@ open Namegen
     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. *)
 
@@ -74,282 +68,56 @@ let coqide_known_option table = List.mem table [
   ["Printing";"Existential";"Instances"];
   ["Printing";"Universes"]]
 
-type command_attribute =
-    NavigationCommand | QueryCommand | DebugCommand | KnownOptionCommand
-    | OtherStatePreservingCommand | GoalStartingCommand | SolveCommand
-    | ProofEndingCommand
-
-let rec attribute_of_vernac_command = function
-  (* Control *)
-  | VernacTime com -> attribute_of_vernac_command com
-  | VernacTimeout(_,com) -> attribute_of_vernac_command com
-  | VernacFail com -> attribute_of_vernac_command com
-  | VernacList _ -> [] (* unsupported *)
-  | VernacLoad _ -> []
-
-  (* Syntax *)
-  | VernacTacticNotation _ -> []
-  | VernacSyntaxExtension _ -> []
-  | VernacDelimiters _ -> []
-  | VernacBindScope _ -> []
-  | VernacOpenCloseScope _ -> []
-  | VernacArgumentsScope _ -> []
-  | VernacInfix _ -> []
-  | VernacNotation _ -> []
-
-  (* Gallina *)
-  | VernacDefinition (_,_,DefineBody _,_) -> []
-  | VernacDefinition (_,_,ProveBody _,_) -> [GoalStartingCommand]
-  | VernacStartTheoremProof _ -> [GoalStartingCommand]
-  | VernacEndProof _ -> [ProofEndingCommand]
-  | VernacExactProof _ -> [ProofEndingCommand]
-
-  | VernacAssumption _ -> []
-  | VernacInductive _ -> []
-  | VernacFixpoint _ -> []
-  | VernacCoFixpoint _ -> []
-  | VernacScheme _ -> []
-  | VernacCombinedScheme _ -> []
-
-  (* Modules *)
-  | VernacDeclareModule _ -> []
-  | VernacDefineModule _  -> []
-  | VernacDeclareModuleType _ -> []
-  | VernacInclude _ -> []
-
-  (* Gallina extensions *)
-  | VernacBeginSection _ -> []
-  | VernacEndSegment _ -> []
-  | VernacRequire _ -> []
-  | VernacImport _ -> []
-  | VernacCanonical _ -> []
-  | VernacCoercion _ -> []
-  | VernacIdentityCoercion _ -> []
-
-  (* Type classes *)
-  | VernacInstance _ -> []
-  | VernacContext _ -> []
-  | VernacDeclareInstances _ -> []
-  | VernacDeclareClass _ -> []
-
-  (* Solving *)
-  | VernacSolve _ -> [SolveCommand]
-  | VernacSolveExistential _ -> [SolveCommand]
-
-  (* Auxiliary file and library management *)
-  | VernacRequireFrom _ -> []
-  | VernacAddLoadPath _ -> []
-  | VernacRemoveLoadPath _ -> []
-  | VernacAddMLPath _ -> []
-  | VernacDeclareMLModule _ -> []
-  | 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 _ -> []
-  | VernacRestoreState _ -> []
-
-  (* Resetting *)
-  | VernacResetName _ -> [NavigationCommand]
-  | VernacResetInitial -> [NavigationCommand]
-  | VernacBack _ -> [NavigationCommand]
-  | VernacBackTo _ -> [NavigationCommand]
-
-  (* Commands *)
-  | VernacDeclareTacticDefinition _ -> []
-  | VernacCreateHintDb _ -> []
-  | VernacRemoveHints _ -> []
-  | VernacHints _ -> []
-  | VernacSyntacticDefinition _ -> []
-  | VernacDeclareImplicits _ -> []
-  | VernacArguments _ -> [] 
-  | VernacDeclareReduction _ -> []
-  | VernacReserve _ -> []
-  | VernacGeneralizable _ -> []
-  | VernacSetOpacity _ -> []
-  | VernacSetOption (_,["Ltac";"Debug"], _) -> [DebugCommand]
-  | VernacSetOption (_,o,BoolValue true) | VernacUnsetOption (_,o) ->
-      if coqide_known_option o then [KnownOptionCommand] else []
-  | VernacSetOption _ -> []
-  | VernacRemoveOption _ -> []
-  | VernacAddOption _ -> []
-  | VernacMemOption _ -> [QueryCommand]
-
-  | VernacPrintOption _ -> [QueryCommand]
-  | VernacCheckMayEval _ -> [QueryCommand]
-  | VernacGlobalCheck _ -> [QueryCommand]
-  | VernacPrint _ -> [QueryCommand]
-  | VernacSearch _ -> [QueryCommand]
-  | VernacLocate _ -> [QueryCommand]
-
-  | VernacComments _ -> [OtherStatePreservingCommand]
-  | VernacNop -> [OtherStatePreservingCommand]
-
-  (* Proof management *)
-  | VernacGoal _ -> [GoalStartingCommand]
-
-  | VernacAbort _ -> []
-  | VernacAbortAll -> [NavigationCommand]
-  | VernacRestart -> [NavigationCommand]
-  | VernacUndo _ -> [NavigationCommand]
-  | VernacUndoTo _ -> [NavigationCommand]
-  | VernacBacktrack _ -> [NavigationCommand]
-
-  | VernacFocus _ -> [SolveCommand]
-  | VernacUnfocus -> [SolveCommand]
-  | VernacShow _ -> [OtherStatePreservingCommand]
-  | VernacCheckGuard -> [OtherStatePreservingCommand]
-  | VernacProof (None, None) -> [OtherStatePreservingCommand]
-  | VernacProof _ -> []
-
-  | VernacProofMode _ -> []
-  | VernacBullet _ -> [SolveCommand]
-  | VernacSubproof _ -> [SolveCommand]
-  | VernacEndSubproof -> [SolveCommand]
-
-  (* Toplevel control *)
-  | VernacToplevelControl _ -> []
-
-  (* Extensions *)
-  | VernacExtend ("Subtac_Obligations", _) -> [GoalStartingCommand]
-  | VernacExtend _ -> []
-
-let is_vernac_navigation_command com =
-  List.mem NavigationCommand (attribute_of_vernac_command com)
-
-let is_vernac_query_command com =
-  List.mem QueryCommand (attribute_of_vernac_command com)
-
-let is_vernac_known_option_command com =
-  List.mem KnownOptionCommand (attribute_of_vernac_command com)
-
-let is_vernac_debug_command com =
-  List.mem DebugCommand (attribute_of_vernac_command com)
-
-let is_vernac_goal_printing_command com =
-  let attribute = attribute_of_vernac_command com in
-  List.mem GoalStartingCommand attribute or
-    List.mem SolveCommand attribute
-
-let is_vernac_state_preserving_command com =
-  let attribute = attribute_of_vernac_command com in
-  List.mem OtherStatePreservingCommand attribute or
-    List.mem QueryCommand attribute
-
-let is_vernac_tactic_command com =
-  List.mem SolveCommand (attribute_of_vernac_command com)
-
-let is_vernac_proof_ending_command com =
-  List.mem ProofEndingCommand (attribute_of_vernac_command com)
-
-
-(** 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 compute_reset_info () =
-  { label = Lib.current_command_label ();
-    proofs = Pfedit.get_all_proof_names ();
-    depth = max 0 (Pfedit.current_proof_depth ()) }
-
-
-(** Interpretation (cf. [Ide_intf.interp]) *)
+let is_known_option cmd = match cmd with
+  | VernacSetOption (_,o,BoolValue true)
+  | VernacUnsetOption (_,o) -> coqide_known_option o
+  | _ -> false
+
+let is_debug cmd = match cmd with
+  | VernacSetOption (_,["Ltac";"Debug"], _) -> true
+  | _ -> false
+
+let is_query cmd = match cmd with
+  | VernacChdir None
+  | VernacMemOption _
+  | VernacPrintOption _
+  | VernacCheckMayEval _
+  | VernacGlobalCheck _
+  | VernacPrint _
+  | VernacSearch _
+  | VernacLocate _ -> true
+  | _ -> false
+
+let is_undo cmd = match cmd with
+  | VernacUndo _ | VernacUndoTo _ -> true
+  | _ -> false
 
 (** Check whether a command is forbidden by CoqIDE *)
 
 let coqide_cmd_checks (loc,ast) =
-  let user_error s =
-    raise (Loc.Exc_located (loc, Errors.UserError ("CoqIde", str s)))
-  in
-  if is_vernac_debug_command ast then
+  let user_error s = Errors.user_err_loc (loc, "CoqIde", str s) in
+  if is_debug ast then
     user_error "Debug mode not available within CoqIDE";
-  if is_vernac_navigation_command ast then
-    user_error "Use CoqIDE navigation instead";
-  if is_vernac_known_option_command ast then
+  if is_known_option ast then
     user_error "Use CoqIDE display menu instead";
-  if is_vernac_query_command ast then
+  if is_navigation_vernac ast then
+    user_error "Use CoqIDE navigation instead";
+  if is_undo ast then
+    msgerrnl (str "Warning: rather use CoqIDE navigation instead");
+  if is_query ast then
     msgerrnl (str "Warning: query commands should not be inserted in scripts")
 
-let raw_eval_expr = Vernac.eval_expr
-
-let eval_expr loc_ast =
-  let rewind_info = compute_reset_info () in
-  raw_eval_expr loc_ast;
-  Stack.push rewind_info com_stk
+(** Interpretation (cf. [Ide_intf.interp]) *)
 
 let interp (raw,verbosely,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;
-  (* 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 (not verbosely);
+  Vernac.eval_expr ~preserving:raw loc_ast;
   Flags.make_silent true;
-  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 =
-  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
-
-
 (** Goal display *)
 
 let hyp_next_tac sigma env (id,_,ast) =
@@ -514,7 +282,7 @@ let eval_call c =
   in
   let handler = {
     Interface.interp = interruptible interp;
-    Interface.rewind = interruptible rewind;
+    Interface.rewind = interruptible Backtrack.back;
     Interface.goals = interruptible goals;
     Interface.evars = interruptible evars;
     Interface.hints = interruptible hints;
@@ -550,9 +318,9 @@ let loop () =
   let () = Xml_parser.check_eof p false in
   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();
+  (* We'll handle goal fetching and display in our own way *)
+  Vernacentries.enable_goal_printing := false;
+  Vernacentries.qed_display_script := false;
   try
     while true do
       let xml_answer =
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 5187b3a28..6a06ba3dc 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -368,9 +368,6 @@ let do_vernac () =
 
 let rec loop () =
   Sys.catch_break true;
-  (* ensure we have a command separator object (DOT) so that the first
-     command can be reseted. *)
-  Lib.mark_end_of_command();
   try
     reset_input_buffer stdin top_buffer;
     while true do do_vernac() done
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index 2ca2f0739..599f8e9ff 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -14,6 +14,7 @@ Command
 Classes
 Record
 Ppvernac
+Backtrack
 Vernacinterp
 Mltop
 Vernacentries
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 60354f4cf..20b45a2b0 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -52,6 +52,8 @@ let real_error = function
   | Error_in_file (_, _, e) -> e
   | e -> e
 
+let user_error loc s = Errors.user_err_loc (loc,"_",str s)
+
 (** Timeout handling *)
 
 (** A global default timeout, controled by option "Set Default Timeout n".
@@ -167,7 +169,7 @@ let pr_new_syntax loc ocom =
   States.unfreeze fs;
   Format.set_formatter_out_channel stdout
 
-let rec vernac_com interpfun (loc,com) =
+let rec vernac_com interpfun checknav (loc,com) =
   let rec interp = function
     | VernacLoad (verbosely, fname) ->
 	let fname = expand_path_macros fname in
@@ -205,8 +207,10 @@ let rec vernac_com interpfun (loc,com) =
 
     | VernacList l -> List.iter (fun (_,v) -> interp v) l
 
+    | v when !just_parsing -> ()
+
     | VernacFail v ->
-	if not !just_parsing then begin try
+	begin try
 	  (* If the command actually works, ignore its effects on the state *)
 	  States.with_state_protection
 	    (fun v -> interp v; raise HasNotFailed) v
@@ -222,22 +226,17 @@ let rec vernac_com interpfun (loc,com) =
 	end
 
     | VernacTime v ->
-	if not !just_parsing then begin
 	  let tstart = System.get_time() in
           interp v;
 	  let tend = System.get_time() in
           msgnl (str"Finished transaction in " ++
                    System.fmt_time_difference tstart tend)
-	end
 
     | VernacTimeout(n,v) ->
-	if not !just_parsing then begin
 	  current_timeout := Some n;
 	  interp v
-	end
 
     | v ->
-        if not !just_parsing then
 	  let psh = default_set_timeout () in
 	  try
             States.with_heavy_rollback interpfun
@@ -246,6 +245,7 @@ let rec vernac_com interpfun (loc,com) =
 	  with e -> restore_timeout psh; raise e
   in
     try
+      checknav loc com;
       current_timeout := !default_timeout;
       if do_beautify () then pr_new_syntax loc (Some com);
       interp com
@@ -259,13 +259,17 @@ and read_vernac_file verbosely s =
     if verbosely then Vernacentries.interp
     else Flags.silently Vernacentries.interp
   in
+  let checknav loc cmd =
+    if is_navigation_vernac cmd then
+	user_error loc "Navigation commands forbidden in files"
+  in
   let (in_chan, fname, input) =
     open_file_twice_if verbosely s in
   try
     (* we go out of the following infinite loop when a End_of_input is
      * raised, which means that we raised the end of the file being loaded *)
     while true do
-      vernac_com interpfun (parse_sentence input);
+      vernac_com interpfun checknav (parse_sentence input);
       pp_flush ()
     done
   with e ->   (* whatever the exception *)
@@ -276,15 +280,21 @@ and read_vernac_file verbosely s =
           if do_beautify () then pr_new_syntax (make_loc (max_int,max_int)) None
       | _ -> raise_with_file fname e
 
-
-(* eval_expr : Util.loc * Vernacexpr.vernac_expr -> unit
- * execute one vernacular command. Marks the end of the command in the lib_stk
- * with a new label to make vernac undoing easier. Also freeze state to speed up
- * backtracking. *)
-let eval_expr last =
-  vernac_com Vernacentries.interp last;
-  Lib.add_frozen_state();
-  Lib.mark_end_of_command()
+(** [eval_expr : ?preserving:bool -> Pp.loc * Vernacexpr.vernac_expr -> unit]
+   It executes one vernacular command. By default the command is
+   considered as non-state-preserving, in which case we add it to the
+   Backtrack stack (triggering a save of a frozen state and the generation
+   of a new state label). An example of state-preserving command is one coming
+   from the query panel of Coqide. *)
+
+let checknav loc ast =
+  if is_deep_navigation_vernac ast then
+    user_error loc "Navigation commands forbidden in nested commands"
+
+let eval_expr ?(preserving=false) loc_ast =
+  vernac_com Vernacentries.interp checknav loc_ast;
+  if not preserving && not (is_navigation_vernac (snd loc_ast)) then
+    Backtrack.mark_command (snd loc_ast)
 
 (* raw_do_vernac : Pcoq.Gram.parsable -> unit
  * vernac_step . parse_sentence *)
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 1cfd94e05..9998fb19c 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -21,7 +21,14 @@ exception DuringCommandInterp of Pp.loc * exn
 exception End_of_input
 
 val just_parsing : bool ref
-val eval_expr : Pp.loc * Vernacexpr.vernac_expr -> unit
+
+(** [eval_expr] executes one vernacular command. By default the command is
+   considered as non-state-preserving, in which case we add it to the
+   Backtrack stack (triggering a save of a frozen state and the generation
+   of a new state label). An example of state-preserving command is one coming
+   from the query panel of Coqide. *)
+
+val eval_expr : ?preserving:bool -> Pp.loc * Vernacexpr.vernac_expr -> unit
 val raw_do_vernac : Pcoq.Gram.parsable -> unit
 
 (** Set XML hooks *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 6100fbd1d..1b89eaa68 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -74,8 +74,9 @@ let show_node () =
   ()
 
 let show_script () =
-  (* spiwack: show_script is currently not working *)
-  ()
+  let prf = Pfedit.get_current_proof_name () in
+  let cmds = Backtrack.get_script prf in
+  msgnl (Pp.prlist_with_sep Pp.fnl Ppvernac.pr_vernac cmds)
 
 let show_thesis () =
      msgnl (anomaly "TODO" )
@@ -92,7 +93,16 @@ let show_prooftree () =
   (* Spiwack: proof tree is currently not working *)
   ()
 
-let print_subgoals () = if_verbose (fun () -> msg (pr_open_subgoals ())) ()
+let enable_goal_printing = ref true
+
+let print_subgoals () =
+  if !enable_goal_printing && is_verbose ()
+  then msg (pr_open_subgoals ())
+
+let try_print_subgoals () =
+  Pp.flush_all();
+  try print_subgoals () with Proof_global.NoCurrentProof | UserError _ -> ()
+
 
   (* Simulate the Intro(s) tactic *)
 
@@ -357,14 +367,21 @@ let vernac_start_proof kind l lettop hook =
 	(str "Let declarations can only be used in proof editing mode.");
   start_proof_and_print (Global, Proof kind) l hook
 
+let qed_display_script = ref true
+
 let vernac_end_proof = function
-  | Admitted -> admit ()
+  | Admitted ->
+    Backtrack.mark_unreachable [Pfedit.get_current_proof_name ()];
+    admit ()
   | Proved (is_opaque,idopt) ->
-    if not !Flags.print_emacs then if_verbose show_script ();
-    match idopt with
+    let prf = Pfedit.get_current_proof_name () in
+    if is_verbose () && !qed_display_script then (show_script (); msg (fnl()));
+    begin match idopt with
     | None -> save_named is_opaque
     | Some ((_,id),None) -> save_anonymous is_opaque id
     | Some ((_,id),Some kind) -> save_anonymous_with_strength kind is_opaque id
+    end;
+    Backtrack.mark_unreachable [prf]
 
   (* A stupid macro that should be replaced by ``Exact c. Save.'' all along
      the theories [??] *)
@@ -732,19 +749,6 @@ let vernac_write_state file = abort_refine States.extern_state file
 
 let vernac_restore_state file = abort_refine States.intern_state file
 
-
-(*************)
-(* Resetting *)
-
-let vernac_reset_name id = abort_refine Lib.reset_name id
-
-let vernac_reset_initial () = abort_refine Lib.reset_initial ()
-
-let vernac_back n = Lib.back n
-
-let vernac_backto n = Lib.reset_label n
-
-(* see also [vernac_backtrack] which combines undoing and resetting *)
 (************)
 (* Commands *)
 
@@ -1320,15 +1324,54 @@ let vernac_locate = function
   | LocateTactic qid -> print_located_tactic qid
   | LocateFile f -> locate_file f
 
+(****************)
+(* Backtracking *)
+
+(** NB: these commands are now forbidden in non-interactive use,
+    e.g. inside VernacLoad, VernacList, ... *)
+
+let vernac_backto lbl =
+  try
+    let lbl' = Backtrack.backto lbl in
+    if lbl <> lbl' then
+      Pp.msg_warning
+	(str "Actually back to state "++ Pp.int lbl' ++ str ".");
+    try_print_subgoals ()
+  with Backtrack.Invalid -> error "Invalid backtrack."
+
+let vernac_back n =
+  try
+    let extra = Backtrack.back n in
+    if extra <> 0 then
+      Pp.msg_warning
+	(str "Actually back by " ++ Pp.int (extra+n) ++ str " steps.");
+    try_print_subgoals ()
+  with Backtrack.Invalid -> error "Invalid backtrack."
+
+let vernac_reset_name id =
+  try Backtrack.reset_name id; try_print_subgoals ()
+  with Backtrack.Invalid -> error "Invalid Reset."
+
+let vernac_reset_initial () = Backtrack.reset_initial ()
+
+(* For compatibility with ProofGeneral: *)
+
+let vernac_backtrack snum pnum naborts =
+  Backtrack.backtrack snum pnum naborts;
+  try_print_subgoals ()
+
+
 (********************)
 (* Proof management *)
 
 let vernac_abort = function
   | None ->
+      Backtrack.mark_unreachable [Pfedit.get_current_proof_name ()];
       delete_current_proof ();
       if_verbose message "Current goal aborted";
       if !pcoq <> None then (Option.get !pcoq).abort ""
   | Some id ->
+      Backtrack.mark_unreachable [snd id];
       delete_proof id;
       let s = string_of_id (snd id) in
       if_verbose message ("Goal "^s^" aborted");
@@ -1336,37 +1379,30 @@ let vernac_abort = function
 
 let vernac_abort_all () =
   if refining() then begin
+    Backtrack.mark_unreachable (Pfedit.get_all_proof_names ());
     delete_all_proofs ();
     message "Current goals aborted"
   end else
     error "No proof-editing in progress."
 
-let vernac_restart () = restart_proof(); print_subgoals ()
-
-  (* Proof switching *)
+let vernac_restart () =
+  Backtrack.mark_unreachable [Pfedit.get_current_proof_name ()];
+  restart_proof(); print_subgoals ()
 
 let vernac_undo n =
-  undo n;
-  print_subgoals ()
-
-(* backtrack with [naborts] abort, then undo_todepth to [pnum], then
-   back-to state number [snum]. This allows to backtrack proofs and
-   state with one command (easier for proofgeneral). *)
-let vernac_backtrack snum pnum naborts =
-  for i = 1 to naborts do vernac_abort None done;
-  undo_todepth pnum;
-  vernac_backto snum;
-  Pp.flush_all();
-  (* there may be no proof in progress, even if no abort *)
-  (try print_subgoals () with Proof_global.NoCurrentProof | UserError _ -> ())
+  let d = Pfedit.current_proof_depth () - n in
+  Backtrack.mark_unreachable ~after:d [Pfedit.get_current_proof_name ()];
+  Pfedit.undo n; print_subgoals ()
 
+let vernac_undoto n =
+  Backtrack.mark_unreachable ~after:n [Pfedit.get_current_proof_name ()];
+  Pfedit.undo_todepth n;
+  print_subgoals ()
 
 let vernac_focus gln =
   let p = Proof_global.give_me_the_proof () in
-  match gln with
-    | None -> Proof.focus focus_command_cond () 1 p; print_subgoals ()
-    | Some n -> Proof.focus focus_command_cond () n p; print_subgoals ()
-
+  let n = match gln with None -> 1 | Some n -> n in
+  Proof.focus focus_command_cond () n p; print_subgoals ()
 
   (* Unfocuses one step in the focus stack. *)
 let vernac_unfocus () =
@@ -1548,7 +1584,7 @@ let interp c = match c with
   | VernacAbortAll -> vernac_abort_all ()
   | VernacRestart -> vernac_restart ()
   | VernacUndo n -> vernac_undo n
-  | VernacUndoTo n -> undo_todepth n
+  | VernacUndoTo n -> vernac_undoto n
   | VernacBacktrack (snum,pnum,naborts) -> vernac_backtrack snum pnum naborts
   | VernacFocus n -> vernac_focus n
   | VernacUnfocus -> vernac_unfocus ()
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 2b6a881d4..66aa6c20a 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -51,14 +51,23 @@ val abort_refine : ('a -> unit) -> 'a -> unit;;
 
 val interp : Vernacexpr.vernac_expr -> unit
 
-val vernac_reset_name : identifier Pp.located -> unit
+(** Print subgoals when the verbose flag is on.
+    Meant to be used inside vernac commands from plugins. *)
 
-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
 
+(** The printing of goals via [print_subgoals] or during
+    [interp] can be controlled by the following flag.
+    Used for instance by coqide, since it has its own
+    goal-fetching mechanism. *)
+
+val enable_goal_printing : bool ref
+
+(** Should Qed try to display the proof script ?
+    True by default, but false in ProofGeneral and coqIDE *)
+
+val qed_display_script : bool ref
+
 (** Prepare a "match" template for a given inductive type.
     For each branch of the match, we list the constructor name
     followed by enough pattern variables.
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index c017393c1..259329a10 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -367,6 +367,26 @@ type vernac_expr =
 
 and located_vernac_expr = loc * vernac_expr
 
+
+(** Categories of [vernac_expr] *)
+
+let rec strip_vernac = function
+  | VernacTime c | VernacTimeout(_,c) | VernacFail c -> strip_vernac c
+  | c -> c (* TODO: what about VernacList ? *)
+
+let rec is_navigation_vernac = function
+  | VernacResetInitial
+  | VernacResetName _
+  | VernacBacktrack _
+  | VernacBackTo _
+  | VernacBack _ -> true
+  | c -> is_deep_navigation_vernac c
+
+and is_deep_navigation_vernac = function
+  | VernacTime c | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c
+  | VernacList l -> List.exists (fun (_,c) -> is_navigation_vernac c) l
+  | _ -> false
+
 (* Locating errors raised just after the dot is parsed but before the
    interpretation phase *)