In coqtop, a terminating "." must now be followed by a blank or eof.

 This way, we forbid contiguous sentences like "tac.{tac.}", which
 should now be written with at least 2 spaces: "tac. {tac. }"

 This should avoid confusion if a user declare a notation involving
 ".{" or ".}" as tokens.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14393 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 18 insertions, 2 deletions

diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 581d151d1..6073860c0 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -459,6 +459,11 @@ let parse_after_qmark bp s =
 	  | Utf8Token (UnicodeLetter, _) -> LEFTQMARK
 	  | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars bp '?' s)
 
+let blank_or_eof cs =
+  match Stream.peek cs with
+    | None -> true
+    | Some (' ' | '\t' | '\n' |'\r') -> true
+    | _ -> false
 
 (* Parse a token in a char stream *)
 
@@ -467,9 +472,14 @@ let rec next_token = parser bp
       comm_loc bp; push_char c; next_token s
   | [< ''$' as c; t = parse_after_special c bp >] ep ->
       comment_stop bp; (t, (ep, bp))
-  | [< ''.' as c; t = parse_after_special c bp >] ep ->
+  | [< ''.' as c; t = parse_after_special c bp; s >] ep ->
       comment_stop bp;
-      if Flags.do_beautify() && t=KEYWORD "." then between_com := true;
+      (* We enforce that "." should either be part of a larger keyword,
+         for instance ".(", or followed by a blank or eof. *)
+      if t = KEYWORD "." then begin
+	if not (blank_or_eof s) then err (bp,ep+1) Undefined_token;
+	if Flags.do_beautify() then between_com := true;
+      end;
       (t, (bp,ep))
   | [< ''?'; s >] ep ->
       let t = parse_after_qmark bp s in comment_stop bp; (t, (ep, bp))
@@ -507,6 +517,12 @@ let rec next_token = parser bp
 	| EmptyStream ->
 	    comment_stop bp; (EOI, (bp, bp + 1))
 
+(* (* Debug: uncomment this for tracing tokens seen by coq...*)
+let next_token s =
+  let (t,(bp,ep)) = next_token s in Printf.eprintf "[%s]\n%!" (Tok.to_string t);
+  (t,(bp,ep))
+*)
+
 (* Location table system for creating tables associating a token count
    to its location in a char stream (the source) *)