# HG changeset patch # User wenzelm # Date 854549140 -3600 # Node ID 9d66b758bce58e386a18715cd63d0e059faf775a # Parent e908e2716f3ad4a09328ebccee5748c8d4af5ea6 removed warning for unprintable chars in strings (functionality will be put into administrative script); diff -r e908e2716f3a -r 9d66b758bce5 src/Pure/Thy/thy_scan.ML --- a/src/Pure/Thy/thy_scan.ML Wed Jan 29 15:34:23 1997 +0100 +++ b/src/Pure/Thy/thy_scan.ML Wed Jan 29 15:45:40 1997 +0100 @@ -67,12 +67,6 @@ scan_ctrl || scan_dig ^^ scan_dig ^^ scan_dig || scan_blanks1 ^^ $$ "\\"; -fun warn_unprintable c n = - (if not (is_printable c) then - warning ("Unprintable char \"\\" ^ string_of_int (ord c) ^ - "\" in string at line " ^ string_of_int n) - else (); c); - fun string ("\"" :: cs) n = (["\""], cs, n) | string ("\\" :: cs) n = (case optional scan_esc cs of @@ -81,7 +75,7 @@ | string ("\n" :: cs) n = cons_fst " " (string cs (n + 1)) | string (c :: cs) n = if is_blank c then cons_fst " " (string cs n) - else cons_fst (warn_unprintable c n) (string cs n) + else cons_fst c (string cs n) | string [] n = lex_err n "missing quote at end of string";