added warning for unprintable chars in strings;
authorwenzelm
Fri Dec 13 17:38:56 1996 +0100 (1996-12-13)
changeset 23871b37895b607a
parent 2386 58f8ff014009
child 2388 d1f0505fc602
added warning for unprintable chars in strings;
src/Pure/Thy/thy_scan.ML
     1.1 --- a/src/Pure/Thy/thy_scan.ML	Fri Dec 13 17:38:17 1996 +0100
     1.2 +++ b/src/Pure/Thy/thy_scan.ML	Fri Dec 13 17:38:56 1996 +0100
     1.3 @@ -67,6 +67,11 @@
     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 @@ -76,7 +81,7 @@
    1.16    | string ("\n" :: cs) n = cons_fst " " (string cs (n + 1))
    1.17    | string (c :: cs) n = 
    1.18        if is_blank c then cons_fst " " (string cs n)
    1.19 -      else cons_fst c (string cs n)
    1.20 +      else cons_fst (warn_unprintable c n) (string cs n)
    1.21    | string [] n = lex_err n "missing quote at end of string";
    1.22  
    1.23