# 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;