# 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 =