added is/to_ascii_lower/upper;
authorwenzelm
Tue Jul 25 21:18:07 2006 +0200 (2006-07-25)
changeset 20200c6fb50dbbc30
parent 20199 3170fea83ae7
child 20201 24b49cbd438b
added is/to_ascii_lower/upper;
tuned alphanum -- needs more work;
src/Pure/General/symbol.ML
     1.1 --- a/src/Pure/General/symbol.ML	Tue Jul 25 21:18:06 2006 +0200
     1.2 +++ b/src/Pure/General/symbol.ML	Tue Jul 25 21:18:07 2006 +0200
     1.3 @@ -27,6 +27,10 @@
     1.4    val is_ascii_digit: symbol -> bool
     1.5    val is_ascii_quasi: symbol -> bool
     1.6    val is_ascii_blank: symbol -> bool
     1.7 +  val is_ascii_lower: symbol -> bool
     1.8 +  val is_ascii_upper: symbol -> bool
     1.9 +  val to_ascii_lower: symbol -> symbol
    1.10 +  val to_ascii_upper: symbol -> symbol
    1.11    val is_raw: symbol -> bool
    1.12    val decode_raw: symbol -> string
    1.13    val encode_raw: string -> string
    1.14 @@ -143,6 +147,12 @@
    1.15    fn " " => true | "\t" => true | "\n" => true | "\^L" => true | "\^M" => true
    1.16      | _ => false;
    1.17  
    1.18 +fun is_ascii_lower s = is_char s andalso (ord "a" <= ord s andalso ord s <= ord "z");
    1.19 +fun is_ascii_upper s = is_char s andalso (ord "A" <= ord s andalso ord s <= ord "Z");
    1.20 +
    1.21 +fun to_ascii_lower s = if is_ascii_upper s then chr (ord s + ord "a" - ord "A") else s;
    1.22 +fun to_ascii_upper s = if is_ascii_lower s then chr (ord s + ord "A" - ord "a") else s;
    1.23 +
    1.24  
    1.25  (* encode_raw *)
    1.26  
    1.27 @@ -482,6 +492,26 @@
    1.28    in implode (rev ss' @ qs) end;
    1.29  
    1.30  
    1.31 +(*turning arbitrary names into alphanumerics*)
    1.32 +
    1.33 +fun alphanum s =
    1.34 +  let
    1.35 +    fun replace_invalid c (last_inv, cs) =
    1.36 +      if (is_ascii_letter c orelse is_ascii_digit c orelse c = "'")
    1.37 +        andalso not ("." = c)   (* FIXME !? *)
    1.38 +      then (false, if last_inv then c :: "_" :: cs else c :: cs)
    1.39 +      else (true, cs);
    1.40 +    fun prefix_num_empty [] = ["x"]
    1.41 +      | prefix_num_empty (cs as c::_) =
    1.42 +          if is_ascii_digit c
    1.43 +          then "x" :: cs
    1.44 +          else cs;
    1.45 +    val (prefix, cs1) = case explode s of "'"::cs => ("'", cs) | cs => ("", cs);
    1.46 +    val (_, cs2) = fold_rev replace_invalid cs1 (false, []);
    1.47 +    val cs3 = prefix_num_empty cs2;
    1.48 +  in implode (prefix :: cs3) end;
    1.49 +
    1.50 +
    1.51  
    1.52  (** print modes **)
    1.53  
    1.54 @@ -517,26 +547,6 @@
    1.55      in (implode (map out syms), real (sym_length syms)) end;
    1.56  
    1.57  
    1.58 -(*turning arbitrary names into alphanumerics*)
    1.59 -
    1.60 -fun alphanum s =
    1.61 -  let
    1.62 -    fun replace_invalid c (last_inv, cs) =
    1.63 -      if ((Char.isAlphaNum o the o Char.fromString) c orelse c = "'")
    1.64 -        andalso not ("." = c)
    1.65 -      then (false, if last_inv then c :: "_" :: cs else c :: cs)
    1.66 -      else (true, cs);
    1.67 -    fun prefix_num_empty [] = ["x"]
    1.68 -      | prefix_num_empty (cs as c::_) =
    1.69 -          if (Char.isDigit o the o Char.fromString) c
    1.70 -          then "x" :: cs
    1.71 -          else cs;
    1.72 -    val (prefix, cs1) = case explode s of "'"::cs => ("'", cs) | cs => ("", cs);
    1.73 -    val (_, cs2) = fold_rev replace_invalid cs1 (false, []);
    1.74 -    val cs3 = prefix_num_empty cs2;
    1.75 -  in implode (prefix :: cs3) end;
    1.76 -
    1.77 -
    1.78  (*final declarations of this structure!*)
    1.79  val length = sym_length;
    1.80  val explode = sym_explode;