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

1 files changed, 20 insertions, 22 deletions

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