aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-04 16:26:37 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-04 16:26:37 +0100
commit5003953d45ea0e780cd50bb9d6521799adf18079 (patch)
tree6b784e05f1cc59f291c0cff39f6a94ff51837f4b /toplevel
parentdf9d3a36e71d6d224286811fdc529ad5a955deb7 (diff)
parent893f8a3a3c573ab6b11cc3938cc67ccdc1b6b4ea (diff)
Merge PR #6735: [toplevel] [vernac] Remove Load hack and check / document supported scenarios.
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/vernac.ml28
1 files changed, 9 insertions, 19 deletions
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