# HG changeset patch
# User wenzelm
# Date 848334499 -3600
# Node ID 1b36ebc70487ef3d296ad35a791e9863d815b10b
# Parent  e8271379ba4b161f595e0cbbd0a619d61cbf5763
added is_printable: string -> bool;

diff -r e8271379ba4b -r 1b36ebc70487 src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Nov 18 17:27:59 1996 +0100
+++ b/src/Pure/library.ML	Mon Nov 18 17:28:19 1996 +0100
@@ -374,6 +374,9 @@
 
 val is_letdig = is_quasi_letter orf is_digit;
 
+(*printable chars*)
+fun is_printable c = ord c > ord " " andalso ord c <= ord "~";
+
 
 (*lower all chars of string*)
 val to_lower =