replaced Symbol.is_hex_letter to Symbol.is_ascii_hex;
tuned Symbol.is_ascii_blank (according to SML syntax);
--- 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");