From 66483fbbb6549bc57bd409c689ee7d99e4d45d9d Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 11 Jul 2012 16:50:17 +0000 Subject: 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 --- parsing/g_vernac.ml4 | 2 +- toplevel/backtrack.ml | 5 +++++ toplevel/backtrack.mli | 5 +++++ toplevel/vernac.ml | 10 +++++++++- toplevel/vernacentries.ml | 25 +++++++++++++++++++++---- 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: *) -- cgit v1.2.3