aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--gramlib/grammar.ml6
-rw-r--r--gramlib/grammar.mli2
-rw-r--r--gramlib/plexing.ml2
-rw-r--r--gramlib/plexing.mli2
-rw-r--r--lib/loc.ml2
-rw-r--r--lib/loc.mli3
-rw-r--r--parsing/cLexer.ml22
-rw-r--r--parsing/cLexer.mli2
-rw-r--r--parsing/pcoq.ml13
-rw-r--r--parsing/pcoq.mli4
-rw-r--r--toplevel/vernac.ml3
-rw-r--r--vernac/vernacentries.ml2
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:59:43 +0000