# HG changeset patch
# User wenzelm
# Date 1169240903 -3600
# Node ID 560c5b5dda1ccbc2c529976f0040171bbc58ed0c
# Parent  4a65d2f4d0b59ffb93e4025b9ebd59230cf37ce2
tuned signature;
added scan_arguments;

diff -r 4a65d2f4d0b5 -r 560c5b5dda1c src/Pure/Isar/antiquote.ML
--- a/src/Pure/Isar/antiquote.ML	Fri Jan 19 22:08:22 2007 +0100
+++ b/src/Pure/Isar/antiquote.ML	Fri Jan 19 22:08:23 2007 +0100
@@ -10,7 +10,9 @@
   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 =
@@ -30,9 +32,9 @@
 
 (* scan_antiquote *)
 
-local
+structure T = OuterLex;
 
-structure T = OuterLex;
+local
 
 val scan_txt =
   T.scan_blank ||
@@ -64,14 +66,30 @@
 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;