Implementation of a new backtracking system, that allow to go back

anywhere in a script (provided no suspend/resume is used):

* the command "Backtrack n m p" (vernac_bactrack) performs the
  following operation:

** do abort p times,
** do undo on the current proof (after the aborts) in order to reach a
   stack depth of m (see vernac_undo_todepth)
** resets the global state to state labelled with n.

* The coq prompt in emacs mode has more informations, it contains:

** the usual coq prompt plus:
** the state number (global state label)
** the depth of the current proof stack
** the names of all pending proofs, in *unspecified* order, separated by '|'

 Example:

     state                        proof stack
      num                           depth
       __                              _
 aux < 12 |aux|SmallStepAntiReflexive| 4 < ù
 ^^^^^^   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^     ^
 usual           pending proofs           usual
                                          special char


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

2 files changed, 23 insertions, 0 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index bbcda792f..f724589f6 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -174,6 +174,21 @@ let undo n =
   with (Invalid_argument "Edit.undo") ->
     errorlabstrm "Pfedit.undo" (str"No focused proof" ++ msg_proofs true)
 
+(* Undo current focused proof to reach depth [n]. This is used in
+   [vernac_backtrack]. *)
+let undo_todepth n =
+  try 
+    Edit.undo_todepth proof_edits n
+  with (Invalid_argument "Edit.undo") ->
+    errorlabstrm "Pfedit.undo" (str"No focused proof" ++ msg_proofs true)
+
+(* Return the depth of the current focused proof stack, this is used
+   to put informations in coq prompt (in emacs mode). *)
+let current_proof_depth() = 
+  try
+    Edit.depth proof_edits
+  with (Invalid_argument "Edit.depth") -> -1
+
 (*********************************************************************)
 (*                  Proof cooking                                    *)
 (*********************************************************************)
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index b0aacd86c..eca13c56c 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -57,6 +57,14 @@ val delete_all_proofs : unit -> unit
 
 val undo : int -> unit
 
+(* Same as undo, but undoes the current proof stack to reach depth
+   [n]. This is used in [vernac_backtrack]. *)
+val undo_todepth : int -> unit
+
+(* Returns the depth of the current focused proof stack, this is used
+   to put informations in coq prompt (in emacs mode). *)
+val current_proof_depth: unit -> int
+
 (* [set_undo (Some n)] sets the size of the ``undo'' stack; [set_undo None]
    sets the size to the default value (12) *)