# HG changeset patch # User haftmann # Date 1255075247 -7200 # Node ID e871d897969c57c0f93b8839b51fdd0a047af3ec # Parent 2b2c56530d257256c60aaee4236fe35578b5f0a3 term styles also cover antiquotations term_type and typeof diff -r 2b2c56530d25 -r e871d897969c NEWS --- a/NEWS Fri Oct 09 09:14:25 2009 +0200 +++ b/NEWS Fri Oct 09 10:00:47 2009 +0200 @@ -27,7 +27,9 @@ *** document preparation *** * New generalized style concept for printing terms: -write @{foo (style) ...} instead of @{foo_style style ...}. +write @{foo (style) ...} instead of @{foo_style style ...} +(old form is still retained for backward compatibility). +Styles can be also applied for antiquotations prop, term_type and typeof. *** HOL *** diff -r 2b2c56530d25 -r e871d897969c doc-src/IsarRef/Thy/Document_Preparation.thy --- a/doc-src/IsarRef/Thy/Document_Preparation.thy Fri Oct 09 09:14:25 2009 +0200 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Fri Oct 09 10:00:47 2009 +0200 @@ -141,9 +141,10 @@ @{antiquotation_def "lemma"} & : & @{text antiquotation} \\ @{antiquotation_def "prop"} & : & @{text antiquotation} \\ @{antiquotation_def "term"} & : & @{text antiquotation} \\ + @{antiquotation_def term_type} & : & @{text antiquotation} \\ + @{antiquotation_def typeof} & : & @{text antiquotation} \\ @{antiquotation_def const} & : & @{text antiquotation} \\ @{antiquotation_def abbrev} & : & @{text antiquotation} \\ - @{antiquotation_def typeof} & : & @{text antiquotation} \\ @{antiquotation_def typ} & : & @{text antiquotation} \\ @{antiquotation_def "text"} & : & @{text antiquotation} \\ @{antiquotation_def goals} & : & @{text antiquotation} \\ @@ -184,9 +185,10 @@ 'lemma' options prop 'by' method | 'prop' options styles prop | 'term' options styles term | + 'term_type' options styles term | + 'typeof' options styles term | 'const' options term | 'abbrev' options term | - 'typeof' options term | 'typ' options type | 'text' options name | 'goals' options | @@ -230,15 +232,17 @@ \item @{text "@{term t}"} prints a well-typed term @{text "t"}. + \item @{text "@{term_type t}"} prints a well-typed term @{text "t"} + annotated with its type. + + \item @{text "@{typeof t}"} prints the type of a well-typed term + @{text "t"}. + \item @{text "@{const c}"} prints a logical or syntactic constant @{text "c"}. \item @{text "@{abbrev c x\<^sub>1 \ x\<^sub>n}"} prints a constant abbreviation @{text "c x\<^sub>1 \ x\<^sub>n \ rhs"} as defined in the current context. - - \item @{text "@{typeof t}"} prints the type of a well-typed term - @{text "t"}. - \item @{text "@{typ \}"} prints a well-formed type @{text "\"}. \item @{text "@{text s}"} prints uninterpreted source text @{text diff -r 2b2c56530d25 -r e871d897969c doc-src/IsarRef/Thy/document/Document_Preparation.tex --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex Fri Oct 09 09:14:25 2009 +0200 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex Fri Oct 09 10:00:47 2009 +0200 @@ -159,9 +159,10 @@ \indexdef{}{antiquotation}{lemma}\hypertarget{antiquotation.lemma}{\hyperlink{antiquotation.lemma}{\mbox{\isa{lemma}}}} & : & \isa{antiquotation} \\ \indexdef{}{antiquotation}{prop}\hypertarget{antiquotation.prop}{\hyperlink{antiquotation.prop}{\mbox{\isa{prop}}}} & : & \isa{antiquotation} \\ \indexdef{}{antiquotation}{term}\hypertarget{antiquotation.term}{\hyperlink{antiquotation.term}{\mbox{\isa{term}}}} & : & \isa{antiquotation} \\ + \indexdef{}{antiquotation}{term\_type}\hypertarget{antiquotation.term-type}{\hyperlink{antiquotation.term-type}{\mbox{\isa{term{\isacharunderscore}type}}}} & : & \isa{antiquotation} \\ + \indexdef{}{antiquotation}{typeof}\hypertarget{antiquotation.typeof}{\hyperlink{antiquotation.typeof}{\mbox{\isa{typeof}}}} & : & \isa{antiquotation} \\ \indexdef{}{antiquotation}{const}\hypertarget{antiquotation.const}{\hyperlink{antiquotation.const}{\mbox{\isa{const}}}} & : & \isa{antiquotation} \\ \indexdef{}{antiquotation}{abbrev}\hypertarget{antiquotation.abbrev}{\hyperlink{antiquotation.abbrev}{\mbox{\isa{abbrev}}}} & : & \isa{antiquotation} \\ - \indexdef{}{antiquotation}{typeof}\hypertarget{antiquotation.typeof}{\hyperlink{antiquotation.typeof}{\mbox{\isa{typeof}}}} & : & \isa{antiquotation} \\ \indexdef{}{antiquotation}{typ}\hypertarget{antiquotation.typ}{\hyperlink{antiquotation.typ}{\mbox{\isa{typ}}}} & : & \isa{antiquotation} \\ \indexdef{}{antiquotation}{text}\hypertarget{antiquotation.text}{\hyperlink{antiquotation.text}{\mbox{\isa{text}}}} & : & \isa{antiquotation} \\ \indexdef{}{antiquotation}{goals}\hypertarget{antiquotation.goals}{\hyperlink{antiquotation.goals}{\mbox{\isa{goals}}}} & : & \isa{antiquotation} \\ @@ -202,9 +203,10 @@ 'lemma' options prop 'by' method | 'prop' options styles prop | 'term' options styles term | + 'term_type' options styles term | + 'typeof' options styles term | 'const' options term | 'abbrev' options term | - 'typeof' options term | 'typ' options type | 'text' options name | 'goals' options | @@ -246,15 +248,17 @@ \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term\ t{\isacharbraceright}{\isachardoublequote}} prints a well-typed term \isa{{\isachardoublequote}t{\isachardoublequote}}. + \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term{\isacharunderscore}type\ t{\isacharbraceright}{\isachardoublequote}} prints a well-typed term \isa{{\isachardoublequote}t{\isachardoublequote}} + annotated with its type. + + \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typeof\ t{\isacharbraceright}{\isachardoublequote}} prints the type of a well-typed term + \isa{{\isachardoublequote}t{\isachardoublequote}}. + \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}const\ c{\isacharbraceright}{\isachardoublequote}} prints a logical or syntactic constant \isa{{\isachardoublequote}c{\isachardoublequote}}. \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}abbrev\ c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isacharbraceright}{\isachardoublequote}} prints a constant abbreviation \isa{{\isachardoublequote}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ rhs{\isachardoublequote}} as defined in the current context. - - \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typeof\ t{\isacharbraceright}{\isachardoublequote}} prints the type of a well-typed term - \isa{{\isachardoublequote}t{\isachardoublequote}}. - \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typ\ {\isasymtau}{\isacharbraceright}{\isachardoublequote}} prints a well-formed type \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}. \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 diff -r 2b2c56530d25 -r e871d897969c doc-src/LaTeXsugar/Sugar/Sugar.thy --- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Fri Oct 09 09:14:25 2009 +0200 +++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Fri Oct 09 10:00:47 2009 +0200 @@ -309,7 +309,7 @@ \verb!we conclude !\verb!@!\verb!{thm (concl) conjI}! \end{quote} Thus you can rearrange or hide premises and typeset the theorem as you like. -Styles like !(prem 1)! are a general mechanism explained +Styles like \verb!(prem 1)! are a general mechanism explained in \S\ref{sec:styles}. *} @@ -396,10 +396,12 @@ \begin{quote} \verb!@!\verb!{thm (style) thm}!\\ \verb!@!\verb!{prop (style) thm}!\\ - \verb!@!\verb!{term (style) term}! + \verb!@!\verb!{term (style) term}!\\ + \verb!@!\verb!{term_type (style) term}!\\ + \verb!@!\verb!{typeof (style) term}!\\ \end{quote} - A ``style'' is a transformation of propositions. There are predefined + A ``style'' is a transformation of a term. There are predefined styles, namely \verb!lhs! and \verb!rhs!, \verb!prem! with one argument, and \verb!concl!. For example, the output @@ -441,10 +443,9 @@ \verb!\end{center}! \end{quote} Beware that any options must be placed \emph{before} - the name of the style, as in this example. + the style, as in this example. Further use cases can be found in \S\ref{sec:yourself}. - If you are not afraid of ML, you may also define your own styles. Have a look at module @{ML_struct Term_Style}. *} diff -r 2b2c56530d25 -r e871d897969c doc-src/LaTeXsugar/Sugar/document/Sugar.tex --- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Fri Oct 09 09:14:25 2009 +0200 +++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Fri Oct 09 10:00:47 2009 +0200 @@ -403,7 +403,7 @@ \verb!we conclude !\verb!@!\verb!{thm (concl) conjI}! \end{quote} Thus you can rearrange or hide premises and typeset the theorem as you like. -Styles like !(prem 1)! are a general mechanism explained +Styles like \verb!(prem 1)! are a general mechanism explained in \S\ref{sec:styles}.% \end{isamarkuptext}% \isamarkuptrue% @@ -518,10 +518,12 @@ \begin{quote} \verb!@!\verb!{thm (style) thm}!\\ \verb!@!\verb!{prop (style) thm}!\\ - \verb!@!\verb!{term (style) term}! + \verb!@!\verb!{term (style) term}!\\ + \verb!@!\verb!{term_type (style) term}!\\ + \verb!@!\verb!{typeof (style) term}!\\ \end{quote} - A ``style'' is a transformation of propositions. There are predefined + A ``style'' is a transformation of a term. There are predefined styles, namely \verb!lhs! and \verb!rhs!, \verb!prem! with one argument, and \verb!concl!. For example, the output @@ -563,10 +565,9 @@ \verb!\end{center}! \end{quote} Beware that any options must be placed \emph{before} - the name of the style, as in this example. + the style, as in this example. Further use cases can be found in \S\ref{sec:yourself}. - If you are not afraid of ML, you may also define your own styles. Have a look at module \verb|Term_Style|.% \end{isamarkuptext}% diff -r 2b2c56530d25 -r e871d897969c src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Fri Oct 09 09:14:25 2009 +0200 +++ b/src/Pure/Thy/thy_output.ML Fri Oct 09 10:00:47 2009 +0200 @@ -443,12 +443,20 @@ fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t; -fun pretty_term_abbrev ctxt t = ProofContext.pretty_term_abbrev (Variable.auto_fixes t ctxt) t; +fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of; + +fun pretty_term_style ctxt (style, t) = + pretty_term ctxt (style t); -fun pretty_term_typ ctxt t = - Syntax.pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t) t); +fun pretty_thm_style ctxt (style, th) = + pretty_term ctxt (style (Thm.full_prop_of th)); -fun pretty_term_typeof ctxt = Syntax.pretty_typ ctxt o Term.fastype_of; +fun pretty_term_typ ctxt (style, t) = + let val t' = style t + in pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t) t) end; + +fun pretty_term_typeof ctxt (style, t) = + Syntax.pretty_typ ctxt (Term.fastype_of (style t)); fun pretty_const ctxt c = let @@ -466,15 +474,9 @@ val (U, u) = Consts.the_abbreviation (ProofContext.consts_of ctxt) c handle TYPE _ => err (); val t' = Term.betapplys (Envir.expand_atom T (U, u), args); - in pretty_term_abbrev ctxt (Logic.mk_equals (t, t')) end; - -fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of; - -fun pretty_term_style ctxt (style, t) = - pretty_term ctxt (style t); - -fun pretty_thm_style ctxt (style, th) = - pretty_term_style ctxt (style, Thm.full_prop_of th); + val eq = Logic.mk_equals (t, t'); + val ctxt' = Variable.auto_fixes eq ctxt; + in ProofContext.pretty_term_abbrev ctxt' eq end; fun pretty_prf full ctxt = ProofSyntax.pretty_proof_of ctxt full; @@ -522,12 +524,10 @@ in val _ = basic_entities_style "thm" (Term_Style.parse -- Attrib.thms) pretty_thm_style; -val _ = basic_entities_style "thm_style" (Term_Style.parse_bare -- Attrib.thms) pretty_thm_style; val _ = basic_entity "prop" (Term_Style.parse -- Args.prop) pretty_term_style; val _ = basic_entity "term" (Term_Style.parse -- Args.term) pretty_term_style; -val _ = basic_entity "term_style" (Term_Style.parse_bare -- Args.term) pretty_term_style; -val _ = basic_entity "term_type" Args.term pretty_term_typ; -val _ = basic_entity "typeof" Args.term pretty_term_typeof; +val _ = basic_entity "term_type" (Term_Style.parse -- Args.term) pretty_term_typ; +val _ = basic_entity "typeof" (Term_Style.parse -- Args.term) pretty_term_typeof; val _ = basic_entity "const" Args.const_proper pretty_const; val _ = basic_entity "abbrev" (Scan.lift Args.name_source) pretty_abbrev; val _ = basic_entity "typ" Args.typ_abbrev Syntax.pretty_typ; @@ -536,6 +536,9 @@ val _ = basic_entities "full_prf" Attrib.thms (pretty_prf true); val _ = basic_entity "theory" (Scan.lift Args.name) pretty_theory; +val _ = basic_entities_style "thm_style" (Term_Style.parse_bare -- Attrib.thms) pretty_thm_style; +val _ = basic_entity "term_style" (Term_Style.parse_bare -- Args.term) pretty_term_style; + end;