From fb119901df9d336886c69f558874ddc05c085fbb Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 26 Jul 2011 16:03:29 +0000 Subject: ide/coq_lex.mll: restore the separate parsing of .. (fix #2578) Trying to have a direct rule for "..." seemed to be less hack-ish, but is in fact _wrong_, shame on me : it's important to have a rule for ".." since this can appear in a coq sentence (for instance in recursive notations), and hence we don't want the second dot to be considered as a terminator. So let's restore the previous situation, with a rule for ".." (ignoring them) and a rule for "."+blank. Then "..." is recognized as ".." + ".", which is quite ok after all. The fact that ".. ." is also recognized by coqide in a similar way isn't actually a problem: after reading this sentence, coqide will send it to coqtop, and it's coqtop that will tell that this sentence makes no sense... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14300 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/coq_lex.mll | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'ide/coq_lex.mll') diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll index b605c13e5..a88c94dac 100644 --- a/ide/coq_lex.mll +++ b/ide/coq_lex.mll @@ -160,8 +160,15 @@ and sentence initial stamp = parse | ident as id { (try here stamp lexbuf (tag_of_ident initial id) with Not_found -> ()); sentence false stamp lexbuf } + | ".." { + (* We must have a particular rule for parsing "..", where no dot + is a terminator, even if we have a blank afterwards + (cf. for instance the syntax for recursive notation). + This rule and the following one also allow to treat the "..." + special case, where the third dot is a terminator. *) + sentence false stamp lexbuf + } | dot_sep { Lexing.lexeme_start lexbuf } (* The usual "." terminator *) - | ".." dot_sep { Lexing.lexeme_start lexbuf + 2 } (* The "..." special case *) | undotted_sep { (* Separators like { or } are only active at the start of a sentence *) if initial then Lexing.lexeme_start lexbuf -- cgit v1.2.3