removed warning for unprintable chars in strings (functionality will
authorwenzelm
Wed Jan 29 15:45:40 1997 +0100 (1997-01-29)
changeset 25649d66b758bce5
parent 2563 e908e2716f3a
child 2565 64e52912eb09
removed warning for unprintable chars in strings (functionality will
be put into administrative script);
src/Pure/Thy/thy_scan.ML
     1.1 --- a/src/Pure/Thy/thy_scan.ML	Wed Jan 29 15:34:23 1997 +0100
     1.2 +++ b/src/Pure/Thy/thy_scan.ML	Wed Jan 29 15:45:40 1997 +0100
     1.3 @@ -67,12 +67,6 @@
     1.4    scan_ctrl || scan_dig ^^ scan_dig ^^ scan_dig ||
     1.5    scan_blanks1 ^^ $$ "\\";
     1.6  
     1.7 -fun warn_unprintable c n =
     1.8 -  (if not (is_printable c) then
     1.9 -    warning ("Unprintable char \"\\" ^ string_of_int (ord c) ^
    1.10 -      "\" in string at line " ^ string_of_int n)
    1.11 -  else (); c);
    1.12 -
    1.13  fun string ("\"" :: cs) n = (["\""], cs, n)
    1.14    | string ("\\" :: cs) n =
    1.15        (case optional scan_esc cs of
    1.16 @@ -81,7 +75,7 @@
    1.17    | string ("\n" :: cs) n = cons_fst " " (string cs (n + 1))
    1.18    | string (c :: cs) n = 
    1.19        if is_blank c then cons_fst " " (string cs n)
    1.20 -      else cons_fst (warn_unprintable c n) (string cs n)
    1.21 +      else cons_fst c (string cs n)
    1.22    | string [] n = lex_err n "missing quote at end of string";
    1.23  
    1.24