src/Pure/Isar/antiquote.ML

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

   | is_antiq (Antiq _) = true;
 
 
 (* scan_antiquote *)
 
+structure T = OuterLex;
+
 local
-
-structure T = OuterLex;
 
 val scan_txt =
   T.scan_blank ||
   T.keep_line ($$ "@" --| Scan.ahead (~$$ "{")) ||
   T.keep_line (Scan.one (fn s => s <> "@" andalso Symbol.not_sync s andalso Symbol.not_eof s));

     scan_antiq >> (fn s => Antiq (s, pos)));
 
 end;
 
 
-(* antiquotes_of *)
+(* scan_antiquotes *)
 
-fun antiquotes_of (s, pos) =
+fun scan_antiquotes (s, pos) =
   (case Scan.error (Scan.finite' Symbol.stopper (Scan.repeat scan_antiquote))
       (pos, Symbol.explode s) of
     (xs, (_, [])) => xs
-  | (_, (pos', ss)) => error ("Malformed quotation/antiquotation text at: " ^
+  | (_, (pos', ss)) => error ("Malformed quotation/antiquotation source at: " ^
       quote (Symbol.beginning 10 ss) ^ Position.str_of pos'));
 
 
+(* scan_arguments *)
+
+fun scan_arguments lex antiq (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 false (K (lex, Scan.empty_lexicon)) pos
+      |> T.source_proper
+      |> Source.source T.stopper (Scan.error (Scan.bulk antiq)) NONE
+      |> Source.exhaust;
+  in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end;
+
 end;