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

2 files changed, 4 insertions, 5 deletions

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
 
-