summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/tex/latex/stex/sproof
diff options
context:
space:
mode:
authorKarl Berry <karl@freefriends.org>2010-07-20 22:30:22 +0000
committerKarl Berry <karl@freefriends.org>2010-07-20 22:30:22 +0000
commitcdfe96a3444a4d0664b9702c4ff6fe6622257834 (patch)
tree577232accd4bf41d7480fae7c177ceef147c8fea /Master/texmf-dist/tex/latex/stex/sproof
parent47e2d96a8faed88dfedd17ca5352227d585a6710 (diff)
stex update once more
git-svn-id: svn://tug.org/texlive/trunk@19548 c570f23f-e606-0410-a88d-b1316a301751
Diffstat (limited to 'Master/texmf-dist/tex/latex/stex/sproof')
-rw-r--r--Master/texmf-dist/tex/latex/stex/sproof/sproof.sty71
-rw-r--r--Master/texmf-dist/tex/latex/stex/sproof/sproof.sty.ltxml122
2 files changed, 193 insertions, 0 deletions
diff --git a/Master/texmf-dist/tex/latex/stex/sproof/sproof.sty b/Master/texmf-dist/tex/latex/stex/sproof/sproof.sty
new file mode 100644
index 00000000000..6a101124b4b
--- /dev/null
+++ b/Master/texmf-dist/tex/latex/stex/sproof/sproof.sty
@@ -0,0 +1,71 @@
+%%
+%% This is file `sproof.sty',
+%% generated with the docstrip utility.
+%%
+%% The original source files were:
+%%
+%% sproof.dtx (with options: `package')
+%%
+\NeedsTeXFormat{LaTeX2e}[1999/12/01]
+\ProvidesPackage{sproof}[2010/06/25 v0.9f Semantic Markup for Proofs]
+\RequirePackage{sref}
+\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}
+\def\spf@flow{flow}
+\newenvironment{pst@with@label}[1]{\edef\pst@label{#1}\advance\count10 by 1\count\count10=1}
+{\advance\count10 by -1}
+\def\the@pst@label{\pst@label.\number\count\count10}
+\def\next@pst@label{\global\advance\count\count10 by 1}
+\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}}
+\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}}
+\newenvironment{@proof}[2][]{\omdsetkeys{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}
+\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{@proof}[#1]{#2}}{\sproofend\end{@proof}}
+\newenvironment{sProof}[2][]{\begin{@proof}[#1]{#2}}{\end{@proof}}
+\newcommand{\spfidea}[2][]{\omdsetkeys{spf}{#1}%
+\stDMemph{\ifx\spf@type\@empty{Proof Idea}\else\spf@type\fi:} #2\sproofend}
+\newenvironment{spfstep}[1][]{\omdsetkeys{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}
+\newenvironment{sproofcomment}[1][]{\omdsetkeys{spf}{#1}
+\ifx\spf@display\spf@flow\else\item[\the@pst@label]\fi}
+{\next@pst@label}
+\newenvironment{spfcases}[2][]{\omdsetkeys{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}
+\newenvironment{spfcase}[2][]{\omdsetkeys{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}
+\newenvironment{subproof}{\begin{pst@with@label}{\pst@label.\number\count\count10}}
+{\ifx\spf@display\spf@flow\else\sproofend\fi\end{pst@with@label}}
+\srefaddidkey{just}
+\omdaddkey{just}{method}
+\omdaddkey{just}{premises}
+\omdaddkey{just}{args}
+\newenvironment{justification}[1][]{}{}
+\newcommand{\premise}[2][]{#2}
+\newcommand{\justarg}[2][]{#2}
+\endinput
+%%
+%% End of file `sproof.sty'.
diff --git a/Master/texmf-dist/tex/latex/stex/sproof/sproof.sty.ltxml b/Master/texmf-dist/tex/latex/stex/sproof/sproof.sty.ltxml
new file mode 100644
index 00000000000..91dc3034627
--- /dev/null
+++ b/Master/texmf-dist/tex/latex/stex/sproof/sproof.sty.ltxml
@@ -0,0 +1,122 @@
+# -*- CPERL -*-
+package LaTeXML::Package::Pool;
+use strict;
+use LaTeXML::Package;
+RequirePackage('sref');
+DefConstructor('\sproofend',"");
+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)()"
+ . "</omdoc:proof>\n");
+DefConstructor('\sProofEndSymbol {}','');
+DefCMPEnvironment('{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><omdoc:p>#2</omdoc:p></omdoc:CMP>"
+ . "</omdoc:omtext>\n)()"
+ . "#body"
+ . "</omdoc:proof>\n");
+DefMacro('\sProof','\sproof');
+DefMacro('\endsProof','\endsproof');
+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:proof>\n");
+DefCMPEnvironment('{spfstep} OptionalKeyVals:pf',
+ "<omdoc:derive "
+ . "?&defined(&KeyVal(#1,'id'))(xml:id='&KeyVal(#1,'id')')()>"
+ . "<omdoc:CMP><omdoc:p>#body</omdoc:derive>\n",
+ beforeConstruct=>sub {
+ $_[0]->maybeCloseElement('omdoc:p');
+ $_[0]->maybeCloseElement('omdoc:CMP');
+ });
+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:omtext>");
+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:method xref='#proof-by-cases'>#body</omdoc:method>"
+ . "</omdoc:derive>\n");
+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:omtext>\n)()"
+ . "#body"
+ . "</omdoc:proof>\n");
+DefEnvironment('{subproof}',
+ "<omdoc:proof>\n #body\n</omdoc:proof>\n");
+DefKeyVal('just','id','Semiverbatim');
+DefKeyVal('just','method','Semiverbatim');
+DefKeyVal('just','premises','Semiverbatim');
+DefKeyVal('just','args','Semiverbatim');
+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; });
+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'/>");
+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; }
+ }
+ });#$
+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);
+1;