diff options
Diffstat (limited to 'Master/texmf-dist/tex/latex/stex/sproof')
| -rw-r--r-- | Master/texmf-dist/tex/latex/stex/sproof/sproof.sty | 84 | ||||
| -rw-r--r-- | Master/texmf-dist/tex/latex/stex/sproof/sproof.sty.ltxml | 125 |
2 files changed, 209 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..35d2470cd02 --- /dev/null +++ b/Master/texmf-dist/tex/latex/stex/sproof/sproof.sty @@ -0,0 +1,84 @@ +%% +%% 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}[2012/01/28 v1.0 Semantic Markup for Proofs] +\DeclareOption{showmeta}{\PassOptionsToPackage{\CurrentOption}{metakeys}} +\ProcessOptions +\RequirePackage{sref} +\srefaddidkey{spf} +\addmetakey*{spf}{display} +\addmetakey{spf}{for} +\addmetakey{spf}{from} +\addmetakey*[\sproof@box]{spf}{proofend} +\addmetakey{spf}{type} +\addmetakey*{spf}{title} +\addmetakey{spf}{continues} +\addmetakey{spf}{functions} +\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@make@label\pst@label{\number\count\count10}} +\def\pst@make@label@long#1#2{\@for\@I:=#1\do{\@I.}#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\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}} +\def\spf@proofsketch@kw{Proof Sketch} +\def\spf@proof@kw{Proof} +\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}} +\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}} +\newcommand{\spfidea}[2][]{\metasetkeys{spf}{#1}% +\stDMemph{\ifx\spf@type\@empty{Proof Idea}\else\spf@type\fi:} #2\sproofend} +\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} +\newenvironment{sproofcomment}[1][]{\metasetkeys{spf}{#1} +\ifx\spf@display\spf@flow\else\item[\the@pst@label]\fi} +{\next@pst@label} +\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} +\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} +\newenvironment{subproof}[1][]% +{\begin{pst@with@label}{\pst@label,\number\count\count10}} +{\ifx\spf@display\spf@flow\else\sproofend\fi\end{pst@with@label}} +\srefaddidkey{just} +\addmetakey{just}{method} +\addmetakey{just}{premises} +\addmetakey{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..042ba7f7dc7 --- /dev/null +++ b/Master/texmf-dist/tex/latex/stex/sproof/sproof.sty.ltxml @@ -0,0 +1,125 @@ +# -*- CPERL -*- +package LaTeXML::Package::Pool; +use strict; +use LaTeXML::Package; +RequirePackage('sref'); +DeclareOption('showmeta',''); +DefConstructor('\sproofend',""); +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 {}',''); +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'); +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"); +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'); + });#$ +DefEnvironment('{sproofcomment} OptionalKeyVals:pf', + "<omdoc:omtext " + . "?&defined(&KeyVal(#1,'id'))(xml:id='&KeyVal(#1,'id')')()>" + . "<omdoc:CMP>#body</omdoc:CMP>" + . "</omdoc:omtext>"); +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"); +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"); +DefEnvironment('{subproof}[]', + "<omdoc:derive>" + . "?#1(<omdoc:CMP>#1</omdoc:CMP>)()" + . "<omdoc:method>" + . "<omdoc:proof>\n #body\n</omdoc:proof>" + . "</omdoc:method>" + ."</omdoc:derive>"); +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; |