diff options
| author | Emilio Jesus Gallego Arias | 2019-02-19 18:06:10 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-02-19 18:06:10 +0100 |
| commit | 6e3850ce5092d5cb432ef917ae6ee79225089f6a (patch) | |
| tree | b3a007d270b5824ed4a3c98e16acbc675b60aa35 | |
| parent | 5f26707db8b78e580801aa7565539fc2a8f0a76a (diff) | |
| parent | 12da73e84897fa17a6ab00e251022339ae36a806 (diff) | |
Merge PR #9604: Gramlib: Fixes #9358 (ensuring that requested locations are effectively computed at lexing time)
Reviewed-by: ejgallego
| -rw-r--r-- | gramlib/grammar.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index e313f2e648..f46ddffd6e 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -1368,6 +1368,9 @@ let parse_parsable entry p = let get_loc () = try let cnt = Stream.count ts in + (* Ensure that the token at location cnt has been peeked so that + the location function knows about it *) + let _ = Stream.peek ts in let loc = fun_loc cnt in if !token_count - 1 <= cnt then loc else Loc.merge loc (fun_loc (!token_count - 1)) |