More on making the lexer more functional (continuing b8ae2de5 and

8a8caba3).

- Adding cLexer.current_file to the lexer state, i.e. making it a
  component of the type "coq_parsable" of lexer state (it was
  forgotten in b8ae2de5 and 8a8caba3).
- Inlining save_translator/restore_translator which have now lost most
  of their substance.

2 files changed, 8 insertions, 24 deletions

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 661a597ae..f03f31178 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -81,7 +81,7 @@ let open_file_twice_if verbosely longfname =
   let in_chan = open_utf8_file_in longfname in
   let verb_ch =
     if verbosely then Some (open_utf8_file_in longfname) else None in
-  let po = Pcoq.Gram.parsable (Stream.of_channel in_chan) in
+  let po = Pcoq.Gram.parsable ~file:longfname (Stream.of_channel in_chan) in
   (in_chan, longfname, (po, verb_ch))
 
 let close_input in_chan (_,verb) =
@@ -145,13 +145,6 @@ let pr_new_syntax (po,_) loc ocom =
   (* Reinstall the context of parsing which includes the bindings of comments to locations *)
   Pcoq.Gram.with_parsable po (pr_new_syntax_in_context loc) ocom
 
-let save_translator () =
-  !chan_beautify
-
-let restore_translator ch =
-  if !Flags.beautify_file then close_out !chan_beautify;
-  chan_beautify := ch
-
 (* For coqtop -time, we display the position in the file,
    and a glimpse of the executed command *)
 
@@ -186,22 +179,17 @@ let rec vernac_com input checknav (loc,com) =
 	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
-	let st = save_translator () in
-        let old_lexer_file = CLexer.get_current_file () in
-        CLexer.set_current_file f;
-	if !Flags.beautify_file then
-	  begin
-	    chan_beautify := open_out (f^beautify_suffix);
-          end;
+	let ch = !chan_beautify in
+	if !Flags.beautify_file then chan_beautify := open_out (f^beautify_suffix);
 	begin
 	  try
             Flags.silently (read_vernac_file verbosely) f;
-	    restore_translator st;
-            CLexer.set_current_file old_lexer_file;
+            if !Flags.beautify_file then close_out !chan_beautify;
+            chan_beautify := ch;
 	  with reraise ->
             let reraise = CErrors.push reraise in
-	    restore_translator st;
-            CLexer.set_current_file old_lexer_file;
+            if !Flags.beautify_file then close_out !chan_beautify;
+            chan_beautify := ch;
 	    iraise reraise
 	end
 
@@ -269,16 +257,12 @@ let (f_xml_end_library, xml_end_library) = Hook.make ~default:ignore ()
 let load_vernac verb file =
   chan_beautify :=
     if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout;
-    let old_lexer_file = CLexer.get_current_file () in
   try
-    CLexer.set_current_file file;
     Flags.silently (read_vernac_file verb) file;
     if !Flags.beautify_file then close_out !chan_beautify;
-    CLexer.set_current_file old_lexer_file;
   with any ->
     let (e, info) = CErrors.push any in
     if !Flags.beautify_file then close_out !chan_beautify;
-    CLexer.set_current_file old_lexer_file;
     iraise (disable_drop e, info)
 
 let warn_file_no_extension =
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index feec23b50..df83f7685 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1813,7 +1813,7 @@ let vernac_load interp fname =
   let input =
     let longfname = Loadpath.locate_file fname in
     let in_chan = open_utf8_file_in longfname in
-    Pcoq.Gram.parsable (Stream.of_channel in_chan) in
+    Pcoq.Gram.parsable ~file:longfname (Stream.of_channel in_chan) in
   try while true do interp (snd (parse_sentence input)) done
   with End_of_input -> ()