diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.ml | 15 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 8 |
2 files changed, 23 insertions, 0 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index bbcda792f0..f724589f69 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 b0aacd86c8..eca13c56cb 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) *) |