[parser] initialization based on Loc.t rather than Loc.source

In this way one can also set the current offsets in a file,
useful if you are parsing a Coq fragment within a file instead
of a full file starting from the first line.

12 files changed, 33 insertions, 30 deletions

diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index f46ddffd6e..74350c4f15 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -15,7 +15,7 @@ module type S =
   sig
     type te
     type parsable
-    val parsable : char Stream.t -> parsable
+    val parsable : ?loc:Loc.t -> char Stream.t -> parsable
     val tokens : string -> (string * int) list
     module Entry :
       sig
@@ -1398,8 +1398,8 @@ let clear_entry e =
     Dlevels _ -> e.edesc <- Dlevels []
   | Dparser _ -> ()
 
-    let parsable cs =
-      let (ts, lf) = L.lexer.Plexing.tok_func cs in
+    let parsable ?loc cs =
+      let (ts, lf) = L.lexer.Plexing.tok_func ?loc cs in
       {pa_chr_strm = cs; pa_tok_strm = ts; pa_loc_func = lf}
     module Entry =
       struct
diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli
index bde07ddc48..7cb7a92f85 100644
--- a/gramlib/grammar.mli
+++ b/gramlib/grammar.mli
@@ -23,7 +23,7 @@ module type S =
   sig
     type te
     type parsable
-    val parsable : char Stream.t -> parsable
+    val parsable : ?loc:Loc.t -> char Stream.t -> parsable
     val tokens : string -> (string * int) list
     module Entry :
       sig
diff --git a/gramlib/plexing.ml b/gramlib/plexing.ml
index fce5445ad8..c294923a85 100644
--- a/gramlib/plexing.ml
+++ b/gramlib/plexing.ml
@@ -5,7 +5,7 @@
 type pattern = string * string
 
 type location_function = int -> Loc.t
-type 'te lexer_func = char Stream.t -> 'te Stream.t * location_function
+type 'te lexer_func = ?loc:Loc.t -> char Stream.t -> 'te Stream.t * location_function
 
 type 'te lexer =
   { tok_func : 'te lexer_func;
diff --git a/gramlib/plexing.mli b/gramlib/plexing.mli
index 6139dc4020..f6e4d96b80 100644
--- a/gramlib/plexing.mli
+++ b/gramlib/plexing.mli
@@ -28,7 +28,7 @@ type 'te lexer =
     tok_match : pattern -> 'te -> string;
     tok_text : pattern -> string;
   }
-and 'te lexer_func = char Stream.t -> 'te Stream.t * location_function
+and 'te lexer_func = ?loc:Loc.t -> char Stream.t -> 'te Stream.t * location_function
 and location_function = int -> Loc.t
   (** The type of a function giving the location of a token in the
       source from the token number in the stream (starting from zero). *)
diff --git a/lib/loc.ml b/lib/loc.ml
index 66b7a7da70..6bcdcc0341 100644
--- a/lib/loc.ml
+++ b/lib/loc.ml
@@ -29,6 +29,8 @@ let create fname line_nb bol_pos bp ep = {
   line_nb_last = line_nb; bol_pos_last = bol_pos; bp = bp; ep = ep;
 }
 
+let initial source = create source 1 0 0 0
+
 let make_loc (bp, ep) = {
   fname = ToplevelInput; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0;
   bp = bp; ep = ep;
diff --git a/lib/loc.mli b/lib/loc.mli
index 23df1ebd9a..1eb3cc49e8 100644
--- a/lib/loc.mli
+++ b/lib/loc.mli
@@ -32,6 +32,9 @@ val create : source -> int -> int -> int -> int -> t
 (** Create a location from a filename, a line number, a position of the
     beginning of the line, a start and end position *)
 
+val initial : source -> t
+(** Create a location corresponding to the beginning of the given source *)
+
 val unloc : t -> int * int
 (** Return the start and end position of a location *)
 
diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml
index 49d6cf01d9..503cfcdb4f 100644
--- a/parsing/cLexer.ml
+++ b/parsing/cLexer.ml
@@ -383,9 +383,6 @@ let rec string loc ~comm_level bp len s = match Stream.peek s with
      let loc = set_loc_pos loc bp ep in
      err loc Unterminated_string
 
-(* To associate locations to a file name *)
-let current_file = ref Loc.ToplevelInput
-
 (* Utilities for comments in beautify *)
 let comment_begin = ref None
 let comm_loc bp = match !comment_begin with
@@ -397,21 +394,20 @@ let current_comment = Buffer.create 8192
 let between_commands = ref true
 
 (* The state of the lexer visible from outside *)
-type lexer_state = int option * string * bool * ((int * int) * string) list * Loc.source
+type lexer_state = int option * string * bool * ((int * int) * string) list
 
-let init_lexer_state f = (None,"",true,[],f)
-let set_lexer_state (o,s,b,c,f) =
+let init_lexer_state () = (None,"",true,[])
+let set_lexer_state (o,s,b,c) =
   comment_begin := o;
   Buffer.clear current_comment; Buffer.add_string current_comment s;
   between_commands := b;
-  comments := c;
-  current_file := f
+  comments := c
 let get_lexer_state () =
-  (!comment_begin, Buffer.contents current_comment, !between_commands, !comments, !current_file)
+  (!comment_begin, Buffer.contents current_comment, !between_commands, !comments)
 let drop_lexer_state () =
-    set_lexer_state (init_lexer_state Loc.ToplevelInput)
+    set_lexer_state (init_lexer_state ())
 
-let get_comment_state (_,_,_,c,_) = c
+let get_comment_state (_,_,_,c) = c
 
 let real_push_char c = Buffer.add_char current_comment c
 
@@ -754,9 +750,9 @@ let token_text = function
   | (con, "") -> con
   | (con, prm) -> con ^ " \"" ^ prm ^ "\""
 
-let func next_token cs =
+let func next_token ?loc cs =
   let loct = loct_create () in
-  let cur_loc = ref (Loc.create !current_file 1 0 0 0) in
+  let cur_loc = ref (Option.default Loc.(initial ToplevelInput) loc) in
   let ts =
     Stream.from
       (fun i ->
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index af3fd7f318..807f37a1a4 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -51,7 +51,7 @@ end
 (* Mainly for comments state, etc... *)
 type lexer_state
 
-val init_lexer_state : Loc.source -> lexer_state
+val init_lexer_state : unit -> lexer_state
 val set_lexer_state : lexer_state -> unit
 val get_lexer_state : unit -> lexer_state
 val drop_lexer_state : unit -> unit
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 759e60fbca..9241205755 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -59,7 +59,7 @@ module type S =
 
   type coq_parsable
 
-  val coq_parsable : ?file:Loc.source -> char Stream.t -> coq_parsable
+  val coq_parsable : ?loc:Loc.t -> char Stream.t -> coq_parsable
   val entry_create : string -> 'a entry
   val entry_parse : 'a entry -> coq_parsable -> 'a
 
@@ -71,10 +71,10 @@ end with type 'a Entry.e = 'a Extend.entry = struct
 
   type coq_parsable = parsable * CLexer.lexer_state ref
 
-  let coq_parsable ?(file=Loc.ToplevelInput) c =
-    let state = ref (CLexer.init_lexer_state file) in
+  let coq_parsable ?loc c =
+    let state = ref (CLexer.init_lexer_state ()) in
     CLexer.set_lexer_state !state;
-    let a = parsable c in
+    let a = parsable ?loc c in
     state := CLexer.get_lexer_state ();
     (a,state)
 
@@ -320,8 +320,9 @@ let map_entry f en =
 (* Parse a string, does NOT check if the entire string was read
    (use eoi_entry) *)
 
-let parse_string f x =
-  let strm = Stream.of_string x in Gram.entry_parse f (Gram.coq_parsable strm)
+let parse_string f ?loc x =
+  let strm = Stream.of_string x in
+  Gram.entry_parse f (Gram.coq_parsable ?loc strm)
 
 type gram_universe = string
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 3203a25b46..0418249e42 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -19,7 +19,7 @@ open Libnames
 module Parsable :
 sig
   type t
-  val make : ?file:Loc.source -> char Stream.t -> t
+  val make : ?loc:Loc.t -> char Stream.t -> t
   (* Get comment parsing information from the Lexer *)
   val comment_state : t -> ((int * int) * string) list
 end
@@ -121,7 +121,7 @@ end
 
 (** Parse a string *)
 
-val parse_string : 'a Entry.t -> string -> 'a
+val parse_string : 'a Entry.t -> ?loc:Loc.t -> string -> 'a
 val eoi_entry : 'a Entry.t -> 'a Entry.t
 val map_entry : ('a -> 'b) -> 'a Entry.t -> 'b Entry.t
 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index ce584f1109..038ff54bf6 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -91,7 +91,8 @@ let load_vernac_core ~echo ~check ~interactive ~state file =
   let input_cleanup () = close_in in_chan; Option.iter close_in in_echo in
 
   let in_pa =
-    Pcoq.Parsable.make ~file:(Loc.InFile file) (Stream.of_channel in_chan) in
+    Pcoq.Parsable.make ~loc:(Loc.initial (Loc.InFile file))
+      (Stream.of_channel in_chan) in
   let open State in
 
   (* ids = For beautify, list of parsed sids *)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 91965e56b1..d2ba882521 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2175,7 +2175,7 @@ let vernac_load ~st interp fname =
   let input =
     let longfname = Loadpath.locate_file fname in
     let in_chan = open_utf8_file_in longfname in
-    Pcoq.Parsable.make ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in
+    Pcoq.Parsable.make ~loc:(Loc.initial (Loc.InFile longfname)) (Stream.of_channel in_chan) in
   let rec load_loop ~pstate =
     try
       let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) pstate in