diff options
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 5 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 28 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 12 |
3 files changed, 24 insertions, 21 deletions
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 1cd23c929..bef31d3fa 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -513,6 +513,9 @@ This command loads the file named {\ident}{\tt .v}, searching successively in each of the directories specified in the {\em loadpath}. (see Section~\ref{loadpath}) +Files loaded this way cannot leave proofs open, and neither the {\tt + Load} command can be use inside a proof. + \begin{Variants} \item {\tt Load {\str}.}\label{Load-str}\\ Loads the file denoted by the string {\str}, where {\str} is any @@ -530,6 +533,8 @@ successively in each of the directories specified in the {\em \begin{ErrMsgs} \item \errindex{Can't find file {\ident} on loadpath} +\item \errindex{Load is not supported inside proofs} +\item \errindex{Files processed by Load cannot leave open proofs} \end{ErrMsgs} \section[Compiled files]{Compiled files\label{compiled}\index{Compiled files}} diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 92dee84f3..a84990f91 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -120,16 +120,9 @@ module State = struct end -let rec interp_vernac ~time ~check ~interactive ~state (loc,com) = +let interp_vernac ~time ~check ~interactive ~state (loc,com) = let open State in - let interp v = - match under_control v with - | VernacLoad (verbosely, fname) -> - let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in - let fname = CUnix.make_suffix fname ".v" in - let f = Loadpath.locate_file fname in - load_vernac ~time ~verbosely ~check ~interactive ~state f - | _ -> + try (* XXX: We need to run this before add as the classification is highly dynamic and depends on the structure of the document. Hopefully this is fixed when VtMeta can be removed @@ -139,13 +132,17 @@ let rec interp_vernac ~time ~check ~interactive ~state (loc,com) = against that... *) let wflags = CWarnings.get_flags () in CWarnings.set_flags "none"; - let is_proof_step = match fst (Vernac_classifier.classify_vernac v) with + let is_proof_step = match fst (Vernac_classifier.classify_vernac com) with | VtProofStep _ | VtMeta | VtStartProof _ -> true | _ -> false in CWarnings.set_flags wflags; - let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) (loc,v) in + (* The -time option is only supported from console-based + clients due to the way it prints. *) + if time then print_cmd_header ?loc com; + let com = if time then VernacTime(time,(CAst.make ?loc com)) else com in + let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) (loc,com) in (* Main STM interaction *) if ntip <> `NewTip then @@ -165,13 +162,6 @@ let rec interp_vernac ~time ~check ~interactive ~state (loc,com) = if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ()); let new_proof = Proof_global.give_me_the_proof_opt () in { doc = ndoc; sid = nsid; proof = new_proof } - in - try - (* The -time option is only supported from console-based - clients due to the way it prints. *) - if time then print_cmd_header ?loc com; - let com = if time then VernacTime(time, CAst.make ?loc com) else com in - interp com with reraise -> (* XXX: In non-interactive mode edit_at seems to do very weird things, so we better avoid it while we investigate *) @@ -184,7 +174,7 @@ let rec interp_vernac ~time ~check ~interactive ~state (loc,com) = end in iraise (reraise, info) (* Load a vernac file. CErrors are annotated with file and location *) -and load_vernac ~time ~verbosely ~check ~interactive ~state file = +let load_vernac ~time ~verbosely ~check ~interactive ~state file = let ft_beautify, close_beautify = if !Flags.beautify_file then let chan_beautify = open_out (file^beautify_suffix) in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 4613100fc..89fd2b641 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1926,6 +1926,8 @@ exception End_of_input without a considerable amount of refactoring. *) let vernac_load interp fname = + if Proof_global.there_are_pending_proofs () then + CErrors.user_err Pp.(str "Load is not supported inside proofs."); let interp x = let proof_mode = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"] in Proof_global.activate_proof_mode proof_mode [@ocaml.warning "-3"]; @@ -1942,8 +1944,13 @@ let vernac_load interp fname = let longfname = Loadpath.locate_file fname in let in_chan = open_utf8_file_in longfname in Pcoq.Gram.parsable ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in - try while true do interp (snd (parse_sentence input)) done - with End_of_input -> () + begin + try while true do interp (snd (parse_sentence input)) done + with End_of_input -> () + end; + (* If Load left a proof open, we fail too. *) + if Proof_global.there_are_pending_proofs () then + CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs.") (* "locality" is the prefix "Local" attribute, while the "local" component * is the outdated/deprecated "Local" attribute of some vernacular commands @@ -1954,6 +1961,7 @@ let interp ?proof ~atts ~st c = vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c); match c with + (* Loading a file requires access to the control interpreter *) | VernacLoad _ -> assert false (* The STM should handle that, but LOAD bypasses the STM... *) |