aboutsummaryrefslogtreecommitdiff
path: root/lib/util.ml
diff options
context:
space:
mode:
authorherbelin2001-01-31 11:24:15 +0000
committerherbelin2001-01-31 11:24:15 +0000
commit7de3189d5f82e11a8f584dd1a6104c7863dcc2b4 (patch)
tree67bee4f7a715207a1e2a5831588e6e8c3c1744fb /lib/util.ml
parentece4c4c205acf42f07f62c314b0f647fd12367e5 (diff)
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
Diffstat (limited to 'lib/util.ml')
-rw-r--r--lib/util.ml11
1 files changed, 11 insertions, 0 deletions
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 =