--- a/src/Pure/ML/ml_lex.ML Mon Jan 20 16:14:19 2014 +0100
+++ b/src/Pure/ML/ml_lex.ML Mon Jan 20 16:56:18 2014 +0100
@@ -241,8 +241,9 @@
$$$ "#" @@@ $$$ "\"" @@@ scan_gaps @@@ Scan.optional (Scan.permissive scan_str @@@ scan_gaps) [];
val scan_string =
- $$$ "\"" @@@ !!! "missing quote at end of string"
- ((Scan.repeat (scan_gap || scan_str) >> flat) @@@ $$$ "\"");
+ Scan.ahead ($$ "\"") |--
+ !!! "unclosed string literal"
+ ($$$ "\"" @@@ (Scan.repeat (scan_gap || scan_str) >> flat) @@@ $$$ "\"");
val recover_string =
$$$ "\"" @@@ (Scan.repeat (scan_gap || Scan.permissive scan_str) >> flat);
@@ -304,9 +305,7 @@
(SOME (false, fn msg => recover msg >> map Antiquote.Text))
|> Source.exhaust
|> tap (Position.reports_text o Antiquote.reports_of (single o report_of_token))
- |> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ())))
- handle ERROR msg =>
- cat_error msg ("The error(s) above occurred in ML source" ^ Position.here pos);
+ |> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ())));
in input @ termination end;
end;