# HG changeset patch
# User haftmann
# Date 1284382436 -7200
# Node ID d4fa19eb082265cfe98227999d009230e0162e5c
# Parent  ad79b89b4351f670e243b95a81ae413005a8dad1
'class' and 'type' are now antiquoations by default

diff -r ad79b89b4351 -r d4fa19eb0822 NEWS
--- a/NEWS	Mon Sep 13 09:29:43 2010 +0200
+++ b/NEWS	Mon Sep 13 14:53:56 2010 +0200
@@ -68,6 +68,9 @@
 * Discontinued ancient 'constdefs' command.  INCOMPATIBILITY, use
 'definition' instead.
 
+* Document antiquotations 'class' and 'type' for printing classes
+and type constructors.
+
 
 *** HOL ***
 
diff -r ad79b89b4351 -r d4fa19eb0822 doc-src/IsarRef/Thy/Document_Preparation.thy
--- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Mon Sep 13 09:29:43 2010 +0200
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Mon Sep 13 14:53:56 2010 +0200
@@ -146,6 +146,8 @@
     @{antiquotation_def const} & : & @{text antiquotation} \\
     @{antiquotation_def abbrev} & : & @{text antiquotation} \\
     @{antiquotation_def typ} & : & @{text antiquotation} \\
+    @{antiquotation_def type} & : & @{text antiquotation} \\
+    @{antiquotation_def class} & : & @{text antiquotation} \\
     @{antiquotation_def "text"} & : & @{text antiquotation} \\
     @{antiquotation_def goals} & : & @{text antiquotation} \\
     @{antiquotation_def subgoals} & : & @{text antiquotation} \\
@@ -190,6 +192,8 @@
       'const' options term |
       'abbrev' options term |
       'typ' options type |
+      'type' options name |
+      'class' options name |
       'text' options name |
       'goals' options |
       'subgoals' options |
@@ -243,8 +247,14 @@
   
   \item @{text "@{abbrev c x\<^sub>1 \<dots> x\<^sub>n}"} prints a constant abbreviation
   @{text "c x\<^sub>1 \<dots> x\<^sub>n \<equiv> rhs"} as defined in the current context.
+
   \item @{text "@{typ \<tau>}"} prints a well-formed type @{text "\<tau>"}.
-  
+
+  \item @{text "@{type \<kappa>}"} prints a type constructor
+    (logical or abbreviation) @{text "\<kappa>"}.
+
+  \item @{text "@{class c}"} prints a class @{text c}.
+
   \item @{text "@{text s}"} prints uninterpreted source text @{text
   s}.  This is particularly useful to print portions of text according
   to the Isabelle document style, without demanding well-formedness,
diff -r ad79b89b4351 -r d4fa19eb0822 doc-src/more_antiquote.ML
--- a/doc-src/more_antiquote.ML	Mon Sep 13 09:29:43 2010 +0200
+++ b/doc-src/more_antiquote.ML	Mon Sep 13 14:53:56 2010 +0200
@@ -47,29 +47,6 @@
   end
 
 
-(* class and type constructor antiquotation *)
-
-local
-
-val pr_text = enclose "\\isa{" "}" o Pretty.output NONE o Pretty.str;
-
-fun pr_class ctxt = ProofContext.read_class ctxt
-  #> Type.extern_class (ProofContext.tsig_of ctxt)
-  #> pr_text;
-
-fun pr_type ctxt = ProofContext.read_type_name_proper ctxt true
-  #> (#1 o Term.dest_Type)
-  #> Type.extern_type (ProofContext.tsig_of ctxt)
-  #> pr_text;
-
-in
-
-val _ = Thy_Output.antiquotation "class" (Scan.lift Args.name) (pr_class o #context);
-val _ = Thy_Output.antiquotation "type" (Scan.lift Args.name) (pr_type o #context);
-
-end;
-
-
 (* code theorem antiquotation *)
 
 local
diff -r ad79b89b4351 -r d4fa19eb0822 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Mon Sep 13 09:29:43 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML	Mon Sep 13 14:53:56 2010 +0200
@@ -507,6 +507,12 @@
     val ctxt' = Variable.auto_fixes eq ctxt;
   in ProofContext.pretty_term_abbrev ctxt' eq end;
 
+fun pretty_class ctxt =
+  Pretty.str o Type.extern_class (ProofContext.tsig_of ctxt) o ProofContext.read_class ctxt;
+
+fun pretty_type ctxt = Pretty.str o Type.extern_type (ProofContext.tsig_of ctxt)
+  o fst o dest_Type o ProofContext.read_type_name_proper ctxt false;
+
 fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;
 
 fun pretty_theory ctxt name =
@@ -561,6 +567,8 @@
 val _ = basic_entity "const" (Args.const_proper false) pretty_const;
 val _ = basic_entity "abbrev" (Scan.lift Args.name_source) pretty_abbrev;
 val _ = basic_entity "typ" Args.typ_abbrev Syntax.pretty_typ;
+val _ = basic_entity "class" (Scan.lift Args.name) pretty_class;
+val _ = basic_entity "type" (Scan.lift Args.name) pretty_type;
 val _ = basic_entity "text" (Scan.lift Args.name) pretty_text;
 val _ = basic_entities "prf" Attrib.thms (pretty_prf false);
 val _ = basic_entities "full_prf" Attrib.thms (pretty_prf true);