# HG changeset patch
# User wenzelm
# Date 1217957348 -7200
# Node ID c7aa4c18739db6f1972d226f754dd4fbbaadd6fe
# Parent  31899d977a89eddbf9216e6fe20997a8bb43a0ea
moved OuterLex.count here;

diff -r 31899d977a89 -r c7aa4c18739d src/Pure/Isar/antiquote.ML
--- a/src/Pure/Isar/antiquote.ML	Tue Aug 05 19:29:07 2008 +0200
+++ b/src/Pure/Isar/antiquote.ML	Tue Aug 05 19:29:08 2008 +0200
@@ -53,33 +53,35 @@
 
 local
 
+fun count scan = Scan.depend (fn pos => scan >> (fn x => (Position.advance [x] pos, x)));
+
 val scan_txt =
-  T.count ($$ "@" --| Scan.ahead (~$$ "{")) ||
-  T.count (Scan.one (fn s =>
+  count ($$ "@" --| Scan.ahead (~$$ "{")) ||
+  count (Scan.one (fn s =>
     s <> "@" andalso s <> "\\<lbrace>" andalso s <> "\\<rbrace>" andalso Symbol.is_regular s));
 
 fun escape "\\" = "\\\\"
   | escape "\"" = "\\\""
   | escape s = s;
 
-val quote_escape = Library.quote o implode o map escape o Symbol.explode;
+val quote_escape = Library.quote o implode o map escape o T.clean_value;
 
 val scan_ant =
   T.scan_string >> quote_escape ||
-  T.count (Scan.one (fn s => s <> "}" andalso Symbol.is_regular s));
+  count (Scan.one (fn s => s <> "}" andalso Symbol.is_regular s));
 
 val scan_antiq =
-  T.count ($$ "@") |-- T.count ($$ "{") |--
+  count ($$ "@") |-- count ($$ "{") |--
     T.!!! "missing closing brace of antiquotation"
-      (Scan.repeat scan_ant >> implode) --| T.count ($$ "}");
+      (Scan.repeat scan_ant >> implode) --| count ($$ "}");
 
 in
 
 fun scan_antiquote (pos, ss) = (pos, ss) |>
   (Scan.repeat1 scan_txt >> (Text o implode) ||
     scan_antiq >> (fn s => Antiq (s, pos)) ||
-    T.count ($$ "\\<lbrace>") >> K (Open pos) ||
-    T.count ($$ "\\<rbrace>") >> K (Close pos));
+    count ($$ "\\<lbrace>") >> K (Open pos) ||
+    count ($$ "\\<rbrace>") >> K (Close pos));
 
 end;