diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-26 16:03:29 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-26 16:03:29 +0000 |
| commit | fb119901df9d336886c69f558874ddc05c085fbb (patch) | |
| tree | c6ff6c483f6b7131ede53ee809302cc2c586a67c /ide/coq_lex.mll | |
| parent | 965081d15e59665cd4d6186d7dd437d92470f782 (diff) | |
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
Diffstat (limited to 'ide/coq_lex.mll')
| -rw-r--r-- | ide/coq_lex.mll | 9 |
1 files changed, 8 insertions, 1 deletions
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 |