--- a/src/Pure/Isar/antiquote.ML Mon Jan 28 22:27:21 2008 +0100
+++ b/src/Pure/Isar/antiquote.ML Mon Jan 28 22:27:23 2008 +0100
@@ -34,9 +34,8 @@
local
val scan_txt =
- T.scan_blank ||
- T.keep_line ($$ "@" --| Scan.ahead (~$$ "{")) ||
- T.keep_line (Scan.one (fn s => s <> "@" andalso Symbol.is_regular s));
+ T.count ($$ "@" --| Scan.ahead (~$$ "{")) ||
+ T.count (Scan.one (fn s => s <> "@" andalso Symbol.is_regular s));
fun escape "\\" = "\\\\"
| escape "\"" = "\\\""
@@ -45,14 +44,13 @@
val quote_escape = Library.quote o implode o map escape o Symbol.explode;
val scan_ant =
- T.scan_blank ||
T.scan_string >> quote_escape ||
- T.keep_line (Scan.one (fn s => s <> "}" andalso Symbol.is_regular s));
+ T.count (Scan.one (fn s => s <> "}" andalso Symbol.is_regular s));
val scan_antiq =
- T.keep_line ($$ "@" -- $$ "{") |--
+ T.count ($$ "@") |-- T.count ($$ "{") |--
T.!!! "missing closing brace of antiquotation"
- (Scan.repeat scan_ant >> implode) --| T.keep_line ($$ "}");
+ (Scan.repeat scan_ant >> implode) --| T.count ($$ "}");
in