diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-01-21 17:36:15 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-01-21 17:36:15 +0000 |
| commit | bd9e36c180f5fce1c932179998cd981583e08f77 (patch) | |
| tree | 7e112616ee9c142f6ce93ac700e06dd101c2481e | |
| parent | ade973ca732d8ae140812cb1041544c3e7ca640a (diff) | |
Export information des references et location de notations pour coqdoc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5228 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/lexer.ml4 | 4 | ||||
| -rw-r--r-- | parsing/lexer.mli | 1 |
2 files changed, 5 insertions, 0 deletions
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 61f28469c..95bd57ce6 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -487,6 +487,9 @@ let loct_add loct i loc = end; !loct.(i) <- Some loc +let current_location_function = + ref (fun _ -> failwith "No location function is set") + let func cs = let loct = loct_create () in let ts = @@ -495,6 +498,7 @@ let func cs = let (tok, loc) = next_token cs in loct_add loct i loc; Some tok) in + current_location_function := loct_func loct; (ts, loct_func loct) (* Names of tokens, for this lexer, used in Grammar error messages *) diff --git a/parsing/lexer.mli b/parsing/lexer.mli index a32ca355d..f1a97a163 100644 --- a/parsing/lexer.mli +++ b/parsing/lexer.mli @@ -23,6 +23,7 @@ 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 check_ident : string -> unit val check_special_token : string -> unit |