--- 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 ***
--- 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,
--- 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
--- 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);