src/Pure/library.ML
changeset 3393 e31ac367387e
parent 3365 86c0d1988622
child 3407 afd288caf573
equal deleted inserted replaced
3392:d0d86b96aa96 3393:e31ac367387e
   389   | is_quasi_letter "'" = true
   389   | is_quasi_letter "'" = true
   390   | is_quasi_letter ch = is_letter ch;
   390   | is_quasi_letter ch = is_letter ch;
   391 
   391 
   392 (*white space: blanks, tabs, newlines, formfeeds*)
   392 (*white space: blanks, tabs, newlines, formfeeds*)
   393 val is_blank : string -> bool =
   393 val is_blank : string -> bool =
   394   fn " " => true | "\t" => true | "\n" => true | "\^L" => true | "160" => true
   394   fn " " => true | "\t" => true | "\n" => true | "\^L" => true | "\160" => true
   395     | _ => false;
   395     | _ => false;
   396 
   396 
   397 val is_letdig = is_quasi_letter orf is_digit;
   397 val is_letdig = is_quasi_letter orf is_digit;
   398 
   398 
   399 (*printable chars*)
   399 (*printable chars*)