From eec197a86c37b0298fd551c0e5de23ac0c276f66 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 11 Aug 2014 12:39:36 +0200
Subject: 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?
---
 parsing/lexer.ml4   | 2 +-
 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
-- 
cgit v1.2.3