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_typ ctxt t =
6.11 - Syntax.pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t) t);
6.12 +fun pretty_term_style ctxt (style, t) =
6.13 + pretty_term ctxt (style t);
6.14
6.15 -fun pretty_term_typeof ctxt = Syntax.pretty_typ ctxt o Term.fastype_of;
6.16 +fun pretty_thm_style ctxt (style, th) =
6.17 + pretty_term ctxt (style (Thm.full_prop_of th));
6.18 +
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