--- a/src/Pure/Isar/token.ML Mon Jan 20 20:04:52 2014 +0100
+++ b/src/Pure/Isar/token.ML Mon Jan 20 20:24:44 2014 +0100
@@ -325,9 +325,11 @@
Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s) >> single;
val scan_verbatim =
- (Symbol_Pos.scan_pos --| $$$ "{" --| $$$ "*") -- !!! "missing end of verbatim text"
- (Symbol_Pos.change_prompt
- ((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- Symbol_Pos.scan_pos)));
+ Scan.ahead ($$$ "{" -- $$$ "*") |--
+ !!! "unclosed verbatim text"
+ ((Symbol_Pos.scan_pos --| $$$ "{" --| $$$ "*") --
+ Symbol_Pos.change_prompt
+ ((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- Symbol_Pos.scan_pos)));
val recover_verbatim =
$$$ "{" @@@ $$$ "*" @@@ (Scan.repeat scan_verb >> flat);