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.

6 files changed, 69 insertions, 84 deletions

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index fcee79e07..6dd7cb970 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -2,6 +2,11 @@
 = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 =
 =========================================
 
+** Parsing **
+
+Pcoq.parsable now takes an extra optional filename argument so as to
+bind locations to a file name when relevant.
+
 ** Files **
 
 To avoid clashes with OCaml's compiler libs, the following files were renamed:
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index 0090117f6..cfee77ab2 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -101,14 +101,6 @@ module Error = struct
 end
 open Error
 
-let current_file = ref ""
-
-let get_current_file () =
-  !current_file
-
-let set_current_file ~fname =
-  current_file := fname
-
 let err loc str = Loc.raise (Compat.to_coqloc loc) (Error.E str)
 
 let bad_token str = raise (Error.E (Bad_token str))
@@ -334,6 +326,9 @@ let rec string loc ~comm_level bp len = parser
 (* Hook for exporting comment into xml theory files *)
 let (f_xml_output_comment, xml_output_comment) = Hook.make ~default:ignore ()
 
+(* To associate locations to a file name *)
+let current_file = ref None
+
 (* Utilities for comments in beautify *)
 let comment_begin = ref None
 let comm_loc bp = match !comment_begin with
@@ -354,16 +349,20 @@ let rec split_comments comacc acc pos = function
 
 let extract_comments pos = split_comments [] [] pos !comments
 
-type comments_state = int option * string * bool * ((int * int) * string) list
-let restore_comments_state (o,s,b,c) =
+(* The state of the lexer visible from outside *)
+type lexer_state = int option * string * bool * ((int * int) * string) list * string option
+
+let init_lexer_state f = (None,"",true,[],f)
+let set_lexer_state (o,s,b,c,f) =
   comment_begin := o;
   Buffer.clear current_comment; Buffer.add_string current_comment s;
   between_commands := b;
-  comments := c
-let default_comments_state = (None,"",true,[])
-let comments_state () =
-  let s = (!comment_begin, Buffer.contents current_comment, !between_commands, !comments) in
-  restore_comments_state default_comments_state; s
+  comments := c;
+  current_file := f
+let release_lexer_state () =
+  (!comment_begin, Buffer.contents current_comment, !between_commands, !comments, !current_file)
+let drop_lexer_state () =
+    set_lexer_state (init_lexer_state None)
 
 let real_push_char c = Buffer.add_char current_comment c
 
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index 71edda760..f69d95335 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -10,14 +10,6 @@ val add_keyword : string -> unit
 val remove_keyword : string -> unit
 val is_keyword : string -> bool
 
-(** [get_current_file fname] returns the filename used in locations emitted by
-    the lexer *)
-val get_current_file : unit -> string
-
-(** [set_current_file fname] sets the filename used in locations emitted by the
-    lexer *)
-val set_current_file : fname:string -> unit
-
 val check_ident : string -> unit
 val is_ident : string -> bool
 val check_keyword : string -> unit
diff --git a/parsing/compat.ml4 b/parsing/compat.ml4
index 26e07c2f2..befa0d01b 100644
--- a/parsing/compat.ml4
+++ b/parsing/compat.ml4
@@ -10,6 +10,10 @@
 
 (** Locations *)
 
+let file_loc_of_file = function
+| None -> ""
+| Some f -> f
+
 IFDEF CAMLP5 THEN
 
 module CompatLoc = struct
@@ -29,7 +33,7 @@ let to_coqloc loc =
     Loc.line_nb_last = Ploc.line_nb_last loc;
     Loc.bol_pos_last = Ploc.bol_pos_last loc; }
 
-let make_loc fname line_nb bol_pos bp ep = Ploc.make_loc fname line_nb bol_pos (bp, ep) ""
+let make_loc fname line_nb bol_pos bp ep = Ploc.make_loc (file_loc_of_file fname) line_nb bol_pos (bp, ep) ""
 
 (* Update a loc without allocating an intermediate pair *)
 let set_loc_pos loc bp ep =
@@ -80,7 +84,7 @@ let to_coqloc loc =
     Loc.bol_pos_last = CompatLoc.stop_bol loc; }
 
 let make_loc fname line_nb bol_pos start stop =
-  CompatLoc.of_tuple (fname, line_nb, bol_pos, start, line_nb, bol_pos, stop, false)
+  CompatLoc.of_tuple (file_loc_of_file fname, line_nb, bol_pos, start, line_nb, bol_pos, stop, false)
 
 open CompatLoc
 
@@ -97,7 +101,7 @@ let bump_loc_line_last loc bol_pos =
 	    stop_line loc + 1, bol_pos, stop_off loc, is_ghost loc)
 
 let set_loc_file loc fname =
-  of_tuple (fname, start_line loc, start_bol loc, start_off loc,
+  of_tuple (file_loc_of_file fname, start_line loc, start_bol loc, start_off loc,
 	    stop_line loc, stop_bol loc, stop_off loc, is_ghost loc)
 
 let after loc =
@@ -138,20 +142,22 @@ module type LexerSig = sig
     exception E of t
     val to_string : t -> string
   end
-  type comments_state
-  val default_comments_state : comments_state
-  val comments_state : unit -> comments_state
-  val restore_comments_state : comments_state -> unit
+  type lexer_state
+  val init_lexer_state : string option -> lexer_state
+  val set_lexer_state : lexer_state -> unit
+  val release_lexer_state : unit -> lexer_state
+  val drop_lexer_state : unit -> unit
 end
 
 ELSE
 
 module type LexerSig = sig
   include Camlp4.Sig.Lexer with module Loc = CompatLoc and type Token.t = Tok.t
-  type comments_state
-  val default_comments_state : comments_state
-  val comments_state : unit -> comments_state
-  val restore_comments_state : comments_state -> unit
+  type lexer_state
+  val init_lexer_state : string option -> lexer_state
+  val set_lexer_state : lexer_state -> unit
+  val release_lexer_state : unit -> lexer_state
+  val drop_lexer_state : unit -> unit
 end
 
 END
@@ -172,7 +178,7 @@ module type GrammarSig = sig
   type extend_statment =
       Gramext.position option * single_extend_statment list
   type coq_parsable
-  val parsable : char Stream.t -> coq_parsable
+  val parsable : ?file:string -> char Stream.t -> coq_parsable
   val action : 'a -> action
   val entry_create : string -> 'a entry
   val entry_parse : 'a entry -> coq_parsable -> 'a
@@ -193,32 +199,34 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct
       string option * Gramext.g_assoc option * production_rule list
   type extend_statment =
       Gramext.position option * single_extend_statment list
-  type coq_parsable = parsable * L.comments_state ref
-  let parsable c =
-    let state = ref L.default_comments_state in (parsable c, state)
+  type coq_parsable = parsable * L.lexer_state ref
+  let parsable ?file c =
+    let state = ref (L.init_lexer_state file) in
+    L.set_lexer_state !state;
+    let a = parsable c in
+    state := L.release_lexer_state ();
+    (a,state)
   let action = Gramext.action
   let entry_create = Entry.create
   let entry_parse e (p,state) =
-    L.restore_comments_state !state;
+    L.set_lexer_state !state;
     try
       let c = Entry.parse e p in
-      state := L.comments_state ();
-      L.restore_comments_state L.default_comments_state;
+      state := L.release_lexer_state ();
       c
     with Exc_located (loc,e) ->
-      L.restore_comments_state L.default_comments_state;
+      L.drop_lexer_state ();
       let loc' = Loc.get_loc (Exninfo.info e) in
       let loc = match loc' with None -> to_coqloc loc | Some loc -> loc in
       Loc.raise loc e
   let with_parsable (p,state) f x =
-    L.restore_comments_state !state;
+    L.set_lexer_state !state;
     try
       let a = f x in
-      state := L.comments_state ();
-      L.restore_comments_state L.default_comments_state;
+      state := L.release_lexer_state ();
       a
     with e ->
-      L.restore_comments_state L.default_comments_state;
+      L.drop_lexer_state ();
       raise e
 
   let entry_print ft x = Entry.print ft x
@@ -234,7 +242,7 @@ module type GrammarSig = sig
   type 'a entry = 'a Entry.t
   type action = Action.t
   type coq_parsable
-  val parsable : char Stream.t -> coq_parsable
+  val parsable : ?file:string -> char Stream.t -> coq_parsable
   val action : 'a -> action
   val entry_create : string -> 'a entry
   val entry_parse : 'a entry -> coq_parsable -> 'a
@@ -249,31 +257,28 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct
   include Camlp4.Struct.Grammar.Static.Make (L)
   type 'a entry = 'a Entry.t
   type action = Action.t
-  type comments_state = int option * string * bool * ((int * int) * string) list
-  type coq_parsable = char Stream.t * L.comments_state ref
-  let parsable s = let state = ref L.default_comments_state in (s, state)
+  type coq_parsable = char Stream.t * L.lexer_state ref
+  let parsable ?file s = let state = ref (L.init_lexer_state file) in (s, state)
   let action = Action.mk
   let entry_create = Entry.mk
   let entry_parse e (s,state) =
-    L.restore_comments_state !state;
+    L.set_lexer_state !state;
     try
       let c = parse e (*FIXME*)CompatLoc.ghost s in
-      state := L.comments_state ();
-      L.restore_comments_state L.default_comments_state;
+      state := L.release_lexer_state ();
       c
     with Exc_located (loc,e) ->
-      L.restore_comments_state L.default_comments_state;
-      raise_coq_loc loc e
+      L.drop_lexer_state ();
+      raise_coq_loc loc e;;
   let with_parsable (p,state) f x =
-    L.restore_comments_state !state;
+    L.set_lexer_state !state;
     try
       let a = f x in
-      state := L.comments_state ();
-      L.restore_comments_state L.default_comments_state;
+      state := L.release_lexer_state ();
       a
     with e ->
-      L.restore_comments_state L.default_comments_state;
-      Pervasives.raise e
+      L.drop_lexer_state ();
+      Pervasives.raise e;;
   let entry_print ft x = Entry.print ft x
   let srules' = srules (entry_create "dummy")
 end
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 -> ()