term styles also cover antiquotations term_type and typeof
authorhaftmann
Fri Oct 09 10:00:47 2009 +0200 (2009-10-09)
changeset 32898e871d897969c
parent 32897 2b2c56530d25
child 32899 c913cc831630
term styles also cover antiquotations term_type and typeof
NEWS
doc-src/IsarRef/Thy/Document_Preparation.thy
doc-src/IsarRef/Thy/document/Document_Preparation.tex
doc-src/LaTeXsugar/Sugar/Sugar.thy
doc-src/LaTeXsugar/Sugar/document/Sugar.tex
src/Pure/Thy/thy_output.ML
     1.1 --- a/NEWS	Fri Oct 09 09:14:25 2009 +0200
     1.2 +++ b/NEWS	Fri Oct 09 10:00:47 2009 +0200
     1.3 @@ -27,7 +27,9 @@
     1.4  *** document preparation ***
     1.5  
     1.6  * New generalized style concept for printing terms:
     1.7 -write @{foo (style) ...} instead of @{foo_style style ...}.
     1.8 +write @{foo (style) ...} instead of @{foo_style style ...}
     1.9 +(old form is still retained for backward compatibility).
    1.10 +Styles can be also applied for antiquotations prop, term_type and typeof.
    1.11  
    1.12  
    1.13  *** HOL ***
     2.1 --- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Fri Oct 09 09:14:25 2009 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Fri Oct 09 10:00:47 2009 +0200
     2.3 @@ -141,9 +141,10 @@
     2.4      @{antiquotation_def "lemma"} & : & @{text antiquotation} \\
     2.5      @{antiquotation_def "prop"} & : & @{text antiquotation} \\
     2.6      @{antiquotation_def "term"} & : & @{text antiquotation} \\
     2.7 +    @{antiquotation_def term_type} & : & @{text antiquotation} \\
     2.8 +    @{antiquotation_def typeof} & : & @{text antiquotation} \\
     2.9      @{antiquotation_def const} & : & @{text antiquotation} \\
    2.10      @{antiquotation_def abbrev} & : & @{text antiquotation} \\
    2.11 -    @{antiquotation_def typeof} & : & @{text antiquotation} \\
    2.12      @{antiquotation_def typ} & : & @{text antiquotation} \\
    2.13      @{antiquotation_def "text"} & : & @{text antiquotation} \\
    2.14      @{antiquotation_def goals} & : & @{text antiquotation} \\
    2.15 @@ -184,9 +185,10 @@
    2.16        'lemma' options prop 'by' method |
    2.17        'prop' options styles prop |
    2.18        'term' options styles term |
    2.19 +      'term_type' options styles term |
    2.20 +      'typeof' options styles term |
    2.21        'const' options term |
    2.22        'abbrev' options term |
    2.23 -      'typeof' options term |
    2.24        'typ' options type |
    2.25        'text' options name |
    2.26        'goals' options |
    2.27 @@ -230,15 +232,17 @@
    2.28  
    2.29    \item @{text "@{term t}"} prints a well-typed term @{text "t"}.
    2.30  
    2.31 +  \item @{text "@{term_type t}"} prints a well-typed term @{text "t"}
    2.32 +  annotated with its type.
    2.33 +
    2.34 +  \item @{text "@{typeof t}"} prints the type of a well-typed term
    2.35 +  @{text "t"}.
    2.36 +
    2.37    \item @{text "@{const c}"} prints a logical or syntactic constant
    2.38    @{text "c"}.
    2.39    
    2.40    \item @{text "@{abbrev c x\<^sub>1 \<dots> x\<^sub>n}"} prints a constant abbreviation
    2.41    @{text "c x\<^sub>1 \<dots> x\<^sub>n \<equiv> rhs"} as defined in the current context.
    2.42 -
    2.43 -  \item @{text "@{typeof t}"} prints the type of a well-typed term
    2.44 -  @{text "t"}.
    2.45 -
    2.46    \item @{text "@{typ \<tau>}"} prints a well-formed type @{text "\<tau>"}.
    2.47    
    2.48    \item @{text "@{text s}"} prints uninterpreted source text @{text
     3.1 --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Fri Oct 09 09:14:25 2009 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Fri Oct 09 10:00:47 2009 +0200
     3.3 @@ -159,9 +159,10 @@
     3.4      \indexdef{}{antiquotation}{lemma}\hypertarget{antiquotation.lemma}{\hyperlink{antiquotation.lemma}{\mbox{\isa{lemma}}}} & : & \isa{antiquotation} \\
     3.5      \indexdef{}{antiquotation}{prop}\hypertarget{antiquotation.prop}{\hyperlink{antiquotation.prop}{\mbox{\isa{prop}}}} & : & \isa{antiquotation} \\
     3.6      \indexdef{}{antiquotation}{term}\hypertarget{antiquotation.term}{\hyperlink{antiquotation.term}{\mbox{\isa{term}}}} & : & \isa{antiquotation} \\
     3.7 +    \indexdef{}{antiquotation}{term\_type}\hypertarget{antiquotation.term-type}{\hyperlink{antiquotation.term-type}{\mbox{\isa{term{\isacharunderscore}type}}}} & : & \isa{antiquotation} \\
     3.8 +    \indexdef{}{antiquotation}{typeof}\hypertarget{antiquotation.typeof}{\hyperlink{antiquotation.typeof}{\mbox{\isa{typeof}}}} & : & \isa{antiquotation} \\
     3.9      \indexdef{}{antiquotation}{const}\hypertarget{antiquotation.const}{\hyperlink{antiquotation.const}{\mbox{\isa{const}}}} & : & \isa{antiquotation} \\
    3.10      \indexdef{}{antiquotation}{abbrev}\hypertarget{antiquotation.abbrev}{\hyperlink{antiquotation.abbrev}{\mbox{\isa{abbrev}}}} & : & \isa{antiquotation} \\
    3.11 -    \indexdef{}{antiquotation}{typeof}\hypertarget{antiquotation.typeof}{\hyperlink{antiquotation.typeof}{\mbox{\isa{typeof}}}} & : & \isa{antiquotation} \\
    3.12      \indexdef{}{antiquotation}{typ}\hypertarget{antiquotation.typ}{\hyperlink{antiquotation.typ}{\mbox{\isa{typ}}}} & : & \isa{antiquotation} \\
    3.13      \indexdef{}{antiquotation}{text}\hypertarget{antiquotation.text}{\hyperlink{antiquotation.text}{\mbox{\isa{text}}}} & : & \isa{antiquotation} \\
    3.14      \indexdef{}{antiquotation}{goals}\hypertarget{antiquotation.goals}{\hyperlink{antiquotation.goals}{\mbox{\isa{goals}}}} & : & \isa{antiquotation} \\
    3.15 @@ -202,9 +203,10 @@
    3.16        'lemma' options prop 'by' method |
    3.17        'prop' options styles prop |
    3.18        'term' options styles term |
    3.19 +      'term_type' options styles term |
    3.20 +      'typeof' options styles term |
    3.21        'const' options term |
    3.22        'abbrev' options term |
    3.23 -      'typeof' options term |
    3.24        'typ' options type |
    3.25        'text' options name |
    3.26        'goals' options |
    3.27 @@ -246,15 +248,17 @@
    3.28  
    3.29    \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term\ t{\isacharbraceright}{\isachardoublequote}} prints a well-typed term \isa{{\isachardoublequote}t{\isachardoublequote}}.
    3.30  
    3.31 +  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term{\isacharunderscore}type\ t{\isacharbraceright}{\isachardoublequote}} prints a well-typed term \isa{{\isachardoublequote}t{\isachardoublequote}}
    3.32 +  annotated with its type.
    3.33 +
    3.34 +  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typeof\ t{\isacharbraceright}{\isachardoublequote}} prints the type of a well-typed term
    3.35 +  \isa{{\isachardoublequote}t{\isachardoublequote}}.
    3.36 +
    3.37    \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}const\ c{\isacharbraceright}{\isachardoublequote}} prints a logical or syntactic constant
    3.38    \isa{{\isachardoublequote}c{\isachardoublequote}}.
    3.39    
    3.40    \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}abbrev\ c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isacharbraceright}{\isachardoublequote}} prints a constant abbreviation
    3.41    \isa{{\isachardoublequote}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ rhs{\isachardoublequote}} as defined in the current context.
    3.42 -
    3.43 -  \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typeof\ t{\isacharbraceright}{\isachardoublequote}} prints the type of a well-typed term
    3.44 -  \isa{{\isachardoublequote}t{\isachardoublequote}}.
    3.45 -
    3.46    \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typ\ {\isasymtau}{\isacharbraceright}{\isachardoublequote}} prints a well-formed type \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}.
    3.47    
    3.48    \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}text\ s{\isacharbraceright}{\isachardoublequote}} prints uninterpreted source text \isa{s}.  This is particularly useful to print portions of text according
     4.1 --- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Fri Oct 09 09:14:25 2009 +0200
     4.2 +++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Fri Oct 09 10:00:47 2009 +0200
     4.3 @@ -309,7 +309,7 @@
     4.4  \verb!we conclude !\verb!@!\verb!{thm (concl) conjI}!
     4.5  \end{quote}
     4.6  Thus you can rearrange or hide premises and typeset the theorem as you like.
     4.7 -Styles like !(prem 1)! are a general mechanism explained
     4.8 +Styles like \verb!(prem 1)! are a general mechanism explained
     4.9  in \S\ref{sec:styles}.
    4.10  *}
    4.11  
    4.12 @@ -396,10 +396,12 @@
    4.13      \begin{quote}
    4.14      \verb!@!\verb!{thm (style) thm}!\\
    4.15      \verb!@!\verb!{prop (style) thm}!\\
    4.16 -    \verb!@!\verb!{term (style) term}!
    4.17 +    \verb!@!\verb!{term (style) term}!\\
    4.18 +    \verb!@!\verb!{term_type (style) term}!\\
    4.19 +    \verb!@!\verb!{typeof (style) term}!\\
    4.20      \end{quote}
    4.21  
    4.22 -  A ``style'' is a transformation of propositions. There are predefined
    4.23 +  A ``style'' is a transformation of a term. There are predefined
    4.24    styles, namely \verb!lhs! and \verb!rhs!, \verb!prem! with one argument, and \verb!concl!.
    4.25    For example, 
    4.26    the output
    4.27 @@ -441,10 +443,9 @@
    4.28      \verb!\end{center}!
    4.29    \end{quote}
    4.30    Beware that any options must be placed \emph{before}
    4.31 -  the name of the style, as in this example.
    4.32 +  the style, as in this example.
    4.33  
    4.34    Further use cases can be found in \S\ref{sec:yourself}.
    4.35 -
    4.36    If you are not afraid of ML, you may also define your own styles.
    4.37    Have a look at module @{ML_struct Term_Style}.
    4.38  *}
     5.1 --- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Fri Oct 09 09:14:25 2009 +0200
     5.2 +++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Fri Oct 09 10:00:47 2009 +0200
     5.3 @@ -403,7 +403,7 @@
     5.4  \verb!we conclude !\verb!@!\verb!{thm (concl) conjI}!
     5.5  \end{quote}
     5.6  Thus you can rearrange or hide premises and typeset the theorem as you like.
     5.7 -Styles like !(prem 1)! are a general mechanism explained
     5.8 +Styles like \verb!(prem 1)! are a general mechanism explained
     5.9  in \S\ref{sec:styles}.%
    5.10  \end{isamarkuptext}%
    5.11  \isamarkuptrue%
    5.12 @@ -518,10 +518,12 @@
    5.13      \begin{quote}
    5.14      \verb!@!\verb!{thm (style) thm}!\\
    5.15      \verb!@!\verb!{prop (style) thm}!\\
    5.16 -    \verb!@!\verb!{term (style) term}!
    5.17 +    \verb!@!\verb!{term (style) term}!\\
    5.18 +    \verb!@!\verb!{term_type (style) term}!\\
    5.19 +    \verb!@!\verb!{typeof (style) term}!\\
    5.20      \end{quote}
    5.21  
    5.22 -  A ``style'' is a transformation of propositions. There are predefined
    5.23 +  A ``style'' is a transformation of a term. There are predefined
    5.24    styles, namely \verb!lhs! and \verb!rhs!, \verb!prem! with one argument, and \verb!concl!.
    5.25    For example, 
    5.26    the output
    5.27 @@ -563,10 +565,9 @@
    5.28      \verb!\end{center}!
    5.29    \end{quote}
    5.30    Beware that any options must be placed \emph{before}
    5.31 -  the name of the style, as in this example.
    5.32 +  the style, as in this example.
    5.33  
    5.34    Further use cases can be found in \S\ref{sec:yourself}.
    5.35 -
    5.36    If you are not afraid of ML, you may also define your own styles.
    5.37    Have a look at module \verb|Term_Style|.%
    5.38  \end{isamarkuptext}%
     6.1 --- a/src/Pure/Thy/thy_output.ML	Fri Oct 09 09:14:25 2009 +0200
     6.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Oct 09 10:00:47 2009 +0200
     6.3 @@ -443,12 +443,20 @@
     6.4  
     6.5  fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
     6.6  
     6.7 -fun pretty_term_abbrev ctxt t = ProofContext.pretty_term_abbrev (Variable.auto_fixes t ctxt) t;
     6.8 +fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
     6.9 +
    6.10 +fun pretty_term_style ctxt (style, t) =
    6.11 +  pretty_term ctxt (style t);
    6.12  
    6.13 -fun pretty_term_typ ctxt t =
    6.14 -  Syntax.pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t) t);
    6.15 +fun pretty_thm_style ctxt (style, th) =
    6.16 +  pretty_term ctxt (style (Thm.full_prop_of th));
    6.17  
    6.18 -fun pretty_term_typeof ctxt = Syntax.pretty_typ ctxt o Term.fastype_of;
    6.19 +fun pretty_term_typ ctxt (style, t) =
    6.20 +  let val t' = style t
    6.21 +  in pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t) t) end;
    6.22 +
    6.23 +fun pretty_term_typeof ctxt (style, t) =
    6.24 +  Syntax.pretty_typ ctxt (Term.fastype_of (style t));
    6.25  
    6.26  fun pretty_const ctxt c =
    6.27    let
    6.28 @@ -466,15 +474,9 @@
    6.29      val (U, u) = Consts.the_abbreviation (ProofContext.consts_of ctxt) c
    6.30        handle TYPE _ => err ();
    6.31      val t' = Term.betapplys (Envir.expand_atom T (U, u), args);
    6.32 -  in pretty_term_abbrev ctxt (Logic.mk_equals (t, t')) end;
    6.33 -
    6.34 -fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
    6.35 -
    6.36 -fun pretty_term_style ctxt (style, t) =
    6.37 -  pretty_term ctxt (style t);
    6.38 -
    6.39 -fun pretty_thm_style ctxt (style, th) =
    6.40 -  pretty_term_style ctxt (style, Thm.full_prop_of th);
    6.41 +    val eq = Logic.mk_equals (t, t');
    6.42 +    val ctxt' = Variable.auto_fixes eq ctxt;
    6.43 +  in ProofContext.pretty_term_abbrev ctxt' eq end;
    6.44  
    6.45  fun pretty_prf full ctxt = ProofSyntax.pretty_proof_of ctxt full;
    6.46  
    6.47 @@ -522,12 +524,10 @@
    6.48  in
    6.49  
    6.50  val _ = basic_entities_style "thm" (Term_Style.parse -- Attrib.thms) pretty_thm_style;
    6.51 -val _ = basic_entities_style "thm_style" (Term_Style.parse_bare -- Attrib.thms) pretty_thm_style;
    6.52  val _ = basic_entity "prop" (Term_Style.parse -- Args.prop) pretty_term_style;
    6.53  val _ = basic_entity "term" (Term_Style.parse -- Args.term) pretty_term_style;
    6.54 -val _ = basic_entity "term_style" (Term_Style.parse_bare -- Args.term) pretty_term_style;
    6.55 -val _ = basic_entity "term_type" Args.term pretty_term_typ;
    6.56 -val _ = basic_entity "typeof" Args.term pretty_term_typeof;
    6.57 +val _ = basic_entity "term_type" (Term_Style.parse -- Args.term) pretty_term_typ;
    6.58 +val _ = basic_entity "typeof" (Term_Style.parse -- Args.term) pretty_term_typeof;
    6.59  val _ = basic_entity "const" Args.const_proper pretty_const;
    6.60  val _ = basic_entity "abbrev" (Scan.lift Args.name_source) pretty_abbrev;
    6.61  val _ = basic_entity "typ" Args.typ_abbrev Syntax.pretty_typ;
    6.62 @@ -536,6 +536,9 @@
    6.63  val _ = basic_entities "full_prf" Attrib.thms (pretty_prf true);
    6.64  val _ = basic_entity "theory" (Scan.lift Args.name) pretty_theory;
    6.65  
    6.66 +val _ = basic_entities_style "thm_style" (Term_Style.parse_bare -- Attrib.thms) pretty_thm_style;
    6.67 +val _ = basic_entity "term_style" (Term_Style.parse_bare -- Args.term) pretty_term_style;
    6.68 +
    6.69  end;
    6.70  
    6.71