# HG changeset patch
# User wenzelm
# Date 1153855087 -7200
# Node ID c6fb50dbbc304c555425d28fb84305b693be6a11
# Parent  3170fea83ae7ce2e1ac607fbc3a49166e3e914e2
added is/to_ascii_lower/upper;
tuned alphanum -- needs more work;

diff -r 3170fea83ae7 -r c6fb50dbbc30 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Tue Jul 25 21:18:06 2006 +0200
+++ b/src/Pure/General/symbol.ML	Tue Jul 25 21:18:07 2006 +0200
@@ -27,6 +27,10 @@
   val is_ascii_digit: symbol -> bool
   val is_ascii_quasi: symbol -> bool
   val is_ascii_blank: symbol -> bool
+  val is_ascii_lower: symbol -> bool
+  val is_ascii_upper: symbol -> bool
+  val to_ascii_lower: symbol -> symbol
+  val to_ascii_upper: symbol -> symbol
   val is_raw: symbol -> bool
   val decode_raw: symbol -> string
   val encode_raw: string -> string
@@ -143,6 +147,12 @@
   fn " " => true | "\t" => true | "\n" => true | "\^L" => true | "\^M" => true
     | _ => false;
 
+fun is_ascii_lower s = is_char s andalso (ord "a" <= ord s andalso ord s <= ord "z");
+fun is_ascii_upper s = is_char s andalso (ord "A" <= ord s andalso ord s <= ord "Z");
+
+fun to_ascii_lower s = if is_ascii_upper s then chr (ord s + ord "a" - ord "A") else s;
+fun to_ascii_upper s = if is_ascii_lower s then chr (ord s + ord "A" - ord "a") else s;
+
 
 (* encode_raw *)
 
@@ -482,6 +492,26 @@
   in implode (rev ss' @ qs) end;
 
 
+(*turning arbitrary names into alphanumerics*)
+
+fun alphanum s =
+  let
+    fun replace_invalid c (last_inv, cs) =
+      if (is_ascii_letter c orelse is_ascii_digit c orelse c = "'")
+        andalso not ("." = c)   (* FIXME !? *)
+      then (false, if last_inv then c :: "_" :: cs else c :: cs)
+      else (true, cs);
+    fun prefix_num_empty [] = ["x"]
+      | prefix_num_empty (cs as c::_) =
+          if is_ascii_digit c
+          then "x" :: cs
+          else cs;
+    val (prefix, cs1) = case explode s of "'"::cs => ("'", cs) | cs => ("", cs);
+    val (_, cs2) = fold_rev replace_invalid cs1 (false, []);
+    val cs3 = prefix_num_empty cs2;
+  in implode (prefix :: cs3) end;
+
+
 
 (** print modes **)
 
@@ -517,26 +547,6 @@
     in (implode (map out syms), real (sym_length syms)) end;
 
 
-(*turning arbitrary names into alphanumerics*)
-
-fun alphanum s =
-  let
-    fun replace_invalid c (last_inv, cs) =
-      if ((Char.isAlphaNum o the o Char.fromString) c orelse c = "'")
-        andalso not ("." = c)
-      then (false, if last_inv then c :: "_" :: cs else c :: cs)
-      else (true, cs);
-    fun prefix_num_empty [] = ["x"]
-      | prefix_num_empty (cs as c::_) =
-          if (Char.isDigit o the o Char.fromString) c
-          then "x" :: cs
-          else cs;
-    val (prefix, cs1) = case explode s of "'"::cs => ("'", cs) | cs => ("", cs);
-    val (_, cs2) = fold_rev replace_invalid cs1 (false, []);
-    val cs3 = prefix_num_empty cs2;
-  in implode (prefix :: cs3) end;
-
-
 (*final declarations of this structure!*)
 val length = sym_length;
 val explode = sym_explode;