# HG changeset patch # User haftmann # Date 1224231252 -7200 # Node ID 764ef122a164da07ae65a6bdfe43b2087afd9169 # Parent 7b2cb494e11c2f43b3e944f9bd58df0aaae21c3a added type antiquotation diff -r 7b2cb494e11c -r 764ef122a164 doc-src/more_antiquote.ML --- a/doc-src/more_antiquote.ML Thu Oct 16 23:58:29 2008 +0200 +++ b/doc-src/more_antiquote.ML Fri Oct 17 10:14:12 2008 +0200 @@ -29,13 +29,22 @@ local -fun pr_class ctxt = enclose "\\isa{" "}" o Pretty.output o Pretty.str - o Sign.extern_class (ProofContext.theory_of ctxt) o Sign.read_class (ProofContext.theory_of ctxt); +val pr_text = enclose "\\isa{" "}" o Pretty.output o Pretty.str; + +fun pr_class ctxt = Sign.read_class (ProofContext.theory_of ctxt) + #> Sign.extern_class (ProofContext.theory_of ctxt) + #> pr_text; + +fun pr_type ctxt = Sign.intern_type (ProofContext.theory_of ctxt) + #> tap (Sign.arity_number (ProofContext.theory_of ctxt)) + #> Sign.extern_type (ProofContext.theory_of ctxt) + #> pr_text; in val _ = O.add_commands - [("class", ThyOutput.args (Scan.lift Args.name) (K pr_class))] + [("class", ThyOutput.args (Scan.lift Args.name) (K pr_class)), + ("type", ThyOutput.args (Scan.lift Args.name) (K pr_type))] end;