Re-allow Reset in compiled files

 This was a wish by A. Chlipala on coq-club

 Both Reset foo and Reset Initial are accepted (with a warning).
 If some proofs were opened, all of them are aborted. This isn't the
 behavior of the interactive Reset that has more information and can
 be more selective, but this shouldn't be a big issue in practice.

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

5 files changed, 41 insertions, 6 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 40cf0d06d..043d2097b 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -938,8 +938,8 @@ GEXTEND Gram
       | IDENT "Restore"; IDENT "State"; s = ne_string -> VernacRestoreState s
 
 (* Resetting *)
-      | IDENT "Reset"; id = identref -> VernacResetName id
       | IDENT "Reset"; IDENT "Initial" -> VernacResetInitial
+      | IDENT "Reset"; id = identref -> VernacResetName id
       | IDENT "Back" -> VernacBack 1
       | IDENT "Back"; n = natural -> VernacBack n
       | IDENT "BackTo"; n = natural -> VernacBackTo n
diff --git a/toplevel/backtrack.ml b/toplevel/backtrack.ml
index d0f258fbf..fb25be7c1 100644
--- a/toplevel/backtrack.ml
+++ b/toplevel/backtrack.ml
@@ -40,6 +40,11 @@ type info = {
 
 let history : info Stack.t = Stack.create ()
 
+(** Is this stack active (i.e. nonempty) ?
+    The stack is currently inactive when compiling files (coqc). *)
+
+let is_active () = not (Stack.is_empty history)
+
 (** For debug purpose, a dump of the history *)
 
 let dump_history () =
diff --git a/toplevel/backtrack.mli b/toplevel/backtrack.mli
index 0b9325bd6..80c1d0a10 100644
--- a/toplevel/backtrack.mli
+++ b/toplevel/backtrack.mli
@@ -19,6 +19,11 @@
 
 val mark_command : Vernacexpr.vernac_expr -> unit
 
+(** Is this history stack active (i.e. nonempty) ?
+    The stack is currently inactive when compiling files (coqc). *)
+
+val is_active : unit -> bool
+
 (** The [Invalid] exception is raised when one of the following function
     tries to empty the history stack, or reach an unknown states, etc.
     The stack is preserved in these cases. *)
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index c2446032d..6bc544aaa 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -41,6 +41,12 @@ and is_deep_navigation_vernac = function
   | VernacList l -> List.exists (fun (_,c) -> is_navigation_vernac c) l
   | _ -> false
 
+(* NB: Reset is now allowed again as asked by A. Chlipala *)
+
+let is_reset = function
+  | VernacResetInitial | VernacResetName _ -> true
+  | _ -> false
+
 (* Specifies which file is read. The intermediate file names are
    discarded here. The Drop exception becomes an error. We forget
    if the error ocurred during interpretation or not *)
@@ -289,7 +295,7 @@ and read_vernac_file verbosely s =
     else Flags.silently Vernacentries.interp
   in
   let checknav loc cmd =
-    if is_navigation_vernac cmd then
+    if is_navigation_vernac cmd && not (is_reset cmd) then
 	user_error loc "Navigation commands forbidden in files"
   in
   let (in_chan, fname, input) =
@@ -299,6 +305,7 @@ and read_vernac_file verbosely s =
      * raised, which means that we raised the end of the file being loaded *)
     while true do
       vernac_com interpfun checknav (parse_sentence input);
+      Lib.mark_end_of_command();
       pp_flush ()
     done
   with e ->   (* whatever the exception *)
@@ -353,6 +360,7 @@ let compile verbosely f =
   Dumpglob.start_dump_glob long_f_dot_v;
   Dumpglob.dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n");
   if !Flags.xml_export then !xml_start_library ();
+  Lib.mark_end_of_command ();
   let _ = load_vernac verbosely long_f_dot_v in
   if Pfedit.get_all_proof_names () <> [] then
     (pperrnl (str "Error: There are pending proofs"); flush_all (); exit 1);
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d4cacf68b..7843d10b4 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1445,10 +1445,27 @@ let vernac_back n =
   with Backtrack.Invalid -> error "Invalid backtrack."
 
 let vernac_reset_name id =
-  try Backtrack.reset_name id; try_print_subgoals ()
-  with Backtrack.Invalid -> error "Invalid Reset."
-
-let vernac_reset_initial () = Backtrack.reset_initial ()
+  try
+    if Backtrack.is_active () then
+      (Backtrack.reset_name id; try_print_subgoals ())
+    else
+      (* When compiling files, Reset is now allowed again
+	 as asked by A. Chlipala. we emulate a simple reset,
+	 that discards all proofs. *)
+      let lbl = Lib.label_before_name id in
+      Pfedit.delete_all_proofs ();
+      Pp.msg_warning (str "Reset occured during compilation.");
+      Lib.reset_label lbl
+  with Backtrack.Invalid | Not_found -> error "Invalid Reset."
+
+
+let vernac_reset_initial () =
+  if Backtrack.is_active () then
+    Backtrack.reset_initial ()
+  else begin
+    Pp.msg_warning (str "Reset occured during compilation.");
+    Lib.reset_label Lib.first_command_label
+  end
 
 (* For compatibility with ProofGeneral: *)