--- 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) =>