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

2 files changed, 16 insertions, 0 deletions

diff --git a/lib/util.ml b/lib/util.ml
index def2d13f5..26b77a82a 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 fce150e80..26d912d15 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