# HG changeset patch
# User wenzelm
# Date 848334758 -3600
# Node ID 64cb98f841e4becb6416a4e213337e1b9437ad63
# Parent  c2dbdc2ef78186871f674af97c31adbac4d45979
improved string scanner: converts 8 bit chars to escape sequences;

diff -r c2dbdc2ef781 -r 64cb98f841e4 src/Pure/Thy/thy_scan.ML
--- a/src/Pure/Thy/thy_scan.ML	Mon Nov 18 17:31:14 1996 +0100
+++ b/src/Pure/Thy/thy_scan.ML	Mon Nov 18 17:32:38 1996 +0100
@@ -73,10 +73,11 @@
       (case optional scan_esc cs of
         (None, _) => lex_err n "bad escape sequence in string"
       | (Some s, cs') => cons_fst ("\\" ^ s) (string cs' (inc_line n s)))
+  | string ("\n" :: cs) n = cons_fst " " (string cs (n + 1))
   | string (c :: cs) n = 
-      if c = "\n" then string cs (n+1)
-      else if is_blank c then cons_fst " " (string cs n)
-      else cons_fst c (string cs n)
+      if is_blank c then cons_fst " " (string cs n)
+      else if is_printable c then cons_fst c (string cs n)
+      else cons_fst ("\\" ^ string_of_int (ord c)) (string cs n)
   | string [] n = lex_err n "missing quote at end of string";