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.dtx511
1 files changed, 223 insertions, 288 deletions
diff --git a/Master/texmf-dist/source/latex/stex/sproof/sproof.dtx b/Master/texmf-dist/source/latex/stex/sproof/sproof.dtx
index ca5baa3660c..8224760461f 100644
--- a/Master/texmf-dist/source/latex/stex/sproof/sproof.dtx
+++ b/Master/texmf-dist/source/latex/stex/sproof/sproof.dtx
@@ -1,30 +1,28 @@
-% \iffalse meta-comment
+% \iffalse meta-comment
% An Infrastructure for Structural Markup for Proofs
% Copyright (C) 2004-2011 Michael Kohlhase, all rights reserved
% this file is released under the
% LaTeX Project Public License (LPPL)
%
-% The development version of this file can be found at
-% $URL: https://svn.kwarc.info/repos/stex/trunk/sty/sproof/sproof.dtx $
-% $Rev: 1999 $; last modified by $Author: kohlhase $
-% $Date: 2012-01-28 08:32:11 +0100 (Sat, 28 Jan 2012) $
+% The original of this file is in the public repository at
+% http://github.com/KWARC/sTeX/
% \fi
%
% \iffalse
%<package>\NeedsTeXFormat{LaTeX2e}[1999/12/01]
-%<package>\ProvidesPackage{sproof}[2012/01/28 v1.0 Semantic Markup for Proofs]
+%<package>\ProvidesPackage{sproof}[2016/04/07 v1.1 Semantic Markup for Proofs]
%
%<*driver>
\documentclass{ltxdoc}
\usepackage{url,array,stex,float,moreverb}
\usepackage[show]{ed}
\usepackage[hyperref=auto,style=alphabetic]{biblatex}
-\bibliography{kwarc}
-\usepackage{../ctansvn}
+\addbibresource{kwarcpubs.bib}
+\addbibresource{extpubs.bib}
+\addbibresource{kwarccrossrefs.bib}
+\addbibresource{extcrossrefs.bib}
+\usepackage{ctangit}
\usepackage{hyperref}
-\usepackage[eso-foot,today]{svninfo}
-\svnInfo $Id: sproof.dtx 1999 2012-01-28 07:32:11Z kohlhase $
-\svnKeyword $HeadURL: https://svn.kwarc.info/repos/stex/trunk/sty/sproof/sproof.dtx $
\makeindex
\floatstyle{boxed}
\newfloat{exfig}{thp}{lop}
@@ -34,7 +32,7 @@
%</driver>
% \fi
%
-% \CheckSum{315}
+% \CheckSum{341}
%
% \changes{v0.9}{2005/06/14}{First Version with Documentation}
% \changes{v0.9a}{2005/07/01}{Completed Documentation}
@@ -46,6 +44,7 @@
% \changes{v0.9f}{2009/12/14}{changing to omd metadata framework}
% \changes{v0.9f}{2008/12/14}{first steps to sref}
% \changes{v1.0}{2011/01/23}{making proof step labels stylable}
+% \changes{v1.1}{2013/09/29}{subproof now more like proof (takes comment arg)}
%
% \GetFileInfo{sproof.sty}
%
@@ -127,7 +126,9 @@
% \end{spfstep}
% \begin{spfstep}
% Thus we have $\sum_{i=1}^{k+1}{(2i-1)}=k^2+2k+1$
-% \begin{justification}[method=fertilize] by inductive hypothesis.\end{justification}
+% \begin{justification}[method=fertilize]
+% by inductive hypothesis.
+% \end{justification}
% \end{spfstep}
% \begin{spfstep}[type=conclusion]
% We can \begin{justification}[method=simplify]simplify\end{justification}
@@ -262,16 +263,24 @@
%
% \subsection{Proof Structure}
%
+% \DescribeEnv{subproof} The |pfcases| environment is used to mark up a subproof. This
+% environment takes an optional |KeyVal| argument for semantic annotations and a second
+% argument that allows to specify an introductory comment (just like in the |proof|
+% environment). The \DescribeMacro{method}|method| key can be used to give the name of the
+% proof method executed to make this subproof.
+%
% \DescribeEnv{spfcases} The |pfcases| environment is used to mark up a proof by
-% cases. This environment takes an optional |KeyVal| argument for semantic annotations and
-% a second argument that allows to specify an introductory comment (just like in the
-% |proof| environment).
+% cases. Technically it is a variant of the |subproof| where the |method| is
+% |by-cases|. Its contents are |spfcase| environments that mark up the cases one by one.
%
% \DescribeEnv{spfcase} The content of a |pfcases| environment are a sequence of case
% proofs marked up in the |pfcase| environment, which takes an optional |KeyVal| argument
% for semantic annotations. The second argument is used to specify the the description of
% the case under consideration. The content of a |pfcase| environment is the same as that
-% of a |proof|, i.e. |step|s, |proofcomment|s, and |pfcases| environments.
+% of a |proof|, i.e. |step|s, |proofcomment|s, and |pfcases|
+% environments. \DescribeMacro{\spfcasesketch}|\spfcasesketch| is a variant of the |spfcase|
+% environment that takes the same arguments, but instead of the |spfstep|s in the body
+% uses a third argument for a proof sketch.
%
% \DescribeEnv{sproofcomment} The |proofcomment| environment is much like a |step|, only
% that it does not have an object-level assertion of its own. Rather than asserting some
@@ -306,7 +315,7 @@
%\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{sproof} & \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}
@@ -355,25 +364,6 @@
%
% \section{The Implementation}
%
-% The |sproof| package generates to files: the {\LaTeX} package (all the code between
-% {\textsf{$\langle$*package$\rangle$}} and {\textsf{$\langle$/package$\rangle$}}) and the
-% {\latexml} bindings (between {\textsf{$\langle$*ltxml$\rangle$}} and
-% {\textsf{$\langle$/ltxml$\rangle$}}). We keep the corresponding code fragments together,
-% since the documentation applies to both of them and to prevent them from getting out of
-% sync.
-%
-% We first set up the Perl Packages for {\latexml}
-%
-% \begin{macrocode}
-%<*ltxml>
-# -*- CPERL -*-
-package LaTeXML::Package::Pool;
-use strict;
-use LaTeXML::Package;
-RequirePackage('sref');
-%</ltxml>
-% \end{macrocode}
-%
% \subsection{Package Options}\label{sec:impl:options}
%
% We declare some switches which will modify the behavior according to the package
@@ -382,26 +372,21 @@ RequirePackage('sref');
%
% \begin{macrocode}
%<*package>
-\DeclareOption{showmeta}{\PassOptionsToPackage{\CurrentOption}{metakeys}}
+\DeclareOption*{\PassOptionsToPackage{\CurrentOption}{sref}}
\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}
-%</package>
+\RequirePackage{etoolbox}
+\RequirePackage[base]{babel}
% \end{macrocode}
%
% \subsection{Proofs}\label{sec:impl:proofs}
%
% We first define some keys for the |proof| environment.
% \begin{macrocode}
-%<*package>
\srefaddidkey{spf}
\addmetakey*{spf}{display}
\addmetakey{spf}{for}
@@ -411,13 +396,13 @@ DeclareOption('showmeta','');
\addmetakey*{spf}{title}
\addmetakey{spf}{continues}
\addmetakey{spf}{functions}
-%</package>
+\addmetakey{spf}{method}
% \end{macrocode}
%
% \begin{macro}{\spf@flow}
% We define this macro, so that we can test whether the |display| key has the value |flow|
% \begin{macrocode}
-%<package>\def\spf@flow{flow}
+\def\spf@flow{flow}
% \end{macrocode}
% \end{macro}
%
@@ -440,36 +425,64 @@ DeclareOption('showmeta','');
% |\count\count10| with 1. In the end call for this environment, we just decrease the
% proof depth counter by 1 again.
% \begin{macrocode}
-%<*package>
-\newenvironment{pst@with@label}[1]%
-{\edef\pst@label{#1}\advance\count10 by 1\count\count10=1}
-{\advance\count10 by -1}
+\newenvironment{pst@with@label}[1]{%
+ \edef\pst@label{#1}%
+ \advance\count10 by 1%
+ \count\count10=1%
+}{%
+ \advance\count10 by -1%
+}%
% \end{macrocode}
% \end{environment}
%
% \begin{macro}{\the@pst@label}
% |\the@pst@label| evaluates to the current step label.
% \begin{macrocode}
-\def\the@pst@label{\pst@make@label\pst@label{\number\count\count10}}
+\def\the@pst@label{%
+ \pst@make@label\pst@label{\number\count\count10}\pstlabel@postfix%
+}%
+% \end{macrocode}
+%\end{macro}
+%
+% \begin{macro}{\setpstlabelstyle}
+% |\setpstlabelstyle{|meta{Key-Val pairs}|}| makes the labeling style customizable.
+% |\setpstlabelstyle{prefix=Pr,delimiter=-,postfix=\dag}| will change the labeling style
+% from \textbf{P.1.2.3} to \textbf{Pr-1-2-3\dag}. |\setpstlabelstyledefault| will set the
+% labeling style back to default.
+% \begin{macrocode}
+\addmetakey[P]{pstlabel}{prefix}[]
+\addmetakey[.]{pstlabel}{delimiter}[]
+\addmetakey[]{pstlabel}{postfix}[]
+\metasetkeys{pstlabel}{}% initialization
+\newrobustcmd\setpstlabelstyle[1]{%
+ \metasetkeys{pstlabel}{#1}%
+}%
+\newrobustcmd\setpstlabelstyledefault{%
+ \metasetkeys{pstlabel}{prefix=P,delimiter=.,postfix=}%
+}%
% \end{macrocode}
%\end{macro}
%
% \begin{macro}{\pstlabelstyle}
-% |\pstlabelstyle| just sets the |\pst@make@label| macro according to the style.
+% |\pstlabelstyle| just sets the |\pst@make@label| macro according to the style.
% \begin{macrocode}
-\def\pst@make@label@long#1#2{\@for\@I:=#1\do{\@I.}#2}
+\def\pst@make@label@long#1#2{\@for\@I:=#1\do{\expandafter\@I\pstlabel@delimiter}#2}
\def\pst@make@label@angles#1#2{\ensuremath{\@for\@I:=#1\do{\rangle}}#2}
\def\pst@make@label@short#1#2{#2}
\def\pst@make@label@empty#1#2{}
-\def\pstlabelstyle#1{\def\pst@make@label{\@nameuse{pst@make@label@#1}}}
-\pstlabelstyle{long}
+\def\pstlabelstyle#1{%
+ \def\pst@make@label{\@nameuse{pst@make@label@#1}}%
+}%
+\pstlabelstyle{long}%
% \end{macrocode}
%\end{macro}
%
% \begin{macro}{\next@pst@label}
% |\next@pst@label| increments the step label at the current level.
% \begin{macrocode}
-\def\next@pst@label{\global\advance\count\count10 by 1}
+\def\next@pst@label{%
+ \global\advance\count\count10 by 1%
+}%
% \end{macrocode}
%\end{macro}
%
@@ -477,39 +490,62 @@ DeclareOption('showmeta','');
% This macro places a little box at the end of the line if there is space, or at the
% end of the next line if there isn't
% \begin{macrocode}
-\def\sproof@box{\hbox{\vrule\vbox{\hrule width 6 pt\vskip 6pt\hrule}\vrule}}
-\def\spf@proofend{\sproof@box}
-\def\sproofend{\ifx\spf@proofend\@empty\else\hfil\null\nobreak\hfill\spf@proofend\par\smallskip\fi}
-\def\sProofEndSymbol#1{\def\sproof@box{#1}}
-%</package>
-%<ltxml>DefConstructor('\sproofend',"");
+\def\sproof@box{%
+ \hbox{\vrule\vbox{\hrule width 6 pt\vskip 6pt\hrule}\vrule}%
+}%
+\def\spf@proofend{\sproof@box}%
+\def\sproofend{%
+ \ifx\spf@proofend\@empty%
+ \else%
+ \hfil\null\nobreak\hfill\spf@proofend\par\smallskip%
+ \fi%
+}%
+\def\sProofEndSymbol#1{\def\sproof@box{#1}}%
% \end{macrocode}
% \end{macro}
%
% \begin{macro}{spf@*@kw}
% \begin{macrocode}
-%<*package>
\def\spf@proofsketch@kw{Proof Sketch}
\def\spf@proof@kw{Proof}
-%</package>
+\def\spf@step@kw{Step}
% \end{macrocode}
% \end{macro}
%
+% For the other languages, we set up triggers
+% \begin{macrocode}
+\AfterBabelLanguage{ngerman}{\input{sproof-ngerman.ldf}}
+% \end{macrocode}
+%
% \begin{macro}{spfsketch}
% \begin{macrocode}
-%<*package>
-\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>#2\n)()"
- . "</omdoc:proof>\n");
-DefConstructor('\sProofEndSymbol {}','');
-%</ltxml>
+\newrobustcmd\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}\sproofend%
+}%
+% \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{spfeq}
+% This is very similar to |\spfsketch|, but uses a computation array\ednote{This should
+% really be more like a tabular with an ensuremath in it. or invoke text on the last
+% column}\ednote{document above}
+% \begin{macrocode}
+\newenvironment{spfeq}[2][]{%
+ \metasetkeys{spf}{#1}\sref@target%
+ \ifx\spf@display\spf@flow%
+ \else%
+ {\stDMemph{\ifx\spf@type\@empty\spf@proof@kw\else\spf@type\fi}:} #2%
+ \fi% display=flow
+ \begin{displaymath}\begin{array}{rcll}%
+}{%
+ \end{array}\end{displaymath}%
+}%
% \end{macrocode}
% \end{macro}
%
@@ -518,47 +554,33 @@ DefConstructor('\sProofEndSymbol {}','');
% up the description environment that will take the proof steps. At the end of the
% proof, we position the proof end into the last line.
% \begin{macrocode}
-%<*package>
-\newenvironment{spf@proof}[2][]{\metasetkeys{spf}{#1}\sref@target
-\count10=10
-\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}}
-\newenvironment{sproof}[2][]{\begin{spf@proof}[#1]{#2}}{\sproofend\end{spf@proof}}
-\newenvironment{sProof}[2][]{\begin{spf@proof}[#1]{#2}}{\end{spf@proof}}
-%</package>
-%<*ltxml>
-DefEnvironment('{sproof} OptionalKeyVals:pf{}',
- "<omdoc:proof "
- . "?&KeyVal(#1,'for')(for='&hash_wrapper(&KeyVal(#1,'for'))')()"
- . "?&defined(&KeyVal(#1,'id'))(xml:id='&KeyVal(#1,'id')')()>\n"
- . "?#2(<omdoc:omtext>"
- . "<omdoc:CMP>#2</omdoc:CMP>"
- . "</omdoc:omtext>\n)()"
- . "#body"
- . "</omdoc:proof>\n");
-DefMacro('\sProof','\sproof');
-DefMacro('\endsProof','\endsproof');
-%</ltxml>
+\newenvironment{spf@proof}[2][]{%
+ \metasetkeys{spf}{#1}%
+ \sref@target%
+ \count10=10%
+ \par\noindent%
+ \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}{\pstlabel@prefix}%
+}{%
+ \end{pst@with@label}\end{description}%
+}%
+\newenvironment{sproof}[2][]{\begin{spf@proof}[#1]{#2}}{\sproofend\end{spf@proof}}%
+\newenvironment{sProof}[2][]{\begin{spf@proof}[#1]{#2}}{\end{spf@proof}}%
% \end{macrocode}
% \end{environment}
%
% \begin{environment}{spfidea}
% \begin{macrocode}
-%<*package>
-\newcommand{\spfidea}[2][]{\metasetkeys{spf}{#1}%
-\stDMemph{\ifx\spf@type\@empty{Proof Idea}\else\spf@type\fi:} #2\sproofend}
-%</package>
-%<*ltxml>
-DefConstructor('\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>#2</omdoc:omtext>\n"
- . "</omdoc:proof>\n");
-%</ltxml>
+\newrobustcmd\spfidea[2][]{%
+ \metasetkeys{spf}{#1}%
+ \stDMemph{\ifx\spf@type\@empty{Proof Idea}\else\spf@type\fi:} #2\sproofend%
+}%
% \end{macrocode}
% \end{environment}
%
@@ -568,64 +590,71 @@ DefConstructor('\spfidea OptionalKeyVals:pf {}',
% generated, otherwise it is. In any case, the proof step number (at the current level) is
% incremented.
% \begin{environment}{spfstep}
+% \ednote{MK: labeling of steps does not work yet.}
% \begin{macrocode}
-%<*package>
-\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}
-%</package>
-%<*ltxml>
-DefEnvironment('{spfstep} OptionalKeyVals:pf',
- "<omdoc:derive "
- . "?&defined(&KeyVal(#1,'id'))(xml:id='&KeyVal(#1,'id')')()>"
- . "<omdoc:CMP>#body</omdoc:derive>\n",
- beforeConstruct=>sub {
- $_[0]->maybeCloseElement('omdoc:CMP');
- });#$
-%</ltxml>
+\newenvironment{spfstep}[1][]{%
+ \metasetkeys{spf}{#1}%
+ \@in@omtexttrue%
+ \ifx\spf@display\spf@flow%
+ \else%
+ \item[\the@pst@label]%
+ \fi%
+ \ifx\spf@title\@empty\else{(\stDMemph{\spf@title})}\fi%
+ \sref@label@id{\pst@label}\ignorespaces%
+}{%
+ \next@pst@label\@in@omtextfalse\ignorespaces%
+}%
% \end{macrocode}
% \end{environment}
%
% \begin{environment}{sproofcomment}
% \begin{macrocode}
-%<*package>
-\newenvironment{sproofcomment}[1][]{\metasetkeys{spf}{#1}
-\ifx\spf@display\spf@flow\else\item[\the@pst@label]\fi}
-{\next@pst@label}
-%</package>
-%<*ltxml>
-DefEnvironment('{sproofcomment} OptionalKeyVals:pf',
- "<omdoc:omtext "
- . "?&defined(&KeyVal(#1,'id'))(xml:id='&KeyVal(#1,'id')')()>"
- . "<omdoc:CMP>#body</omdoc:CMP>"
- . "</omdoc:omtext>");
-%</ltxml>
+\newenvironment{sproofcomment}[1][]{%
+ \metasetkeys{spf}{#1}%
+ \ifx\spf@display\spf@flow\else\item[\the@pst@label]\fi%
+}{%
+ \next@pst@label%
+}%
% \end{macrocode}
% \end{environment}
%
% The next two environments also take a |KeyVal| argument, but also a regular one, which
% contains a start text. Both environments start a new numbered proof level.
%
+% \begin{environment}{subproof}
+% In the |subproof| environment, a new (lower-level) proof environment is started.
+% \begin{macrocode}
+\newenvironment{subproof}[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}%
+}{%
+ \end{pst@with@label}\next@pst@label%
+}%
+% \end{macrocode}
+% \end{environment}
+%
% \begin{environment}{spfcases}
-% In the |pfcases| environment, the start text is displayed as the first comment of the
-% proof.
+% In the |pfcases| environment, the start text is displayed as the first comment of the
+% proof.
% \begin{macrocode}
-%<*package>
-\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}}
-{\end{pst@with@label}\next@pst@label}
-%</package>
-%<*ltxml>
-DefEnvironment('{spfcases} OptionalKeyVals:pf {}',
- "<omdoc:derive "
- . "?&defined(&KeyVal(#1,'id'))(xml:id='&KeyVal(#1,'id')')()>\n"
- . "<omdoc:CMP>#2</omdoc:CMP>\n"
- . "<omdoc:method xref='#proof-by-cases'>#body</omdoc:method>"
- . "</omdoc:derive>\n");
-%</ltxml>
+\newenvironment{spfcases}[2][]{%
+ \def\@test{#1}%
+ \ifx\@test\empty%
+ \begin{subproof}[method=by-cases]{#2}%
+ \else%
+ \begin{subproof}[#1,method=by-cases]{#2}%
+ \fi%
+}{%
+ \end{subproof}%
+}%
% \end{macrocode}
% \end{environment}
%
@@ -633,44 +662,42 @@ DefEnvironment('{spfcases} OptionalKeyVals:pf {}',
% In the |pfcase| environment, the start text is displayed specification of the case
% after the |\item|
% \begin{macrocode}
-%<*package>
-\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}}
-{\ifx\spf@display\spf@flow\else\sproofend\fi\end{pst@with@label}\next@pst@label}
-%</package>
-%<*ltxml>
-DefEnvironment('{spfcase} OptionalKeyVals:pf{}',
- "<omdoc:proof "
- . "?&defined(&KeyVal(#1,'id'))(xml:id='&KeyVal(#1,'id')')()>\n"
- . "?#2(<omdoc:omtext>"
- . "<omdoc:CMP>#2</omdoc:CMP>"
- . "</omdoc:omtext>\n)()"
- . "#body"
- . "</omdoc:proof>\n");
-%</ltxml>
+\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}: }% need blank here
+ \fi%
+ \begin{pst@with@label}{\pst@label,\number\count\count10}
+}{%
+ \ifx\spf@display\spf@flow%
+ \else%
+ \sproofend%
+ \fi%
+ \end{pst@with@label}%
+ \next@pst@label%
+}%
% \end{macrocode}
% \end{environment}
%
-% \begin{environment}{subproof}
-% In the |subproof| environment, a new (lower-level) proof environment is
-% started.\ednote{document this above}
+% \begin{environment}{spfcase}
+% similar to |spfcase|, takes a third argument.
% \begin{macrocode}
-%<*package>
-\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:derive>"
- . "?#1(<omdoc:CMP>#1</omdoc:CMP>)()"
- . "<omdoc:method>"
- . "<omdoc:proof>\n #body\n</omdoc:proof>"
- . "</omdoc:method>"
- ."</omdoc:derive>");
-%</ltxml>
+\newrobustcmd\spfcasesketch[3][]{%
+ \metasetkeys{spf}{#1}%
+ \ifx\spf@display\spf@flow%
+ \else%
+ \item[\the@pst@label]%
+ \fi%
+ \def\@test{#2}%
+ \ifx\@test\@empty%
+ \else%
+ {\stDMemph{#2}: }%
+ \fi#3%
+ \next@pst@label%
+}%
% \end{macrocode}
% \end{environment}
%
@@ -680,18 +707,10 @@ DefEnvironment('{subproof}[]',
% encountered. Here this is very simple, we just define an internal macro with the value,
% so that we can use it later.
% \begin{macrocode}
-%<*package>
\srefaddidkey{just}
\addmetakey{just}{method}
\addmetakey{just}{premises}
\addmetakey{just}{args}
-%</package>
-%<*ltxml>
-DefKeyVal('just','id','Semiverbatim');
-DefKeyVal('just','method','Semiverbatim');
-DefKeyVal('just','premises','Semiverbatim');
-DefKeyVal('just','args','Semiverbatim');
-%</ltxml>
% \end{macrocode}
%
% The next three environments and macros are purely semantic, so we ignore the keyval
@@ -700,55 +719,13 @@ DefKeyVal('just','args','Semiverbatim');
%
% \begin{environment}{justification}
% \begin{macrocode}
-%<*package>
\newenvironment{justification}[1][]{}{}
-%</package>
-%<*ltxml>
-sub extractBodyText {
- my ($box, $remove) = @_;
- my $str = '';
- my @boxes = $box->unlist;
- foreach my $b(@boxes) {
- my $s = '';
- if ($b =~ /LaTeXML::Whatsit/) {
- my $body = $b->getBody;
- $s = $body ? extractBodyText($body, $remove) : '';
- } elsif ($b =~ /LaTeXML::Box/) {
- $s = $b->toString || '';
- @{$b}[0] = '' if $remove; }
- $str .= $s; }
- $str =~ s/\s+/ /g;
- $str; }
-
-DefEnvironment('{justification} OptionalKeyVals:just', sub {
- my ($doc, $keys, %props) = @_;
- my $text = extractBodyText($props{body}, 1);
- my $node = LookupValue('_LastSeenCMP');
- #$node->appendText($text) if $node;
- my $method = $keys ? $keys->getValue('method') : undef;
- $doc->openElement("omdoc:method", $method ? (xref => $method) : ());
- $doc->absorb($props{body}) if $props{body};
- $doc->closeElement("omdoc:method");
- return; });
-%</ltxml>
% \end{macrocode}
% \end{environment}
%
% \begin{macro}{\premise}
% \begin{macrocode}
-%<*package>
-\newcommand{\premise}[2][]{#2}
-%</package>
-%<*ltxml>
-DefMacro('\premise[]{}', sub {
- my ($xref, $text) = ($_[1], $_[2]);
- my @res = (T_CS('\premise@content'));
- push(@res, T_OTHER('['), $xref->unlist, T_OTHER(']')) if $xref;
- push(@res, T_SPACE, $text->unlist) if $text;
- @res; });
-DefConstructor('\premise@content[]',
- "<omdoc:premise xref='#1'/>");
-%</ltxml>
+\newrobustcmd\premise[2][]{#2}
% \end{macrocode}
% \end{macro}
%
@@ -756,56 +733,13 @@ DefConstructor('\premise@content[]',
% the |\justarg| macro is purely semantic, so we ignore the keyval arguments for now and
% only display the content.
% \begin{macrocode}
-%<*package>
-\newcommand{\justarg}[2][]{#2}
+\newrobustcmd\justarg[2][]{#2}
%</package>
-%<*ltxml>
-DefMacro('\justarg[]{}', sub { (($_[1] ? $_[1]->unlist : ()),
- T_SPACE, $_[2]->unlist, T_SPACE); });
-Tag('omdoc:derive', afterClose=>sub {
- my ($doc, $node) = @_;
- my @children = grep($_->nodeType == XML_ELEMENT_NODE, $node->childNodes);
- my $firstCMP = undef;
- foreach my $child(@children) {
- next unless ($child->localname || '') eq 'CMP';
- if ($child->hasChildNodes()) {
- next unless $#{$child->childNodes} == 0;
- next unless $child->firstChild->nodeType == XML_TEXT_NODE; }
-
- if ($firstCMP) {
- $firstCMP->appendText($child->textContent);
- $node->removeChild($child);
- } else { $firstCMP = $child; }
- }
- });#$
-%</ltxml>
% \end{macrocode}
% \end{macro}
%
-% \subsection{Providing IDs for {\omdoc} Elements}\label{sec:impl:ids}
-%
-% To provide default identifiers, we tag all {\omdoc}
-% elements that allow |xml:id| attributes by executing the |numberIt| procedure from |omdoc.sty.ltxml|.
-%
-% \begin{macrocode}
-%<*ltxml>
-Tag('omdoc:proof',afterOpen=>\&numberIt,afterClose=>\&locateIt);
-Tag('omdoc:derive',afterOpen=>\&numberIt,afterClose=>\&locateIt);
-Tag('omdoc:method',afterOpen=>\&numberIt,afterClose=>\&locateIt);
-Tag('omdoc:premise',afterOpen=>\&numberIt,afterClose=>\&locateIt);
-Tag('omdoc:derive',afterOpen=>\&numberIt,afterClose=>\&locateIt);
-%</ltxml>
-% \end{macrocode}
-%
-% \section{Finale}
-%
-% Finally, we need to terminate the file with a success mark for perl.
-% \begin{macrocode}
-%<ltxml>1;
-% \end{macrocode}
% \Finale
\endinput
-
%%% Local Variables:
%%% mode: doctex
%%% TeX-master: t
@@ -831,4 +765,5 @@ Tag('omdoc:derive',afterOpen=>\&numberIt,afterClose=>\&locateIt);
% LocalWords: textbackslash makeatletter sketchproof compactenum tracissue
% LocalWords: metakeys addmetakey metasetkeys stylable pstlabelstyle pstlabel
% LocalWords: pstlabelstyle pstlabelstyle ldots ldots ensuremath inparaenum
-% LocalWords: nameuse prooflistenv
+% LocalWords: nameuse prooflistenv spfcasesketch spfcasesketch spfeq rcll
+% LocalWords: displaymath noindent ignorespaces