equal
deleted
inserted
replaced
27 |
27 |
28 (* class antiquotation *) |
28 (* class antiquotation *) |
29 |
29 |
30 local |
30 local |
31 |
31 |
32 fun pr_class ctxt = enclose "\\isa{" "}" o Pretty.output o Pretty.str |
32 val pr_text = enclose "\\isa{" "}" o Pretty.output o Pretty.str; |
33 o Sign.extern_class (ProofContext.theory_of ctxt) o Sign.read_class (ProofContext.theory_of ctxt); |
33 |
|
34 fun pr_class ctxt = Sign.read_class (ProofContext.theory_of ctxt) |
|
35 #> Sign.extern_class (ProofContext.theory_of ctxt) |
|
36 #> pr_text; |
|
37 |
|
38 fun pr_type ctxt = Sign.intern_type (ProofContext.theory_of ctxt) |
|
39 #> tap (Sign.arity_number (ProofContext.theory_of ctxt)) |
|
40 #> Sign.extern_type (ProofContext.theory_of ctxt) |
|
41 #> pr_text; |
34 |
42 |
35 in |
43 in |
36 |
44 |
37 val _ = O.add_commands |
45 val _ = O.add_commands |
38 [("class", ThyOutput.args (Scan.lift Args.name) (K pr_class))] |
46 [("class", ThyOutput.args (Scan.lift Args.name) (K pr_class)), |
|
47 ("type", ThyOutput.args (Scan.lift Args.name) (K pr_type))] |
39 |
48 |
40 end; |
49 end; |
41 |
50 |
42 |
51 |
43 (* code antiquotation *) |
52 (* code antiquotation *) |