--- a/src/Pure/Syntax/lexicon.ML Mon Jan 20 20:04:52 2014 +0100
+++ b/src/Pure/Syntax/lexicon.ML Mon Jan 20 20:24:44 2014 +0100
@@ -217,12 +217,14 @@
$$$ "'" --| Scan.ahead (~$$$ "'");
val scan_str =
- $$$ "'" @@@ $$$ "'" @@@ !!! "missing end of string"
- ((Scan.repeat scan_chr >> flat) @@@ $$$ "'" @@@ $$$ "'");
+ Scan.ahead ($$ "'" -- $$ "'") |--
+ !!! "unclosed string literal"
+ ($$$ "'" @@@ $$$ "'" @@@ (Scan.repeat scan_chr >> flat) @@@ $$$ "'" @@@ $$$ "'");
val scan_str_body =
- $$$ "'" |-- $$$ "'" |-- !!! "missing end of string"
- ((Scan.repeat scan_chr >> flat) --| $$$ "'" --| $$$ "'");
+ Scan.ahead ($$$ "'" |-- $$$ "'") |--
+ !!! "unclosed string literal"
+ ($$ "'" |-- $$ "'" |-- (Scan.repeat scan_chr >> flat) --| $$ "'" --| $$ "'");
fun implode_str cs = enclose "''" "''" (implode (map (fn "'" => "\\'" | c => c) cs));