--- a/src/Pure/General/symbol_pos.ML Mon Jan 20 20:04:52 2014 +0100
+++ b/src/Pure/General/symbol_pos.ML Mon Jan 20 20:24:44 2014 +0100
@@ -204,12 +204,14 @@
in
fun scan_comment err_prefix =
- $$$ "(" @@@ $$$ "*" @@@
- !!! (fn () => err_prefix ^ "missing end of comment") (scan_body @@@ $$$ "*" @@@ $$$ ")");
+ Scan.ahead ($$ "(" -- $$ "*") |--
+ !!! (fn () => err_prefix ^ "unclosed comment")
+ ($$$ "(" @@@ $$$ "*" @@@ scan_body @@@ $$$ "*" @@@ $$$ ")");
fun scan_comment_body err_prefix =
- $$$ "(" |-- $$$ "*" |--
- !!! (fn () => err_prefix ^ "missing end of comment") (scan_body --| $$$ "*" --| $$$ ")");
+ Scan.ahead ($$ "(" -- $$ "*") |--
+ !!! (fn () => err_prefix ^ "unclosed comment")
+ ($$ "(" |-- $$ "*" |-- scan_body --| $$ "*" --| $$ ")");
val recover_comment =
$$$ "(" @@@ $$$ "*" @@@ scan_cmts;