'class' and 'type' are now antiquoations by default
authorhaftmann
Mon Sep 13 14:53:56 2010 +0200 (2010-09-13)
changeset 39305d4fa19eb0822
parent 39300 ad79b89b4351
child 39306 c1f3992c9097
'class' and 'type' are now antiquoations by default
NEWS
doc-src/IsarRef/Thy/Document_Preparation.thy
doc-src/more_antiquote.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/NEWS	Mon Sep 13 09:29:43 2010 +0200
     1.2 +++ b/NEWS	Mon Sep 13 14:53:56 2010 +0200
     1.3 @@ -68,6 +68,9 @@
     1.4  * Discontinued ancient 'constdefs' command.  INCOMPATIBILITY, use
     1.5  'definition' instead.
     1.6  
     1.7 +* Document antiquotations 'class' and 'type' for printing classes
     1.8 +and type constructors.
     1.9 +
    1.10  
    1.11  *** HOL ***
    1.12  
     2.1 --- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Mon Sep 13 09:29:43 2010 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Mon Sep 13 14:53:56 2010 +0200
     2.3 @@ -146,6 +146,8 @@
     2.4      @{antiquotation_def const} & : & @{text antiquotation} \\
     2.5      @{antiquotation_def abbrev} & : & @{text antiquotation} \\
     2.6      @{antiquotation_def typ} & : & @{text antiquotation} \\
     2.7 +    @{antiquotation_def type} & : & @{text antiquotation} \\
     2.8 +    @{antiquotation_def class} & : & @{text antiquotation} \\
     2.9      @{antiquotation_def "text"} & : & @{text antiquotation} \\
    2.10      @{antiquotation_def goals} & : & @{text antiquotation} \\
    2.11      @{antiquotation_def subgoals} & : & @{text antiquotation} \\
    2.12 @@ -190,6 +192,8 @@
    2.13        'const' options term |
    2.14        'abbrev' options term |
    2.15        'typ' options type |
    2.16 +      'type' options name |
    2.17 +      'class' options name |
    2.18        'text' options name |
    2.19        'goals' options |
    2.20        'subgoals' options |
    2.21 @@ -243,8 +247,14 @@
    2.22    
    2.23    \item @{text "@{abbrev c x\<^sub>1 \<dots> x\<^sub>n}"} prints a constant abbreviation
    2.24    @{text "c x\<^sub>1 \<dots> x\<^sub>n \<equiv> rhs"} as defined in the current context.
    2.25 +
    2.26    \item @{text "@{typ \<tau>}"} prints a well-formed type @{text "\<tau>"}.
    2.27 -  
    2.28 +
    2.29 +  \item @{text "@{type \<kappa>}"} prints a type constructor
    2.30 +    (logical or abbreviation) @{text "\<kappa>"}.
    2.31 +
    2.32 +  \item @{text "@{class c}"} prints a class @{text c}.
    2.33 +
    2.34    \item @{text "@{text s}"} prints uninterpreted source text @{text
    2.35    s}.  This is particularly useful to print portions of text according
    2.36    to the Isabelle document style, without demanding well-formedness,
     3.1 --- a/doc-src/more_antiquote.ML	Mon Sep 13 09:29:43 2010 +0200
     3.2 +++ b/doc-src/more_antiquote.ML	Mon Sep 13 14:53:56 2010 +0200
     3.3 @@ -47,29 +47,6 @@
     3.4    end
     3.5  
     3.6  
     3.7 -(* class and type constructor antiquotation *)
     3.8 -
     3.9 -local
    3.10 -
    3.11 -val pr_text = enclose "\\isa{" "}" o Pretty.output NONE o Pretty.str;
    3.12 -
    3.13 -fun pr_class ctxt = ProofContext.read_class ctxt
    3.14 -  #> Type.extern_class (ProofContext.tsig_of ctxt)
    3.15 -  #> pr_text;
    3.16 -
    3.17 -fun pr_type ctxt = ProofContext.read_type_name_proper ctxt true
    3.18 -  #> (#1 o Term.dest_Type)
    3.19 -  #> Type.extern_type (ProofContext.tsig_of ctxt)
    3.20 -  #> pr_text;
    3.21 -
    3.22 -in
    3.23 -
    3.24 -val _ = Thy_Output.antiquotation "class" (Scan.lift Args.name) (pr_class o #context);
    3.25 -val _ = Thy_Output.antiquotation "type" (Scan.lift Args.name) (pr_type o #context);
    3.26 -
    3.27 -end;
    3.28 -
    3.29 -
    3.30  (* code theorem antiquotation *)
    3.31  
    3.32  local
     4.1 --- a/src/Pure/Thy/thy_output.ML	Mon Sep 13 09:29:43 2010 +0200
     4.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Sep 13 14:53:56 2010 +0200
     4.3 @@ -507,6 +507,12 @@
     4.4      val ctxt' = Variable.auto_fixes eq ctxt;
     4.5    in ProofContext.pretty_term_abbrev ctxt' eq end;
     4.6  
     4.7 +fun pretty_class ctxt =
     4.8 +  Pretty.str o Type.extern_class (ProofContext.tsig_of ctxt) o ProofContext.read_class ctxt;
     4.9 +
    4.10 +fun pretty_type ctxt = Pretty.str o Type.extern_type (ProofContext.tsig_of ctxt)
    4.11 +  o fst o dest_Type o ProofContext.read_type_name_proper ctxt false;
    4.12 +
    4.13  fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;
    4.14  
    4.15  fun pretty_theory ctxt name =
    4.16 @@ -561,6 +567,8 @@
    4.17  val _ = basic_entity "const" (Args.const_proper false) pretty_const;
    4.18  val _ = basic_entity "abbrev" (Scan.lift Args.name_source) pretty_abbrev;
    4.19  val _ = basic_entity "typ" Args.typ_abbrev Syntax.pretty_typ;
    4.20 +val _ = basic_entity "class" (Scan.lift Args.name) pretty_class;
    4.21 +val _ = basic_entity "type" (Scan.lift Args.name) pretty_type;
    4.22  val _ = basic_entity "text" (Scan.lift Args.name) pretty_text;
    4.23  val _ = basic_entities "prf" Attrib.thms (pretty_prf false);
    4.24  val _ = basic_entities "full_prf" Attrib.thms (pretty_prf true);