src/Pure/library.ML
changeset 2196 1b36ebc70487
parent 2182 29e56f003599
child 2243 3ebeaaacfbd1
equal deleted inserted replaced
2195:e8271379ba4b 2196:1b36ebc70487
   371 (*white space: blanks, tabs, newlines, formfeeds*)
   371 (*white space: blanks, tabs, newlines, formfeeds*)
   372 val is_blank : string -> bool =
   372 val is_blank : string -> bool =
   373   fn " " => true | "\t" => true | "\n" => true | "\^L" => true | _ => false;
   373   fn " " => true | "\t" => true | "\n" => true | "\^L" => true | _ => false;
   374 
   374 
   375 val is_letdig = is_quasi_letter orf is_digit;
   375 val is_letdig = is_quasi_letter orf is_digit;
       
   376 
       
   377 (*printable chars*)
       
   378 fun is_printable c = ord c > ord " " andalso ord c <= ord "~";
   376 
   379 
   377 
   380 
   378 (*lower all chars of string*)
   381 (*lower all chars of string*)
   379 val to_lower =
   382 val to_lower =
   380   let
   383   let