diff options
| author | herbelin | 2003-02-27 16:47:04 +0000 |
|---|---|---|
| committer | herbelin | 2003-02-27 16:47:04 +0000 |
| commit | 0207af4b3f550c3972676f881c9528ddfb0da260 (patch) | |
| tree | f2837c1b04e06ee06bae65f7e07ee2ea23f8f5bd | |
| parent | bed6c4c2212781feac37258e6de41a18730b18bc (diff) | |
Correction test token normal
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3715 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/lexer.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 362a066f58..ff54f74ef0 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -69,7 +69,7 @@ let bad_token str = raise (Error (Bad_token str)) let check_special_token str = let rec loop = parser - | [< ' (' ' | '\n' | '\r' | '\t') >] -> bad_token str + | [< ' (' ' | '\n' | '\r' | '\t' | '"') >] -> bad_token str | [< _ = Stream.empty >] -> () | [< '_ ; s >] -> loop s in @@ -109,7 +109,7 @@ let is_keyword s = let is_normal_token str = if String.length str > 0 then match str.[0] with - | ' ' | '\n' | '\r' | '\t' | '0'..'9' | '"' -> bad_token str + | ' ' | '\n' | '\r' | '\t' | '"' -> bad_token str | '_' | '$' | 'a'..'z' | 'A'..'Z' -> true (* utf-8 symbols of the form "E2 xx xx" [E2=226] *) | '\226' when String.length str > 2 -> |