diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-03 08:31:37 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-03 08:31:37 +0000 |
| commit | 72f121c514c0dc2f8942a1e4395ec5843d5e901c (patch) | |
| tree | 50fc1a780ca6b48b461254324915899f3168cf66 /parsing | |
| parent | 9e77807e1cbca5c23888ec2b7a8c94523b00eb28 (diff) | |
Le '.' peut faire partie d'un token
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3359 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/lexer.ml4 | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index d2a46fcf4..cb0f07111 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -238,11 +238,14 @@ let rec next_token = parser bp | [< '' ' | '\n' | '\r'| '\t'; s >] -> next_token s | [< ''$'; len = ident (store 0 '$') >] ep -> (("METAIDENT", get_buff len), (bp,ep)) - | [< ''.'; t = parser + | [< ''.' as c; t = parser | [< ' ('_' | 'a'..'z' | 'A'..'Z' | '\192'..'\214' | '\216'..'\246' | '\248'..'\255' as c); len = ident (store 0 c) >] -> ("FIELD", get_buff len) +(* | [< >] -> ("", ".") >] ep -> (t, (bp,ep)) +*) + | [< (t,_) = process_chars bp c >] -> t >] ep -> (t, (bp,ep)) | [< ' ('_' | 'a'..'z' | 'A'..'Z' | '\192'..'\214' | '\216'..'\246' | '\248'..'\255' as c); len = ident (store 0 c) >] ep -> |