40 (* attribute source *) |
40 (* attribute source *) |
41 |
41 |
42 val _ = Theory.setup |
42 val _ = Theory.setup |
43 (ML_Antiquotation.declaration @{binding attributes} (Scan.lift Parse.attribs) |
43 (ML_Antiquotation.declaration @{binding attributes} (Scan.lift Parse.attribs) |
44 (fn _ => fn raw_srcs => fn ctxt => |
44 (fn _ => fn raw_srcs => fn ctxt => |
45 let |
45 let val i = serial () in |
46 val i = serial (); |
46 ctxt |
47 |
47 |> put_attributes (i, Attrib.check_attribs ctxt raw_srcs) |
48 val (a, ctxt') = ctxt |
48 |> ML_Context.value_decl "attributes" |
49 |> ML_Antiquotation.variant "attributes" |
49 ("ML_Thms.the_attributes ML_context " ^ string_of_int i) |
50 ||> put_attributes (i, Attrib.check_attribs ctxt raw_srcs); |
50 end)); |
51 val ml = |
|
52 ("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^ |
|
53 string_of_int i ^ ";\n", "Isabelle." ^ a); |
|
54 in (K ml, ctxt') end)); |
|
55 |
51 |
56 |
52 |
57 (* fact references *) |
53 (* fact references *) |
58 |
54 |
59 fun thm_binding kind is_single thms ctxt = |
55 fun thm_binding kind is_single thms ctxt = |
60 let |
56 let |
61 val initial = null (get_thmss ctxt); |
57 val initial = null (get_thmss ctxt); |
62 val (name, ctxt') = ML_Antiquotation.variant kind ctxt; |
58 val (name, ctxt') = ML_Context.variant kind ctxt; |
63 val ctxt'' = cons_thms ((name, is_single), thms) ctxt'; |
59 val ctxt'' = cons_thms ((name, is_single), thms) ctxt'; |
64 |
60 |
65 val ml_body = "Isabelle." ^ name; |
61 val ml_body = "Isabelle." ^ name; |
66 fun decl final_ctxt = |
62 fun decl final_ctxt = |
67 if initial then |
63 if initial then |