diff options
Diffstat (limited to 'Master/texmf-dist/source/latex/stex/sproof/sproof.dtx')
-rw-r--r-- | Master/texmf-dist/source/latex/stex/sproof/sproof.dtx | 139 |
1 files changed, 98 insertions, 41 deletions
diff --git a/Master/texmf-dist/source/latex/stex/sproof/sproof.dtx b/Master/texmf-dist/source/latex/stex/sproof/sproof.dtx index dbfb53e897f..bb4f6b04a0e 100644 --- a/Master/texmf-dist/source/latex/stex/sproof/sproof.dtx +++ b/Master/texmf-dist/source/latex/stex/sproof/sproof.dtx @@ -6,8 +6,8 @@ % % The development version of this file can be found at % $URL: https://svn.kwarc.info/repos/stex/trunk/sty/sproof/sproof.dtx $ -% $Rev: 1502 $; last modified by $Author: kohlhase $ -% $Date: 2010-07-20 10:17:00 +0200 (Tue, 20 Jul 2010) $ +% $Rev: 1671 $; last modified by $Author: kohlhase $ +% $Date: 2010-11-06 08:05:15 +0100 (Sat, 06 Nov 2010) $ % \fi % % \iffalse @@ -23,17 +23,18 @@ \usepackage{../ctansvn} \usepackage{hyperref} \usepackage[eso-foot,today]{svninfo} -\svnInfo $Id: sproof.dtx 1502 2010-07-20 08:17:00Z kohlhase $ +\svnInfo $Id: sproof.dtx 1671 2010-11-06 07:05:15Z kohlhase $ \svnKeyword $HeadURL: https://svn.kwarc.info/repos/stex/trunk/sty/sproof/sproof.dtx $ \makeindex \floatstyle{boxed} \newfloat{exfig}{thp}{lop} \floatname{exfig}{Example} +\def\tracissue#1{\cite{sTeX:online}, \hyperlink{http://trac.kwarc.info/sTeX/ticket/#1}{issue #1}} \begin{document}\DocInput{sproof.dtx}\end{document} %</driver> % \fi % -% \CheckSum{279} +% \iffalse\CheckSum{279}\fi % % \changes{v0.9}{2005/06/14}{First Version with Documentation} % \changes{v0.9a}{2005/07/01}{Completed Documentation} @@ -149,6 +150,12 @@ % % \section{The User Interface} % +% \subsection{Package Options}\label{sec:user:options} +% +% The |sproofs| package takes a single option: \DescribeMacro{showmeta}|showmeta|. If +% this is set, then the metadata keys are shown (see~\cite{Kohlhase:metakeys:ctan} for details +% and customization options). +% % \subsection{Proofs and Proof steps} % % \DescribeEnv{sproof} The |proof| environment is the main container for proofs. It takes @@ -217,7 +224,7 @@ % \begin{spfstep}[type=conclusion] % We can \begin{justification}[method=simplify-eq] % simplify the {\justarg[rhs]{right-hand side}} -% \end{justification} to ${k+1}^2$, which proves the assertion. +% \end{justification} to $(k+1)^2$, which proves the assertion. % \end{spfstep} % \end{spfcase} % \begin{spfstep}[type=conclusion] @@ -288,7 +295,34 @@ % this wastes space (especially, if a proof ends in a case analysis which will supply its % own proof end marker). To suppress it locally, just set |proofend={}| in them or use use % |\sProofEndSymbol{}|. -% +% +% \subsection{Configuration of the Presentation}\label{sec:user:conf} +% +% Finally, we provide configuration hooks in Figure~\ref{fig:hooks} for the keywords in +% proofs. These are mainly intended for package authors building on |statements|, e.g. for +% multi-language support.\ednote{we might want to develop an extension +% \texttt{sproof-babel} in the future.}. +%\begin{figure}[ht]\centering +% \begin{tabular}{|lll|}\hline +% Environment & configuration macro & value\\\hline\hline +% \texttt{proof} & \texttt{\textbackslash spf@proof@kw} & \makeatletter\spf@proof@kw\\\hline +% \texttt{sketchproof} & \texttt{\textbackslash spf@sketchproof@kw} & \makeatletter\spf@proofsketch@kw\\\hline +% \end{tabular} +% \caption{Configuration Hooks for Semantic Proof Markup}\label{fig:hooks} +% \end{figure} +% +% \section{Limitations}\label{sec:limitations} +% +% In this section we document known limitations. If you want to help alleviate them, +% please feel free to contact the package author. Some of them are currently discussed in +% the TRAC. +% \begin{compactenum} +% \item The numbering scheme of proofs cannot be changed. It is more geared for teaching +% proof structures (the author's main use case) and not for writing papers.\lec{reported +% by Tobias Pfeiffer; see \tracissue{1658}} +% \end{compactenum} +% +% % \StopEventually{\newpage\PrintIndex\newpage\PrintChanges\printbibliography} % \newpage % @@ -312,7 +346,24 @@ use LaTeXML::Package; RequirePackage('sref'); %</ltxml> % \end{macrocode} -% Then we make sure that the {\stex} |sref| package is loaded~\ctancite{Kohlhase:sref}. +% +% \subsection{Package Options}\label{sec:impl:options} +% +% We declare some switches which will modify the behavior according to the package +% options. Generally, an option |xxx| will just set the appropriate switches to true +% (otherwise they stay false).\ednote{need an implementation for {\latexml}} +% +% \begin{macrocode} +%<*package> +\DeclareOption{showmeta}{\PassOptionsToPackage{\CurrentOption}{metakeys}} +\ProcessOptions +%</package> +%<*ltxml> +DeclareOption('showmeta',''); +%</ltxml> +% \end{macrocode} +% +% Then we make sure that the |sref| package is loaded~\ctancite{Kohlhase:sref}. % \begin{macrocode} %<*package> \RequirePackage{sref} @@ -325,13 +376,13 @@ RequirePackage('sref'); % \begin{macrocode} %<*package> \srefaddidkey{spf} -\omdaddkey{spf}{display} -\omdaddkey{spf}{for} -\omdaddkey{spf}{from} -\omdaddkey[\sproof@box]{spf}{proofend} -\omdaddkey{spf}{type} -\omdaddkey{spf}{title} -\omdaddkey{spf}{continues} +\addmetakey*{spf}{display} +\addmetakey{spf}{for} +\addmetakey{spf}{from} +\addmetakey*[\sproof@box]{spf}{proofend} +\addmetakey{spf}{type} +\addmetakey*{spf}{title} +\addmetakey{spf}{continues} %</package> % \end{macrocode} % @@ -397,17 +448,16 @@ RequirePackage('sref'); % \begin{macro}{spfsketch} % \begin{macrocode} %<*package> -\newcommand{\spfsketch}[2][]{\omdsetkeys{spf}{#1}\sref@target -\ifx\spf@display\spf@flow\else{\stDMemph{\ifx\spf@type\@empty{Proof}\else\spf@type\fi}:}\fi{ #2}% -\sref@label@id{this \ifx\spf@type\@empty{Proof}\else\spf@type\fi}} +\def\spf@proofsketch@kw{Proof Sketch} +\newcommand{\spfsketch}[2][]{\metasetkeys{spf}{#1}\sref@target +\ifx\spf@display\spf@flow\else{\stDMemph{\ifx\spf@type\@empty\spf@proofsketch@kw\else\spf@type\fi}:}\fi{ #2}% +\sref@label@id{this \ifx\spf@type\@empty\spf@proofsketch@kw\else\spf@type\fi}} %</package> %<*ltxml> DefConstructor('\spfsketch OptionalKeyVals:pf{}', "<omdoc:proof " . "?&defined(&KeyVal(#1,'id'))(xml:id='&KeyVal(#1,'id')')()>\n" - . "?#2(<omdoc:omtext>" - . "<omdoc:CMP><omdoc:p>#2</omdoc:p></omdoc:CMP>" - . "</omdoc:omtext>\n)()" + . "?#2(<omdoc:omtext><omdoc:CMP><omdoc:p>#2\n)()" . "</omdoc:proof>\n"); DefConstructor('\sProofEndSymbol {}',''); %</ltxml> @@ -420,10 +470,11 @@ DefConstructor('\sProofEndSymbol {}',''); % proof, we position the proof end into the last line. % \begin{macrocode} %<*package> -\newenvironment{@proof}[2][]{\omdsetkeys{spf}{#1}\sref@target +\def\spf@proof@kw{Proof} +\newenvironment{@proof}[2][]{\metasetkeys{spf}{#1}\sref@target \count10=10 -\ifx\spf@display\spf@flow\else{\stDMemph{\ifx\spf@type\@empty{Proof}\else\spf@type\fi}:}\fi{ #2}% -\sref@label@id{this \ifx\spf@type\@empty{Proof}\else\spf@type\fi} +\ifx\spf@display\spf@flow\else{\stDMemph{\ifx\spf@type\@empty\spf@proof@kw\else\spf@type\fi}:}\fi{ #2}% +\sref@label@id{this \ifx\spf@type\@empty\spf@proof@kw\else\spf@type\fi} \def\pst@label{}\newcount\pst@count% initialize the labeling mechanism \begin{description}\begin{pst@with@label}{P}} {\end{pst@with@label}\end{description}} @@ -436,7 +487,7 @@ DefCMPEnvironment('{sproof} OptionalKeyVals:pf{}', . "?&KeyVal(#1,'for')(for='&hash_wrapper(&KeyVal(#1,'for'))')()" . "?&defined(&KeyVal(#1,'id'))(xml:id='&KeyVal(#1,'id')')()>\n" . "?#2(<omdoc:omtext>" - . "<omdoc:CMP><omdoc:p>#2</omdoc:p></omdoc:CMP>" + . "<omdoc:CMP><omdoc:p>#2</omdoc:CMP>" . "</omdoc:omtext>\n)()" . "#body" . "</omdoc:proof>\n"); @@ -449,7 +500,7 @@ DefMacro('\endsProof','\endsproof'); % \begin{environment}{spfidea} % \begin{macrocode} %<*package> -\newcommand{\spfidea}[2][]{\omdsetkeys{spf}{#1}% +\newcommand{\spfidea}[2][]{\metasetkeys{spf}{#1}% \stDMemph{\ifx\spf@type\@empty{Proof Idea}\else\spf@type\fi:} #2\sproofend} %</package> %<*ltxml> @@ -457,7 +508,7 @@ DefCMPConstructor('\spfidea OptionalKeyVals:pf {}', "<omdoc:proof " . "?&defined(&KeyVal(#1,'id'))(xml:id='&KeyVal(#1,'id')')()" . "?&KeyVal(#1,'for')(for='&hash_wrapper(&KeyVal(#1,'for'))')()>\n" - . "<omdoc:omtext><omdoc:CMP><omdoc:p>#2</omdoc:p></omdoc:CMP></omdoc:omtext>\n" + . "<omdoc:omtext><omdoc:CMP><omdoc:p>#2</omdoc:omtext>\n" . "</omdoc:proof>\n"); %</ltxml> % \end{macrocode} @@ -471,7 +522,7 @@ DefCMPConstructor('\spfidea OptionalKeyVals:pf {}', % \begin{environment}{spfstep} % \begin{macrocode} %<*package> -\newenvironment{spfstep}[1][]{\omdsetkeys{spf}{#1} +\newenvironment{spfstep}[1][]{\metasetkeys{spf}{#1} \ifx\spf@display\spf@flow\else\item[\the@pst@label]\fi \ifx\spf@title\@empty\else{(\stDMemph{\spf@title})}\fi} {\next@pst@label} @@ -492,7 +543,7 @@ DefCMPEnvironment('{spfstep} OptionalKeyVals:pf', % \begin{environment}{sproofcomment} % \begin{macrocode} %<*package> -\newenvironment{sproofcomment}[1][]{\omdsetkeys{spf}{#1} +\newenvironment{sproofcomment}[1][]{\metasetkeys{spf}{#1} \ifx\spf@display\spf@flow\else\item[\the@pst@label]\fi} {\next@pst@label} %</package> @@ -500,7 +551,7 @@ DefCMPEnvironment('{spfstep} OptionalKeyVals:pf', DefCMPEnvironment('{sproofcomment} OptionalKeyVals:pf', "<omdoc:omtext " . "?&defined(&KeyVal(#1,'id'))(xml:id='&KeyVal(#1,'id')')()>" - . "<omdoc:CMP><omdoc:p>#body</omdoc:p></omdoc:CMP>" + . "<omdoc:CMP><omdoc:p>#body</omdoc:CMP>" . "</omdoc:omtext>"); %</ltxml> % \end{macrocode} @@ -514,7 +565,7 @@ DefCMPEnvironment('{sproofcomment} OptionalKeyVals:pf', % proof. % \begin{macrocode} %<*package> -\newenvironment{spfcases}[2][]{\omdsetkeys{spf}{#1} +\newenvironment{spfcases}[2][]{\metasetkeys{spf}{#1} \def\@test{#2}\ifx\@test\empty\else \ifx\spf@display\spf@flow {#2}\else\item[\the@pst@label]{#2} \fi\fi \begin{pst@with@label}{\pst@label.\number\count\count10}} @@ -524,7 +575,7 @@ DefCMPEnvironment('{sproofcomment} OptionalKeyVals:pf', DefEnvironment('{spfcases} OptionalKeyVals:pf {}', "<omdoc:derive " . "?&defined(&KeyVal(#1,'id'))(xml:id='&KeyVal(#1,'id')')()>\n" - . "<omdoc:CMP><omdoc:p>#2</omdoc:p></omdoc:CMP>\n" + . "<omdoc:CMP><omdoc:p>#2</omdoc:CMP>\n" . "<omdoc:method xref='#proof-by-cases'>#body</omdoc:method>" . "</omdoc:derive>\n"); %</ltxml> @@ -536,7 +587,7 @@ DefEnvironment('{spfcases} OptionalKeyVals:pf {}', % after the |\item| % \begin{macrocode} %<*package> -\newenvironment{spfcase}[2][]{\omdsetkeys{spf}{#1} +\newenvironment{spfcase}[2][]{\metasetkeys{spf}{#1} \ifx\spf@display\spf@flow\else\item[\the@pst@label]\fi \def\@test{#2}\ifx\@test\@empty\else{\stDMemph{#2}:}\fi \begin{pst@with@label}{\pst@label.\number\count\count10}} @@ -547,7 +598,7 @@ DefEnvironment('{spfcase} OptionalKeyVals:pf{}', "<omdoc:proof " . "?&defined(&KeyVal(#1,'id'))(xml:id='&KeyVal(#1,'id')')()>\n" . "?#2(<omdoc:omtext>" - . "<omdoc:CMP><omdoc:p>#2</omdoc:p></omdoc:CMP>" + . "<omdoc:CMP><omdoc:p>#2</omdoc:CMP>" . "</omdoc:omtext>\n)()" . "#body" . "</omdoc:proof>\n"); @@ -560,12 +611,18 @@ DefEnvironment('{spfcase} OptionalKeyVals:pf{}', % started.\ednote{document this above} % \begin{macrocode} %<*package> -\newenvironment{subproof}{\begin{pst@with@label}{\pst@label.\number\count\count10}} +\newenvironment{subproof}[1][]% +{\begin{pst@with@label}{\pst@label.\number\count\count10}} {\ifx\spf@display\spf@flow\else\sproofend\fi\end{pst@with@label}} %</package> %<*ltxml> -DefEnvironment('{subproof}', - "<omdoc:proof>\n #body\n</omdoc:proof>\n"); +DefEnvironment('{subproof}[]', + "<omdoc:derive>" + . "?#1(<omdoc:CMP><omdoc:p>#1</omdoc:CMP>)()" + . "<omdoc:method>" + . "<omdoc:proof>\n #body\n</omdoc:proof>" + . "</omdoc:method>" + ."</omdoc:derive>"); %</ltxml> % \end{macrocode} % \end{environment} @@ -578,9 +635,9 @@ DefEnvironment('{subproof}', % \begin{macrocode} %<*package> \srefaddidkey{just} -\omdaddkey{just}{method} -\omdaddkey{just}{premises} -\omdaddkey{just}{args} +\addmetakey{just}{method} +\addmetakey{just}{premises} +\addmetakey{just}{args} %</package> %<*ltxml> DefKeyVal('just','id','Semiverbatim'); @@ -721,6 +778,6 @@ Tag('omdoc:derive',afterOpen=>\&numberIt,afterClose=>\&locateIt); % LocalWords: spfidea spfsketch spfsketch spfstep justarg spfcases spfcase rhs % LocalWords: sproofcomment ind-hyp splitit arith byindhyp sproofend proofend % LocalWords: printbibliography textsf langle textsf langle ltxml ctancite spf -% LocalWords: srefaddidkey omdaddkey pf.sty newenvironment hbox vrule vbox ifx +% LocalWords: srefaddidkey pf.sty newenvironment hbox vrule vbox ifx % LocalWords: hrule vskip hrule vrule hfil nobreak hfill smallskip newcommand -% LocalWords: omdsetkeys stDMemph newcount endsproof xref doctex +% LocalWords: stDMemph newcount endsproof xref doctex |