equal
deleted
inserted
replaced
59 in Pretty.str (Proof_Context.extern_type ctxt name) end; |
59 in Pretty.str (Proof_Context.extern_type ctxt name) end; |
60 |
60 |
61 fun pretty_prf full ctxt = Proof_Syntax.pretty_clean_proof_of ctxt full; |
61 fun pretty_prf full ctxt = Proof_Syntax.pretty_clean_proof_of ctxt full; |
62 |
62 |
63 fun pretty_theory ctxt (name, pos) = |
63 fun pretty_theory ctxt (name, pos) = |
64 (Theory.check {long = false} ctxt (name, pos); Pretty.str name); |
64 (Theory.check {long = true} ctxt (name, pos); Pretty.str name); |
65 |
65 |
66 val basic_entity = Thy_Output.antiquotation_pretty_source; |
66 val basic_entity = Thy_Output.antiquotation_pretty_source; |
67 |
67 |
68 fun basic_entities name scan pretty = |
68 fun basic_entities name scan pretty = |
69 Document_Antiquotation.setup name scan |
69 Document_Antiquotation.setup name scan |