# HG changeset patch
# User wenzelm
# Date 1165869663 -3600
# Node ID 3f9324ff06e3ee2fcd4681acd1b8b4fec95f1b82
# Parent  0038f5fc2065f951b1801afc01a7768f0a239293
xstr: disallow backslashes;

diff -r 0038f5fc2065 -r 3f9324ff06e3 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Mon Dec 11 21:39:28 2006 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Mon Dec 11 21:41:03 2006 +0100
@@ -224,8 +224,8 @@
   "Inner lexical error: " ^ msg ^ " at " ^ quote (prfx ^ Symbol.beginning 10 cs);
 
 val scan_chr =
-  $$ "\\" |-- Scan.one Symbol.not_eof ||
-  Scan.one (fn s => s <> "'" andalso Symbol.not_eof s) ||
+  $$ "\\" |-- $$ "'" ||
+  Scan.one (fn s => s <> "\\" andalso s <> "'" andalso Symbol.not_eof s) ||
   $$ "'" --| Scan.ahead (~$$ "'");
 
 val scan_str =