clarified @{type} antiquotation: abbreviations and nonterminals count as "syntactic", disallow TFrees;
authorwenzelm
Fri Sep 24 16:17:59 2010 +0200 (2010-09-24)
changeset 3968978b185bf7660
parent 39688 a6e703a1fb4f
child 39690 6c6164b37fef
clarified @{type} antiquotation: abbreviations and nonterminals count as "syntactic", disallow TFrees;
tuned;
NEWS
doc-src/IsarRef/Thy/Document_Preparation.thy
doc-src/IsarRef/Thy/document/Document_Preparation.tex
src/Pure/Thy/thy_output.ML
     1.1 --- a/NEWS	Fri Sep 24 15:56:29 2010 +0200
     1.2 +++ b/NEWS	Fri Sep 24 16:17:59 2010 +0200
     1.3 @@ -68,7 +68,7 @@
     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 +* Document antiquotations @{class} and @{type} for printing classes
     1.9  and type constructors.
    1.10  
    1.11  
     2.1 --- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Fri Sep 24 15:56:29 2010 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Fri Sep 24 16:17:59 2010 +0200
     2.3 @@ -250,8 +250,8 @@
     2.4  
     2.5    \item @{text "@{typ \<tau>}"} prints a well-formed type @{text "\<tau>"}.
     2.6  
     2.7 -  \item @{text "@{type \<kappa>}"} prints a type constructor
     2.8 -    (logical or abbreviation) @{text "\<kappa>"}.
     2.9 +  \item @{text "@{type \<kappa>}"} prints a (logical or syntactic) type
    2.10 +    constructor @{text "\<kappa>"}.
    2.11  
    2.12    \item @{text "@{class c}"} prints a class @{text c}.
    2.13  
     3.1 --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Fri Sep 24 15:56:29 2010 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Fri Sep 24 16:17:59 2010 +0200
     3.3 @@ -266,8 +266,8 @@
     3.4  
     3.5    \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typ\ {\isasymtau}{\isacharbraceright}{\isachardoublequote}} prints a well-formed type \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}.
     3.6  
     3.7 -  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}type\ {\isasymkappa}{\isacharbraceright}{\isachardoublequote}} prints a type constructor
     3.8 -    (logical or abbreviation) \isa{{\isachardoublequote}{\isasymkappa}{\isachardoublequote}}.
     3.9 +  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}type\ {\isasymkappa}{\isacharbraceright}{\isachardoublequote}} prints a (logical or syntactic) type
    3.10 +    constructor \isa{{\isachardoublequote}{\isasymkappa}{\isachardoublequote}}.
    3.11  
    3.12    \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}class\ c{\isacharbraceright}{\isachardoublequote}} prints a class \isa{c}.
    3.13  
     4.1 --- a/src/Pure/Thy/thy_output.ML	Fri Sep 24 15:56:29 2010 +0200
     4.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Sep 24 16:17:59 2010 +0200
     4.3 @@ -511,10 +511,8 @@
     4.4    Pretty.str o Type.extern_class (ProofContext.tsig_of ctxt) o ProofContext.read_class ctxt;
     4.5  
     4.6  fun pretty_type ctxt s =
     4.7 -  let
     4.8 -    val tsig = ProofContext.tsig_of ctxt;
     4.9 -    val _ = ProofContext.read_type_name ctxt false s;
    4.10 -  in (Pretty.str o Type.extern_type tsig o Type.intern_type tsig) s end;
    4.11 +  let val Type (name, _) = ProofContext.read_type_name_proper ctxt false s
    4.12 +  in Pretty.str (Type.extern_type (ProofContext.tsig_of ctxt) name) end;
    4.13  
    4.14  fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;
    4.15