replaced Symbol.is_hex_letter to Symbol.is_ascii_hex;
authorwenzelm
Sat, 15 Sep 2007 19:25:54 +0200
changeset 24580 916259859344
parent 24579 852fc50927b1
child 24581 6491d89ba76c
replaced Symbol.is_hex_letter to Symbol.is_ascii_hex; tuned Symbol.is_ascii_blank (according to SML syntax);
src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Sat Sep 15 19:25:43 2007 +0200
+++ b/src/Pure/General/symbol.ML	Sat Sep 15 19:25:54 2007 +0200
@@ -23,8 +23,8 @@
   val is_regular: symbol -> bool
   val is_ascii: symbol -> bool
   val is_ascii_letter: symbol -> bool
-  val is_hex_letter: symbol -> bool
   val is_ascii_digit: symbol -> bool
+  val is_ascii_hex: symbol -> bool
   val is_ascii_quasi: symbol -> bool
   val is_ascii_blank: symbol -> bool
   val is_ascii_lower: symbol -> bool
@@ -127,20 +127,21 @@
    (ord "A" <= ord s andalso ord s <= ord "Z" orelse
     ord "a" <= ord s andalso ord s <= ord "z");
 
-fun is_hex_letter s =
-  is_char s andalso
-   (ord "A" <= ord s andalso ord s <= ord "F" orelse
-    ord "a" <= ord s andalso ord s <= ord "f");
-
 fun is_ascii_digit s =
   is_char s andalso ord "0" <= ord s andalso ord s <= ord "9";
 
+fun is_ascii_hex s =
+  is_char s andalso
+   (ord "0" <= ord s andalso ord s <= ord "9" orelse
+    ord "A" <= ord s andalso ord s <= ord "F" orelse
+    ord "a" <= ord s andalso ord s <= ord "f");
+
 fun is_ascii_quasi "_" = true
   | is_ascii_quasi "'" = true
   | is_ascii_quasi _ = false;
 
 val is_ascii_blank =
-  fn " " => true | "\t" => true | "\n" => true | "\^L" => true | "\^M" => true
+  fn " " => true | "\t" => true | "\n" => true | "\^K" => true | "\^L" => true | "\^M" => true
     | _ => false;
 
 fun is_ascii_lower s = is_char s andalso (ord "a" <= ord s andalso ord s <= ord "z");