# HG changeset patch
# User wenzelm
# Date 1201555643 -3600
# Node ID 469ee728a5d77ffa47f6b5f723928650a0853b0e
# Parent  d0a133941155659f095a48dc2813fd737f5e3dd4
T.count/counted: improved position handling for token syntax;

diff -r d0a133941155 -r 469ee728a5d7 src/Pure/Isar/antiquote.ML
--- 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