# HG changeset patch # User haftmann # Date 1255010356 -7200 # Node ID dbef0e6438ec4c02fc8734b597b9af2d3e2d9e38 # Parent 9742f6130f10fc2907bf67cc17801aa644bbe557 updated generated documentation diff -r 9742f6130f10 -r dbef0e6438ec doc-src/IsarRef/Thy/document/Document_Preparation.tex --- 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}% diff -r 9742f6130f10 -r dbef0e6438ec doc-src/LaTeXsugar/Sugar/document/Sugar.tex --- 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% %