replaced Symbol.is_hex_letter to Symbol.is_ascii_hex;
authorwenzelm
Sat Sep 15 19:25:54 2007 +0200 (2007-09-15)
changeset 24580916259859344
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
     1.1 --- a/src/Pure/General/symbol.ML	Sat Sep 15 19:25:43 2007 +0200
     1.2 +++ b/src/Pure/General/symbol.ML	Sat Sep 15 19:25:54 2007 +0200
     1.3 @@ -23,8 +23,8 @@
     1.4    val is_regular: symbol -> bool
     1.5    val is_ascii: symbol -> bool
     1.6    val is_ascii_letter: symbol -> bool
     1.7 -  val is_hex_letter: symbol -> bool
     1.8    val is_ascii_digit: symbol -> bool
     1.9 +  val is_ascii_hex: symbol -> bool
    1.10    val is_ascii_quasi: symbol -> bool
    1.11    val is_ascii_blank: symbol -> bool
    1.12    val is_ascii_lower: symbol -> bool
    1.13 @@ -127,20 +127,21 @@
    1.14     (ord "A" <= ord s andalso ord s <= ord "Z" orelse
    1.15      ord "a" <= ord s andalso ord s <= ord "z");
    1.16  
    1.17 -fun is_hex_letter s =
    1.18 -  is_char s andalso
    1.19 -   (ord "A" <= ord s andalso ord s <= ord "F" orelse
    1.20 -    ord "a" <= ord s andalso ord s <= ord "f");
    1.21 -
    1.22  fun is_ascii_digit s =
    1.23    is_char s andalso ord "0" <= ord s andalso ord s <= ord "9";
    1.24  
    1.25 +fun is_ascii_hex s =
    1.26 +  is_char s andalso
    1.27 +   (ord "0" <= ord s andalso ord s <= ord "9" orelse
    1.28 +    ord "A" <= ord s andalso ord s <= ord "F" orelse
    1.29 +    ord "a" <= ord s andalso ord s <= ord "f");
    1.30 +
    1.31  fun is_ascii_quasi "_" = true
    1.32    | is_ascii_quasi "'" = true
    1.33    | is_ascii_quasi _ = false;
    1.34  
    1.35  val is_ascii_blank =
    1.36 -  fn " " => true | "\t" => true | "\n" => true | "\^L" => true | "\^M" => true
    1.37 +  fn " " => true | "\t" => true | "\n" => true | "\^K" => true | "\^L" => true | "\^M" => true
    1.38      | _ => false;
    1.39  
    1.40  fun is_ascii_lower s = is_char s andalso (ord "a" <= ord s andalso ord s <= ord "z");