improved is_letter etc.;
authorwenzelm
Thu Feb 12 12:35:50 1998 +0100 (1998-02-12)
changeset 4616d257e6c6614f
parent 4615 67457d16cdbc
child 4617 cea2a5b5ee10
improved is_letter etc.;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Tue Feb 10 10:27:30 1998 +0100
     1.2 +++ b/src/Pure/library.ML	Thu Feb 12 12:35:50 1998 +0100
     1.3 @@ -374,11 +374,12 @@
     1.4  (** strings **)
     1.5  
     1.6  fun is_letter ch =
     1.7 -  ord "A" <= ord ch andalso ord ch <= ord "Z" orelse
     1.8 -  ord "a" <= ord ch andalso ord ch <= ord "z";
     1.9 +  size ch = 1 andalso
    1.10 +   (ord "A" <= ord ch andalso ord ch <= ord "Z" orelse
    1.11 +    ord "a" <= ord ch andalso ord ch <= ord "z");
    1.12  
    1.13  fun is_digit ch =
    1.14 -  ord "0" <= ord ch andalso ord ch <= ord "9";
    1.15 +  size ch = 1 andalso ord "0" <= ord ch andalso ord ch <= ord "9";
    1.16  
    1.17  (*letter or _ or prime (')*)
    1.18  fun is_quasi_letter "_" = true
    1.19 @@ -393,13 +394,13 @@
    1.20  val is_letdig = is_quasi_letter orf is_digit;
    1.21  
    1.22  (*printable chars*)
    1.23 -fun is_printable c = ord c > ord " " andalso ord c <= ord "~";
    1.24 +fun is_printable c = size c = 1 andalso ord c > ord " " andalso ord c <= ord "~";
    1.25  
    1.26  (*lower all chars of string*)
    1.27  val to_lower =
    1.28    let
    1.29      fun lower ch =
    1.30 -      if ch >= "A" andalso ch <= "Z" then
    1.31 +      if size ch = 1 andalso ch >= "A" andalso ch <= "Z" then
    1.32          chr (ord ch - ord "A" + ord "a")
    1.33        else ch;
    1.34    in implode o (map lower) o explode end;