aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/toplevel.mllib
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-03-23 16:49:52 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-03-23 16:49:52 +0000
commit85a16702cc7561f9a96eed9c2d707b9711130f09 (patch)
tree76acae0330eb6ddf125f48e7f1c5994d24b05296 /toplevel/toplevel.mllib
parent5c915de161fe453914525e5920d1a165bba8fa43 (diff)
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
Diffstat (limited to 'toplevel/toplevel.mllib')
-rw-r--r--toplevel/toplevel.mllib1
1 files changed, 1 insertions, 0 deletions
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