Ajout d'espace dans les règles d'affichage des infix si des lettres figurent dans le token

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1297 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 27 insertions, 17 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index fa95bc2034..8b1cb71a13 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -6,30 +6,20 @@ open Util
 
 (* Utilities *)
 
-let is_letter c =
-  (c >= Char.code 'a' && c <= Char.code 'z') or
-  (c >= Char.code 'A' && c <= Char.code 'Z') or
-  (c >= Char.code '\248' && c <= Char.code '\255') or
-  (c >= Char.code '\192' && c <= Char.code '\214') or
-  (c >= Char.code '\216' && c <= Char.code '\246')
-
 let code_of_0 = Char.code '0'
 let code_of_9 = Char.code '9'
 
-let is_digit c = (c >= code_of_0 && c <= code_of_9)
-
-
 (* This checks that a string is acceptable as an ident, i.e. starts
    with a letter and contains only letters, digits or "'" *)
 
 let check_ident s =
   let l = String.length s in
   if l = 0 then error "The empty string is not an identifier"; 
-  let c = Char.code (String.get s 0) in
+  let c = String.get s 0 in
   if not (is_letter c) then error "An identifier starts with a letter";
   for i=1 to l-1 do
-    let c = Char.code (String.get s i) in
-    if not (is_letter c or is_digit c or c = Char.code '\'') then
+    let c = String.get s i in
+    if not (is_letter c or is_digit c or c = '\'') then
       error
 	("Character "^(String.sub s i 1)^" is not allowed in an identifier")
   done
@@ -153,16 +143,16 @@ let id_ord = Pervasives.compare
 let lift_ident id =
   let len = String.length id in
   let rec add carrypos =
-    let c = Char.code (id.[carrypos]) in
+    let c = id.[carrypos] in
     if is_digit c then
-      if c = code_of_9 then begin
+      if c = '9' then begin
 	assert (carrypos>0);
 	add (carrypos-1)
       end
       else begin
 	let newid = String.copy id in
 	String.fill newid (carrypos+1) (len-1-carrypos) '0';
-	newid.[carrypos] <- Char.chr (c + 1);
+	newid.[carrypos] <- Char.chr (Char.code c + 1);
 	newid
       end
     else begin
@@ -175,7 +165,7 @@ let lift_ident id =
     end
   in add (len-1)
 
-let has_index id = is_digit (Char.code (id.[String.length id - 1]))
+let has_index id = is_digit (id.[String.length id - 1])
 
 let restart_ident id =
   let len = String.length id in
diff --git a/lib/util.ml b/lib/util.ml
index def2d13f5c..26b77a82a3 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -19,6 +19,17 @@ let anomaly_loc (loc,s,strm) = Stdpp.raise_with_loc loc (Anomaly (s,strm))
 let user_err_loc (loc,s,strm) = Stdpp.raise_with_loc loc (UserError (s,strm))
 let invalid_arg_loc (loc,s) = Stdpp.raise_with_loc loc (Invalid_argument s)
 
+(* Characters *)
+
+let is_letter c =
+  (c >= 'a' && c <= 'z') or
+  (c >= 'A' && c <= 'Z') or
+  (c >= '\248' && c <= '\255') or
+  (c >= '\192' && c <= '\214') or
+  (c >= '\216' && c <= '\246')
+
+let is_digit c = (c >= '0' && c <= '9')
+
 (* Strings *)
 
 let explode s = 
diff --git a/lib/util.mli b/lib/util.mli
index fce150e803..26d912d152 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -25,6 +25,11 @@ val anomaly_loc : loc * string * std_ppcmds -> 'a
 val user_err_loc : loc * string * std_ppcmds -> 'a
 val invalid_arg_loc : loc * string -> 'a
 
+(*s Chars. *)
+
+val is_letter : char -> bool
+val is_digit : char -> bool
+
 (*s Strings. *)
 
 val explode : string -> string list
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 41250931cc..d0eb926a45 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -168,6 +168,10 @@ let infix_syntax_entry assoc n inf prefname astpref =
     | Some(Gramext.NonA) -> (Extend.L,Extend.L)
     | None -> (Extend.E,Extend.L)  (* LEFTA by default *)
   in
+  let inf =
+    (* Not necessary but increases legibility (e.g. for "=_S") *)
+    if is_letter (inf.[String.length inf -1]) then " "^inf^" " else inf
+  in
   [{Extend.syn_id = prefname;
     Extend.syn_prec = n,0,0;
     Extend.syn_astpat =