tuned signature;

--- a/src/Pure/Isar/attrib.ML	Mon Aug 25 08:45:32 2014 +0200
+++ b/src/Pure/Isar/attrib.ML	Mon Aug 25 12:58:20 2014 +0200
@@ -48,6 +48,8 @@
   val thm: thm context_parser
   val thms: thm list context_parser
   val multi_thm: thm list context_parser
+  val check_attribs: Proof.context -> Token.src list -> Token.src list
+  val read_attribs: Proof.context -> Symbol_Pos.text * Position.T -> Token.src list
   val transform_facts: morphism ->
     (Attrib.binding * (thm list * Token.src list) list) list ->
     (Attrib.binding * (thm list * Token.src list) list) list
@@ -276,6 +278,25 @@
 end;
 
 
+(* read attribute source *)
+
+fun check_attribs ctxt raw_srcs =
+  let
+    val srcs = map (check_src ctxt) raw_srcs;
+    val _ = map (attribute ctxt) srcs;
+  in srcs end;
+
+fun read_attribs ctxt (text, pos) =
+  let
+    val lex = #1 (Keyword.get_lexicons ());
+    val syms = Symbol_Pos.explode (text, pos);
+  in
+    (case Token.read lex Parse.attribs (syms, pos) of
+      [raw_srcs] => check_attribs ctxt raw_srcs
+    | _ => error ("Malformed attributes" ^ Position.here pos))
+  end;
+
+
 (* transform fact expressions *)
 
 fun transform_facts phi = map (fn ((a, atts), bs) =>

--- a/src/Pure/Isar/token.ML	Mon Aug 25 08:45:32 2014 +0200
+++ b/src/Pure/Isar/token.ML	Mon Aug 25 12:58:20 2014 +0200
@@ -86,9 +86,10 @@
   val source: {do_recover: bool option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
     Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
       (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
-  val read_antiq: Scan.lexicon -> (T list -> 'a * T list) -> Symbol_Pos.T list * Position.T -> 'a
   type 'a parser = T list -> 'a * T list
   type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list)
+  val read: Scan.lexicon -> 'a parser -> Symbol_Pos.T list * Position.T -> 'a list
+  val read_antiq: Scan.lexicon -> 'a parser -> Symbol_Pos.T list * Position.T -> 'a
   val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic
   val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
 end;
@@ -585,28 +586,33 @@
 end;
 
 
-(* read_antiq *)
-
-fun read_antiq lex scan (syms, pos) =
-  let
-    fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.here pos ^ ":\n" ^
-      "@{" ^ Symbol_Pos.content syms ^ "}");
-
-    val res =
-      Source.of_list syms
-      |> source' {do_recover = NONE} (K (lex, Scan.empty_lexicon))
-      |> source_proper
-      |> Source.source stopper (Scan.error (Scan.bulk scan)) NONE
-      |> Source.exhaust;
-  in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end;
-
-
 
 (** parsers **)
 
 type 'a parser = T list -> 'a * T list;
 type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list);
 
+
+(* read source *)
+
+fun read lex scan (syms, pos) =
+  Source.of_list syms
+  |> source' {do_recover = NONE} (K (lex, Scan.empty_lexicon))
+  |> source_proper
+  |> Source.source stopper (Scan.error (Scan.bulk scan)) NONE
+  |> Source.exhaust;
+
+fun read_antiq lex scan (syms, pos) =
+  let
+    fun err msg =
+      cat_error msg ("Malformed antiquotation" ^ Position.here pos ^ ":\n" ^
+        "@{" ^ Symbol_Pos.content syms ^ "}");
+    val res = read lex scan (syms, pos) handle ERROR msg => err msg;
+  in (case res of [x] => x | _ => err "") end;
+
+
+(* wrapped syntax *)
+
 fun syntax_generic scan (Src {name = (name, pos), args = args0, output_info}) context =
   let
     val args1 = map init_assignable args0;

--- a/src/Pure/ML/ml_thms.ML	Mon Aug 25 08:45:32 2014 +0200
+++ b/src/Pure/ML/ml_thms.ML	Mon Aug 25 12:58:20 2014 +0200
@@ -44,10 +44,10 @@
     (fn _ => fn raw_srcs => fn ctxt =>
       let
         val i = serial ();
-        val srcs = map (Attrib.check_src ctxt) raw_srcs;
-        val _ = map (Attrib.attribute ctxt) srcs;
+
         val (a, ctxt') = ctxt
-          |> ML_Antiquotation.variant "attributes" ||> put_attributes (i, srcs);
+          |> ML_Antiquotation.variant "attributes"
+          ||> put_attributes (i, Attrib.check_attribs ctxt raw_srcs);
         val ml =
           ("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^
             string_of_int i ^ ";\n", "Isabelle." ^ a);