diff options
| author | Hugo Herbelin | 2014-08-11 12:39:36 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-08-12 13:37:13 +0200 |
| commit | eec197a86c37b0298fd551c0e5de23ac0c276f66 (patch) | |
| tree | dbe5c18243dcea67180253809a31b3198b472498 | |
| parent | c48ade3f0d6324872d292932e797ffd718ad57d9 (diff) | |
Fixing parsing of bullets after a "...".
The lexer parses bullets only at the beginning of sentence. In
particular, the lexer recognizes sentences (this feature was
introduced for the translator and it is still used for the
beautifier). It recognized "." but not "...'. I added "..." followed
by space or eol as a terminator of sentences. I hope this is
compatible with the rest of the code dealing with end of
sentences.
Fixed also parse_to_dot which was not aware of "...".
Maybe there are similar things to do with coqide or PG?
| -rw-r--r-- | parsing/lexer.ml4 | 2 | ||||
| -rw-r--r-- | toplevel/coqloop.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 88590fa4af..13f8359516 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -501,7 +501,7 @@ let rec next_token = parser bp (* We enforce that "." should either be part of a larger keyword, for instance ".(", or followed by a blank or eof. *) let () = match t with - | KEYWORD "." -> + | KEYWORD ("." | "...") -> if not (blank_or_eof s) then err (bp,ep+1) Undefined_token; between_com := true; | _ -> () diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 07a398903c..de2a81b7c9 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -270,7 +270,7 @@ let print_toplevel_error e = (* Read the input stream until a dot is encountered *) let parse_to_dot = let rec dot st = match Compat.get_tok (Stream.next st) with - | Tok.KEYWORD "." -> () + | Tok.KEYWORD ("."|"...") -> () | Tok.EOI -> raise End_of_input | _ -> dot st in |