T.count/counted: improved position handling for token syntax;
authorwenzelm
Mon, 28 Jan 2008 22:27:23 +0100
changeset 26002 469ee728a5d7
parent 26001 d0a133941155
child 26003 7a8aee8353cf
T.count/counted: improved position handling for token syntax;
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