src/Pure/Isar/attrib.ML

   val internal: (morphism -> attribute) -> Token.src
   val add_del: attribute -> attribute -> attribute context_parser
   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
   val partial_evaluation: Proof.context ->
     (binding * (thm list * Token.src list) list) list ->

 val thm = gen_thm Facts.the_single;
 val multi_thm = gen_thm (K I);
 val thms = Scan.repeat multi_thm >> flat;
 
 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) =>