diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-23 18:16:21 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-23 18:16:21 +0000 |
| commit | 7c56058bad50c783a24bfa2d7adf5e257198303a (patch) | |
| tree | b7d838436c6b9eb7f7db778a5e506c6c93f4287f /toplevel | |
| parent | a672da543ac5ba589abb016e8f1cd8e448326fc3 (diff) | |
Fix issues with "Reset Initial" in scripts given to coqtop -l
Doing coqtop -l on a file starting with Reset Initial used to fail.
To avoid that, we now always place an initial DOT in the libstack.
Backtrack.reset_initial has been adapted accordingly: during an
interactive session following a Load via coqtop -l (or .coqrc),
a Reset Initial will bring back at the start of the interactive
session, *not* undoing the initial Load.
Note : Reset Initial might hence not be equivalent anymore to BackTo 1.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16449 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/backtrack.ml | 24 | ||||
| -rw-r--r-- | toplevel/backtrack.mli | 4 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
3 files changed, 11 insertions, 19 deletions
diff --git a/toplevel/backtrack.ml b/toplevel/backtrack.ml index 1954d1682..e259da7af 100644 --- a/toplevel/backtrack.ml +++ b/toplevel/backtrack.ml @@ -179,25 +179,15 @@ let backtrack snum pnum naborts = (** [reset_initial] resets the system and clears the command history stack, only pushing back the initial entry. It should be equivalent - to [backto Lib.first_command_label], but sligthly more efficient. *) + to [backto n0] where [n0] is the first label stored in the history. + Note that there might be other labels before [n0] in the libstack, + created during evaluation of .coqrc or initial Load's. *) let reset_initial () = - let init_label = Lib.first_command_label in - if Int.equal (Lib.current_command_label ()) init_label then () - else begin - Pfedit.delete_all_proofs (); - Lib.reset_label init_label; - Stack.clear history; - Stack.push - { label = init_label; - nproofs = 0; - prfname = None; - prfdepth = 0; - ngoals = 0; - reachable = true; - cmd = VernacNop } - history - end + let n = Stack.length history in + npop (n-1); + Pfedit.delete_all_proofs (); + Lib.reset_label (top ()).label (** Reset to the last known state just before defining [id] *) diff --git a/toplevel/backtrack.mli b/toplevel/backtrack.mli index 5f9e9f98c..d4ac7cc61 100644 --- a/toplevel/backtrack.mli +++ b/toplevel/backtrack.mli @@ -60,7 +60,9 @@ val backtrack : int -> int -> int -> unit (** [reset_initial] resets the system and clears the command history stack, only pushing back the initial entry. It should be equivalent - to [backto Lib.first_command_label], but sligthly more efficient. *) + to [backto n0] where [n0] is the first label stored in the history. + Note that there might be other labels before [n0] in the libstack, + created during evaluation of .coqrc or initial Load's. *) val reset_initial : unit -> unit diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 498c653ab..18b5e8029 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1582,7 +1582,7 @@ let vernac_reset_initial () = Backtrack.reset_initial () else begin Pp.msg_warning (str "Reset command occurred in non-interactive mode."); - Lib.reset_label Lib.first_command_label + Lib.raw_reset_initial () end (* For compatibility with ProofGeneral: *) |