equal
deleted
inserted
replaced
62 #> Type.extern_type (ProofContext.tsig_of ctxt) |
62 #> Type.extern_type (ProofContext.tsig_of ctxt) |
63 #> pr_text; |
63 #> pr_text; |
64 |
64 |
65 in |
65 in |
66 |
66 |
67 val _ = ThyOutput.antiquotation "class" (Scan.lift Args.name) (pr_class o #context); |
67 val _ = Thy_Output.antiquotation "class" (Scan.lift Args.name) (pr_class o #context); |
68 val _ = ThyOutput.antiquotation "type" (Scan.lift Args.name) (pr_type o #context); |
68 val _ = Thy_Output.antiquotation "type" (Scan.lift Args.name) (pr_type o #context); |
69 |
69 |
70 end; |
70 end; |
71 |
71 |
72 |
72 |
73 (* code theorem antiquotation *) |
73 (* code theorem antiquotation *) |
93 val thms = Code_Preproc.cert eqngr const |
93 val thms = Code_Preproc.cert eqngr const |
94 |> Code.equations_of_cert thy |
94 |> Code.equations_of_cert thy |
95 |> snd |
95 |> snd |
96 |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE) |
96 |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE) |
97 |> map (holize o no_vars ctxt o AxClass.overload thy); |
97 |> map (holize o no_vars ctxt o AxClass.overload thy); |
98 in ThyOutput.output (ThyOutput.maybe_pretty_source (pretty_thm ctxt) src thms) end; |
98 in Thy_Output.output (Thy_Output.maybe_pretty_source (pretty_thm ctxt) src thms) end; |
99 |
99 |
100 in |
100 in |
101 |
101 |
102 val _ = ThyOutput.antiquotation "code_thms" Args.term |
102 val _ = Thy_Output.antiquotation "code_thms" Args.term |
103 (fn {source, context, ...} => pretty_code_thm source context); |
103 (fn {source, context, ...} => pretty_code_thm source context); |
104 |
104 |
105 end; |
105 end; |
106 |
106 |
107 |
107 |
121 >> (fn insts => fn thy => fn naming => map_filter (Code_Thingol.lookup_instance naming o apsnd (Sign.intern_type thy) o apfst (Sign.intern_class thy) o swap) insts); |
121 >> (fn insts => fn thy => fn naming => map_filter (Code_Thingol.lookup_instance naming o apsnd (Sign.intern_type thy) o apfst (Sign.intern_class thy) o swap) insts); |
122 val parse_names = parse_consts || parse_types || parse_classes || parse_instances; |
122 val parse_names = parse_consts || parse_types || parse_classes || parse_instances; |
123 |
123 |
124 in |
124 in |
125 |
125 |
126 val _ = ThyOutput.antiquotation "code_stmts" |
126 val _ = Thy_Output.antiquotation "code_stmts" |
127 (parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name)) |
127 (parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name)) |
128 (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), target) => |
128 (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), target) => |
129 let val thy = ProofContext.theory_of ctxt in |
129 let val thy = ProofContext.theory_of ctxt in |
130 Code_Target.code_of thy |
130 Code_Target.code_of thy |
131 target NONE "Example" (mk_cs thy) |
131 target NONE "Example" (mk_cs thy) |