--- 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 ***
--- 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 \<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 "@{typeof t}"} prints the type of a well-typed term
- @{text "t"}.
-
\item @{text "@{typ \<tau>}"} prints a well-formed type @{text "\<tau>"}.
\item @{text "@{text s}"} prints uninterpreted source text @{text
--- 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
--- 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}.
*}
--- 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}%
--- 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;