# HG changeset patch
# User wenzelm
# Date 1237539101 -3600
# Node ID de241396389cf0b4ef02b9ce194854f98c6973dc
# Parent  4216e9c70cfe6766df47dcc54926fd46964bfd8d
allow non-printable symbols within string tokens;

diff -r 4216e9c70cfe -r de241396389c src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Thu Mar 19 22:05:37 2009 +0100
+++ b/src/Pure/ML/ml_lex.ML	Fri Mar 20 09:51:41 2009 +0100
@@ -163,8 +163,8 @@
     Scan.one (Symbol.is_ascii_digit o symbol) >> (fn ((a, b), c) => [a, b, c]);
 
 val scan_str =
-  Scan.one (fn (s, _) => Symbol.is_regular s andalso Symbol.is_printable s
-    andalso s <> "\"" andalso s <> "\\") >> single ||
+  Scan.one (fn (s, _) => Symbol.is_regular s andalso s <> "\"" andalso s <> "\\" andalso
+    (not (Symbol.is_char s) orelse Symbol.is_printable s)) >> single ||
   $$$ "\\" @@@ !!! "bad escape character in string" scan_escape;
 
 val scan_gap = $$$ "\\" @@@ scan_blanks1 @@@ $$$ "\\";