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 | 511 |
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 |