--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex Thu Oct 08 15:59:15 2009 +0200
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex Thu Oct 08 15:59:16 2009 +0200
@@ -163,8 +163,6 @@
\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}{thm\_style}\hypertarget{antiquotation.thm-style}{\hyperlink{antiquotation.thm-style}{\mbox{\isa{thm{\isacharunderscore}style}}}} & : & \isa{antiquotation} \\
- \indexdef{}{antiquotation}{term\_style}\hypertarget{antiquotation.term-style}{\hyperlink{antiquotation.term-style}{\mbox{\isa{term{\isacharunderscore}style}}}} & : & \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} \\
\indexdef{}{antiquotation}{subgoals}\hypertarget{antiquotation.subgoals}{\hyperlink{antiquotation.subgoals}{\mbox{\isa{subgoals}}}} & : & \isa{antiquotation} \\
@@ -200,16 +198,14 @@
antiquotation:
'theory' options name |
- 'thm' options thmrefs |
+ 'thm' options styles thmrefs |
'lemma' options prop 'by' method |
- 'prop' options prop |
- 'term' options term |
+ 'prop' options styles prop |
+ 'term' options styles term |
'const' options term |
'abbrev' options term |
'typeof' options term |
'typ' options type |
- 'thm\_style' options name thmref |
- 'term\_style' options name term |
'text' options name |
'goals' options |
'subgoals' options |
@@ -223,6 +219,10 @@
;
option: name | name '=' name
;
+ styles: '(' (style + ',') ')'
+ ;
+ style: (name +)
+ ;
\end{rail}
Note that the syntax of antiquotations may \emph{not} include source
@@ -257,12 +257,6 @@
\item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}typ\ {\isasymtau}{\isacharbraceright}{\isachardoublequote}} prints a well-formed type \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}.
- \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}thm{\isacharunderscore}style\ s\ a{\isacharbraceright}{\isachardoublequote}} prints theorem \isa{a},
- previously applying a style \isa{s} to it (see below).
-
- \item \isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term{\isacharunderscore}style\ s\ t{\isacharbraceright}{\isachardoublequote}} prints a well-typed term \isa{t}
- after applying a style \isa{s} to it (see below).
-
\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
to the Isabelle document style, without demanding well-formedness,
e.g.\ small pieces of terms that should not be parsed or
@@ -301,8 +295,10 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Some antiquotations like \isa{thm{\isacharunderscore}style} and \isa{term{\isacharunderscore}style} admit an extra \emph{style} specification to modify the
- printed result. The following standard styles are available:
+The antiquotations \isa{thm}, \isa{prop} and \isa{term} admit an extra \emph{style} specification to modify the
+ printed result. A style is specified by a name with a possibly
+ empty number of arguments; multiple styles can be sequenced with
+ commas. The following standard styles are available:
\begin{description}
@@ -316,8 +312,8 @@
\item \isa{{\isachardoublequote}concl{\isachardoublequote}} extracts the conclusion \isa{C} from a rule
in Horn-clause normal form \isa{{\isachardoublequote}A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C{\isachardoublequote}}.
- \item \isa{{\isachardoublequote}prem{\isadigit{1}}{\isachardoublequote}}, \dots, \isa{{\isachardoublequote}prem{\isadigit{9}}{\isachardoublequote}} extract premise number
- \isa{{\isachardoublequote}{\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isadigit{9}}{\isachardoublequote}}, respectively, from from a rule in Horn-clause
+ \item \isa{{\isachardoublequote}prem{\isachardoublequote}} \isa{n} extract premise number
+ \isa{{\isachardoublequote}n{\isachardoublequote}} from from a rule in Horn-clause
normal form \isa{{\isachardoublequote}A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C{\isachardoublequote}}
\end{description}%
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Thu Oct 08 15:59:15 2009 +0200
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Thu Oct 08 15:59:16 2009 +0200
@@ -390,20 +390,20 @@
own way, you can extract the premises and the conclusion explicitly
and combine them as you like:
\begin{itemize}
-\item \verb!@!\verb!{thm_style prem1! $thm$\verb!}!
-prints premise 1 of $thm$ (and similarly up to \texttt{prem9}).
-\item \verb!@!\verb!{thm_style concl! $thm$\verb!}!
+\item \verb!@!\verb!{thm (prem 1)! $thm$\verb!}!
+prints premise 1 of $thm$.
+\item \verb!@!\verb!{thm (concl)! $thm$\verb!}!
prints the conclusion of $thm$.
\end{itemize}
For example, ``from \isa{Q} and
\isa{P} we conclude \isa{P\ {\isasymand}\ Q}''
is produced by
\begin{quote}
-\verb!from !\verb!@!\verb!{thm_style prem2 conjI}! \verb!and !\verb!@!\verb!{thm_style prem1 conjI}!\\
-\verb!we conclude !\verb!@!\verb!{thm_style concl conjI}!
+\verb!from !\verb!@!\verb!{thm (prem 2) conjI}! \verb!and !\verb!@!\verb!{thm (prem 1) conjI}!\\
+\verb!we conclude !\verb!@!\verb!{thm (concl) conjI}!
\end{quote}
Thus you can rearrange or hide premises and typeset the theorem as you like.
-The \verb!thm_style! antiquotation is a general mechanism explained
+Styles like !(prem 1)! are a general mechanism explained
in \S\ref{sec:styles}.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -516,12 +516,13 @@
``styles'':
\begin{quote}
- \verb!@!\verb!{thm_style stylename thm}!\\
- \verb!@!\verb!{term_style stylename term}!
+ \verb!@!\verb!{thm (style) thm}!\\
+ \verb!@!\verb!{prop (style) thm}!\\
+ \verb!@!\verb!{term (style) term}!
\end{quote}
A ``style'' is a transformation of propositions. There are predefined
- styles, namely \verb!lhs! and \verb!rhs!, \verb!prem1! up to \verb!prem9!, and \verb!concl!.
+ styles, namely \verb!lhs! and \verb!rhs!, \verb!prem! with one argument, and \verb!concl!.
For example,
the output
\begin{center}
@@ -534,8 +535,8 @@
\begin{quote}
\verb!\begin{center}!\\
\verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
- \verb!@!\verb!{thm_style lhs foldl_Nil} & @!\verb!{thm_style rhs foldl_Nil}!\\
- \verb!@!\verb!{thm_style lhs foldl_Cons} & @!\verb!{thm_style rhs foldl_Cons}!\\
+ \verb!@!\verb!{thm (lhs) foldl_Nil} & @!\verb!{thm (rhs) foldl_Nil}!\\
+ \verb!@!\verb!{thm (lhs) foldl_Cons} & @!\verb!{thm (rhs) foldl_Cons}!\\
\verb!\end{tabular}!\\
\verb!\end{center}!
\end{quote}
@@ -558,7 +559,7 @@
type
\begin{quote}
\verb!\begin{center}!\\
- \verb!@!\verb!{thm_style [show_types] concl hd_Cons_tl}!\\
+ \verb!@!\verb!{thm [show_types] (concl) hd_Cons_tl}!\\
\verb!\end{center}!
\end{quote}
Beware that any options must be placed \emph{before}
@@ -567,53 +568,7 @@
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.
- A style is implemented by an ML function of type
- \verb!Proof.context -> term -> term!.
- Have a look at the following example:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\begin{isamarkuptext}%
-\begin{quote}
- \verb!setup {!\verb!*!\\
- \verb!let!\\
- \verb! fun my_concl ctxt = Logic.strip_imp_concl!\\
- \verb! in TermStyle.add_style "my_concl" my_concl!\\
- \verb!end;!\\
- \verb!*!\verb!}!\\
- \end{quote}
-
- \noindent
- This example shows how the \verb!concl! style is implemented
- and may be used as as a ``copy-and-paste'' pattern to write your own styles.
-
- The code should go into your theory file, separate from the \LaTeX\ text.
- The \verb!let! expression avoids polluting the
- ML global namespace. Each style receives the current proof context
- as first argument; this is helpful in situations where the
- style has some object-logic specific behaviour for example.
-
- The mapping from identifier name to the style function
- is done by the \verb|TermStyle.add_style| expression which expects the desired
- style name and the style function as arguments.
-
- After this \verb!setup!,
- there will be a new style available named \verb!my_concl!, thus allowing
- antiquoations like \verb!@!\verb!{thm_style my_concl hd_Cons_tl}!
- yielding \isa{hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}.%
+ Have a look at module \verb|Term_Style|.%
\end{isamarkuptext}%
\isamarkuptrue%
%