diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/lexer.ml4 | 12 | ||||
| -rw-r--r-- | parsing/lexer.mli | 7 |
2 files changed, 15 insertions, 4 deletions
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 95bd57ce67..6424cb3d9c 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -487,8 +487,10 @@ let loct_add loct i loc = end; !loct.(i) <- Some loc -let current_location_function = - ref (fun _ -> failwith "No location function is set") +let current_location_table = ref (ref [||]) + +let location_function n = + loct_func !current_location_table n let func cs = let loct = loct_create () in @@ -498,9 +500,13 @@ let func cs = let (tok, loc) = next_token cs in loct_add loct i loc; Some tok) in - current_location_function := loct_func loct; + current_location_table := loct; (ts, loct_func loct) +type location_table = (int * int) option array ref +let location_table () = !current_location_table +let restore_location_table t = current_location_table := t + (* Names of tokens, for this lexer, used in Grammar error messages *) let token_text = function diff --git a/parsing/lexer.mli b/parsing/lexer.mli index f1a97a163e..b44e62eb91 100644 --- a/parsing/lexer.mli +++ b/parsing/lexer.mli @@ -23,7 +23,12 @@ val add_keyword : string -> unit val is_keyword : string -> bool val func : char Stream.t -> (string * string) Stream.t * (int -> int * int) -val current_location_function : (int -> int * int) ref +val location_function : int -> int * int + +(* for coqdoc *) +type location_table +val location_table : unit -> location_table +val restore_location_table : location_table -> unit val check_ident : string -> unit val check_special_token : string -> unit |