summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/tex/latex/stex/sproof.sty.ltxml
diff options
context:
space:
mode:
Diffstat (limited to 'Master/texmf-dist/tex/latex/stex/sproof.sty.ltxml')
-rw-r--r--Master/texmf-dist/tex/latex/stex/sproof.sty.ltxml107
1 files changed, 107 insertions, 0 deletions
diff --git a/Master/texmf-dist/tex/latex/stex/sproof.sty.ltxml b/Master/texmf-dist/tex/latex/stex/sproof.sty.ltxml
new file mode 100644
index 00000000000..afd3433e9b8
--- /dev/null
+++ b/Master/texmf-dist/tex/latex/stex/sproof.sty.ltxml
@@ -0,0 +1,107 @@
+# -*- CPERL -*-
+package LaTeXML::Package::Pool;
+use strict;
+use LaTeXML::Package;
+RequirePackage('omdoc');
+DefKeyVal('pf','id','Semiverbatim');
+DefKeyVal('pf','display','Semiverbatim'); # not used at the moment
+DefKeyVal('pf','for','Semiverbatim');
+DefKeyVal('pf','from','Semiverbatim');
+DefKeyVal('pf','proofend','Semiverbatim');
+DefKeyVal('pf','noproofend','Semiverbatim');
+DefKeyVal('pf','type','Semiverbatim');
+DefKeyVal('pf','title','Semiverbatim');
+DefKeyVal('pf','continues','Semiverbatim');
+DefConstructor('\sproofend',"");
+DefEnvironment('{sproof} OptionalKeyVals:pf{}',
+ "<omdoc:proof ?&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('{sproofidea} OptionalKeyVals:pf {}',
+ "<omdoc:proof ?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id')')()>\n"
+ . "<omdoc:omtext><omdoc:CMP><omdoc:p>#2</omdoc:p></omdoc:CMP></omdoc:omtext>\n"
+ . "</omdoc:proof>\n");
+DefCMPEnvironment('{spfstep} OptionalKeyVals:pf',
+ "<omdoc:derive ?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id')')()>"
+ . "<omdoc:CMP><omdoc:p>#body</omdoc:p></omdoc:CMP>"
+ . "</omdoc:derive>\n");
+DefCMPEnvironment('{sproofcomment} OptionalKeyVals:pf',
+ "<omdoc:omtext ?&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 ?&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 ?&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);
+Tag('omdoc:derive',afterOpen=>\&numberIt);
+Tag('omdoc:method',afterOpen=>\&numberIt);
+1;