summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/source/latex/stex/sproof/sproof.dtx
diff options
context:
space:
mode:
Diffstat (limited to 'Master/texmf-dist/source/latex/stex/sproof/sproof.dtx')
-rw-r--r--Master/texmf-dist/source/latex/stex/sproof/sproof.dtx139
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