diff options
author | 2003-02-27 16:00:16 +0000 | |
---|---|---|
committer | 2003-02-27 16:00:16 +0000 | |
commit | 538aff1e33de17e3aa840402731dd6ba483f1cdb (patch) | |
tree | 7c1cfc15ff0a1def6b0d249de5b72d0dcf9e7747 /toplevel | |
parent | c7b40c6ce35eb54f708d5d91ef264f6be92949c0 (diff) |
Le lexeur et Notation savent reconnaître si un unicode des blocs
0380-03FF (lettres grecques) 2100-214F (symboles assimilés à des
lettres), 2200-22FF (opérateurs mathématiques), 2300-23FF (symboles
techniques divers) et 2600-26FF (symboles divers) est un caractère
spécial ou non lorsque encodé en utf-8.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3712 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/metasyntax.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index d41ce2803..fbbae0a1b 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -391,15 +391,13 @@ let quote x = else x -let is_symbol = function String s -> not (is_letter s.[0]) | _ -> false - let rec find_symbols c_current c_next c_last vars = function | [] -> (vars, []) - | String x :: sl when is_letter x.[0] -> + | String x :: sl when Lexer.is_normal_token x -> + Lexer.check_ident x; let id = Names.id_of_string x in if List.mem_assoc id vars then error ("Variable "^x^" occurs more than once"); -(* let prec = if List.exists is_symbol sl then c_current else c_last in*) let prec = if sl <> [] then c_current else c_last in let (vars,l) = find_symbols c_next c_next c_last vars sl in ((id,prec)::vars, NonTerminal id :: l) @@ -413,6 +411,7 @@ let rec find_symbols c_current c_next c_last vars = function (vars, NonTerminal (prec, meta) :: l) *) | String s :: sl -> + Lexer.check_special_token s; let (vars,l) = find_symbols c_next c_next c_last vars sl in (vars, Terminal (strip s) :: l) | WhiteSpace n :: sl -> |