diff options
| author | Hugo Herbelin | 2019-02-19 15:04:30 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-02-19 15:09:51 +0100 |
| commit | 12da73e84897fa17a6ab00e251022339ae36a806 (patch) | |
| tree | 405839dc3c31b4bb07ea673efa56a5e6c0c7650e | |
| parent | 7c62153610f54a96cdded0455af0fff7ff91a53a (diff) | |
Gramlib: Fixes #9358 (ensuring that the loc function has something to compute).
| -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)) |