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

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 ->