diff options
| author |  marche <marche@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-01-14 09:06:09 +0000 |
|---|---|---|
| committer | marche <marche@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-01-14 09:06:09 +0000 |
| commit | c53d8648b40d329a99ca7e0ef12c4d276ac716c8 (patch) | |
| tree | 434630cd442fe0b2aae3a5af49c4298d42435f77 /parsing/lexer.ml4 | |
| parent | bec6b37606bb0c507fa4ce7fa35120182d903dd0 (diff) | |
make libraries, lexing of more utf8 symbols
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5201 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/lexer.ml4')
| -rw-r--r-- | parsing/lexer.ml4 | 19 |
1 files changed, 14 insertions, 5 deletions
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 5ffd29984..61f28469c 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -431,11 +431,20 @@ let rec next_token = parser bp (try ("", find_keyword id) with Not_found -> ("IDENT", id)), (bp, ep)) (* iso 8859-1 accentuated letters *) - | [< ' ('\192'..'\214' | '\216'..'\246' | '\248'..'\255' as c); - len = ident_tail (store 0 c) >] ep -> - let id = get_buff len in - comment_stop bp; - (try ("", find_keyword id) with Not_found -> ("IDENT", id)), (bp, ep) + | [< ' ('\192'..'\214' | '\216'..'\246' | '\248'..'\255' as c) ; s >] -> + if !Options.v7 then + begin + match s with parser + [< len = ident_tail (store 0 c) >] ep -> + let id = get_buff len in + comment_stop bp; + (try ("", find_keyword id) with Not_found -> ("IDENT", id)), (bp, ep) + end + else + begin + match s with parser + [< t = process_chars bp c >] -> comment_stop bp; t + end | [< ' ('0'..'9' as c); len = number (store 0 c) >] ep -> comment_stop bp; (("INT", get_buff len), (bp, ep)) |