src/Pure/Isar/antiquote.ML

 sig
   datatype antiquote =
     Text of string | Antiq of (string * Position.T) * Position.T |
     Open of Position.T | Close of Position.T
   val is_antiq: antiquote -> bool
-  val scan_antiquotes: string * Position.T -> antiquote list
-  val scan_arguments: Scan.lexicon -> (OuterLex.token list -> 'a * OuterLex.token list) ->
+  val read: string * Position.T -> antiquote list
+  val read_arguments: Scan.lexicon -> (OuterLex.token list -> 'a * OuterLex.token list) ->
     string * Position.T -> 'a
 end;
 
 structure Antiquote: ANTIQUOTE =
 struct

   in check antiqs [] end;
 
 
 (* scan_antiquote *)
 
+open BasicSymbolPos;
 structure T = OuterLex;
 
 local
 
-fun count scan = Scan.depend (fn pos => scan >> (fn x => (Position.advance [x] pos, x)));
-
 val scan_txt =
-  count ($$ "@" --| Scan.ahead (~$$ "{")) ||
-  count (Scan.one (fn s =>
-    s <> "@" andalso s <> "\\<lbrace>" andalso s <> "\\<rbrace>" andalso Symbol.is_regular s));
+  $$$ "@" --| Scan.ahead (~$$$ "{") ||
+  Scan.one (fn (s, _) => s <> "@" andalso s <> "\\<lbrace>" andalso s <> "\\<rbrace>"
+    andalso Symbol.is_regular s) >> single;
 
 val scan_ant =
-  T.scan_quoted >> implode ||
-  count (Scan.one (fn s => s <> "}" andalso Symbol.is_regular s));
+  T.scan_quoted ||
+  Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
 
 val scan_antiq =
-  Scan.state -- (count ($$ "@") |-- count ($$ "{") |--
+  SymbolPos.scan_position -- ($$$ "@" |-- $$$ "{" |--
     T.!!! "missing closing brace of antiquotation"
-      (Scan.state -- Scan.repeat scan_ant -- Scan.state -- (count ($$ "}") |-- Scan.state)))
+      (SymbolPos.scan_position -- Scan.repeat scan_ant -- SymbolPos.scan_position --
+        ($$$ "}" |-- SymbolPos.scan_position)))
   >> (fn (pos1, (((pos2, body), pos3), pos4)) =>
-    Antiq ((implode body, Position.encode_range (pos2, pos3)), Position.encode_range (pos1, pos4)));
+    Antiq ((implode (map symbol (flat body)),
+      Position.encode_range (pos2, pos3)), Position.encode_range (pos1, pos4)));
 
 in
 
-val scan_antiquote =
-  Scan.repeat1 scan_txt >> (Text o implode) ||
+val scan_antiquote = T.!!! "malformed quotation/antiquotation"
+ (Scan.repeat1 scan_txt >> (Text o implode o map symbol o flat) ||
   scan_antiq ||
-  Scan.state --| count ($$ "\\<lbrace>") >> Open ||
-  Scan.state --| count ($$ "\\<rbrace>") >> Close;
+  SymbolPos.scan_position --| $$$ "\\<lbrace>" >> Open ||
+  SymbolPos.scan_position --| $$$ "\\<rbrace>" >> Close);
 
 end;
 
 
-(* scan_antiquotes *)
+(* read *)
 
-fun scan_antiquotes (s, pos) =
-  (case Scan.error (Scan.finite' Symbol.stopper (Scan.repeat scan_antiquote))
-      (pos, Symbol.explode s) of
-    (xs, (_, [])) => (check_nesting xs; xs)
-  | (_, (pos', ss)) => error ("Malformed quotation/antiquotation source at: " ^
-      quote (Symbol.beginning 10 ss) ^ Position.str_of pos'));
+fun read ("", _) = []
+  | read (s, pos) =
+      (case Scan.read SymbolPos.stopper (Scan.bulk scan_antiquote) (SymbolPos.explode (s, pos)) of
+        SOME xs => (check_nesting xs; xs)
+      | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
 
 
 (* scan_arguments *)
 
-fun scan_arguments lex antiq (s, pos) =
+fun read_arguments lex scan (s, pos) =
   let
     fun err msg = cat_error msg
       ("Malformed antiquotation: " ^ quote ("@{" ^ s ^ "}") ^ Position.str_of pos);
 
     val res =
       Source.of_string s
       |> Symbol.source false
       |> T.source NONE (K (lex, Scan.empty_lexicon)) pos
       |> T.source_proper
-      |> Source.source T.stopper (Scan.error (Scan.bulk antiq)) NONE
+      |> Source.source T.stopper (Scan.error (Scan.bulk scan)) NONE
       |> Source.exhaust;
   in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end;
 
 end;