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

@@ -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

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,46 +210,39 @@ 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
     close_input in_chan input;    (* we must close the file first *)
     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
    Backtrack stack (triggering a save of a frozen state and the generation
    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 ()

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