equal
deleted
inserted
replaced
37 val _ = Theory.setup |
37 val _ = Theory.setup |
38 (ML_Context.add_antiq @{binding attributes} |
38 (ML_Context.add_antiq @{binding attributes} |
39 (Scan.depend (fn context => Parse_Spec.attribs >> (fn raw_srcs => |
39 (Scan.depend (fn context => Parse_Spec.attribs >> (fn raw_srcs => |
40 let |
40 let |
41 val ctxt = Context.the_proof context; |
41 val ctxt = Context.the_proof context; |
42 val thy = Proof_Context.theory_of ctxt; |
|
43 |
42 |
44 val i = serial (); |
43 val i = serial (); |
45 val srcs = map (Attrib.intern_src thy) raw_srcs; |
44 val srcs = map (Attrib.check_src ctxt) raw_srcs; |
46 val _ = map (Attrib.attribute ctxt) srcs; |
45 val _ = map (Attrib.attribute ctxt) srcs; |
47 val (a, ctxt') = ctxt |
46 val (a, ctxt') = ctxt |
48 |> ML_Antiquote.variant "attributes" ||> put_attributes (i, srcs); |
47 |> ML_Antiquote.variant "attributes" ||> put_attributes (i, srcs); |
49 val ml = |
48 val ml = |
50 ("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^ |
49 ("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^ |