[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.

4 files changed, 19 insertions, 22 deletions

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