From 35961a4ff5a5b8c9b9786cbab0abd279263eb655 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 11 Oct 2016 22:53:56 +0200 Subject: Vernac.ml: inlining read_vernac_file within load_vernac. Also renaming vernac_com into interp_vernac and eval_expr into process_vernac to clarify that it does side-effects (on the contrary of Stm.interp/Vernacentries.interp). --- toplevel/coqloop.ml | 4 ++-- toplevel/vernac.ml | 31 ++++++++++++------------------- toplevel/vernac.mli | 2 +- 3 files changed, 15 insertions(+), 22 deletions(-) (limited to 'toplevel') diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index ea7539fce..f0f8f1864 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -34,7 +34,7 @@ let resize_buffer ibuf = ibuf.str <- nstr (* Delete all irrelevant lines of the input buffer. Keep the last line - in the buffer (useful when there are several commands on the same line. *) + in the buffer (useful when there are several commands on the same line). *) let resynch_buffer ibuf = match ibuf.bols with @@ -299,7 +299,7 @@ let do_vernac () = resynch_buffer top_buffer; try let input = (top_buffer.tokens, None) in - Vernac.eval_expr top_buffer.tokens (read_sentence input) + Vernac.process_expr top_buffer.tokens (read_sentence input) with | End_of_input | CErrors.Quit -> top_stderr (fnl ()); raise CErrors.Quit diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 2e3ea8180..54b2ac3c1 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -185,7 +185,7 @@ let print_cmd_header loc com = Pp.pp_with !Pp_control.std_ft (pp_cmd_header loc com); Format.pp_print_flush !Pp_control.std_ft () -let rec vernac_com po chan_beautify checknav (loc,com) = +let rec interp_vernac po chan_beautify checknav (loc,com) = let interp = function | VernacLoad (verbosely, fname) -> let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in @@ -210,15 +210,18 @@ let rec vernac_com po chan_beautify checknav (loc,com) = if Loc.is_ghost loc' then iraise (reraise, Loc.add_loc info loc) else iraise (reraise, info) -and read_vernac_file verbosely chan_beautify s = - let (in_chan, fname, input) = open_file_twice_if verbosely s in +(* Load a vernac file. CErrors are annotated with file and location *) +and load_vernac verbosely file = + let chan_beautify = + if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout in + let (in_chan, fname, input) = open_file_twice_if verbosely file in try (* we go out of the following infinite loop when a End_of_input is * raised, which means that we raised the end of the file being loaded *) while true do - let loc_ast = parse_sentence input in + let loc_ast = Flags.silently parse_sentence input in CWarnings.set_current_loc (fst loc_ast); - vernac_com (fst input) chan_beautify checknav_simple loc_ast; + Flags.silently (interp_vernac (fst input) chan_beautify checknav_simple) loc_ast; done with any -> (* whatever the exception *) let (e, info) = CErrors.push any in @@ -226,22 +229,12 @@ and read_vernac_file verbosely chan_beautify s = match e with | End_of_input -> if do_beautify () then - pr_new_syntax (fst input) chan_beautify (Loc.make_loc (max_int,max_int)) None + pr_new_syntax (fst input) chan_beautify (Loc.make_loc (max_int,max_int)) None; + if !Flags.beautify_file then close_out chan_beautify; | reraise -> + if !Flags.beautify_file then close_out chan_beautify; iraise (disable_drop e, info) -(* Load a vernac file. CErrors are annotated with file and location *) -and load_vernac verbosely file = - let chan_beautify = - if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout in - try - Flags.silently (read_vernac_file verbosely chan_beautify) file; - if !Flags.beautify_file then close_out chan_beautify; - with any -> - let (e, info) = CErrors.push any in - if !Flags.beautify_file then close_out chan_beautify; - iraise (disable_drop e, info) - (** [eval_expr : ?preserving:bool -> Loc.t * Vernacexpr.vernac_expr -> unit] It executes one vernacular command. By default the command is considered as non-state-preserving, in which case we add it to the @@ -249,7 +242,7 @@ and load_vernac verbosely file = of a new state label). An example of state-preserving command is one coming from the query panel of Coqide. *) -let eval_expr po loc_ast = vernac_com po stdout checknav_deep loc_ast +let process_expr po loc_ast = interp_vernac po stdout checknav_deep loc_ast (* XML output hooks *) let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore () diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index 52216bbfd..c9714f8c9 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -21,7 +21,7 @@ exception End_of_input val just_parsing : bool ref -val eval_expr : Pcoq.Gram.coq_parsable -> Loc.t * Vernacexpr.vernac_expr -> unit +val process_expr : Pcoq.Gram.coq_parsable -> Loc.t * Vernacexpr.vernac_expr -> unit (** Set XML hooks *) val xml_start_library : (unit -> unit) Hook.t -- cgit v1.2.3