diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-11 23:26:10 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-02-28 18:14:54 +0100 |
| commit | f5abd069a86b85829ab49141d27ef7633f4b84a1 (patch) | |
| tree | f8855946b56d03188a6415e81cbf94cdde2ae0b2 /vernac | |
| parent | f726e860917b56abc94f21d9d5add7594d23bb6d (diff) | |
[toplevel] [vernac] Remove Load hack and check supported scenarios.
Parsing in `VernacLoad` was broken for a while, but the situation has
improved by miscellaneous refactoring.
However, we still cannot support `Load` properly when proofs are
crossing file boundaries. So in this patch we do two things:
- We check for supported scenarios [no proofs open at `Load` entry/exit]
- Remove the hack in `toplevel` so the behavior of `Load` is
consistent between `coqide`/`coqc`.
We close #5053 as its main bug was fixed by the main toplevel
refactoring and the remaining cases are documented now.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 12 |
1 files changed, 10 insertions, 2 deletions
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... *) |