bussproofs-extra (4apr19)

git-svn-id: svn://tug.org/texlive/trunk@50760 c570f23f-e606-0410-a88d-b1316a301751

1 files changed, 265 insertions, 0 deletions

diff --git a/Master/texmf-dist/tex/latex/bussproofs-extra/bussproofs-extra.sty b/Master/texmf-dist/tex/latex/bussproofs-extra/bussproofs-extra.sty
new file mode 100644
index 00000000000..e740e1ef218
--- /dev/null
+++ b/Master/texmf-dist/tex/latex/bussproofs-extra/bussproofs-extra.sty
@@ -0,0 +1,265 @@
+%%
+%% This is file `bussproofs-extra.sty',
+%% generated with the docstrip utility.
+%%
+%% The original source files were:
+%%
+%% bussproofs-extra.dtx  (with options: `package')
+%% 
+%% This is a generated file.
+%% 
+%% Copyright (C) 2019 by Richard Zach <rzach@ucalgary.ca>
+%% 
+%% This file may be distributed and/or modified under the conditions of
+%% the LaTeX Project Public License, either version 1.3 of this license
+%% or (at your option) any later version.  The latest version of this
+%% license is in:
+%% 
+%%    http://www.latex-project.org/lppl.txt
+%% 
+%% and version 1.3 or later is part of all distributions of LaTeX version
+%% 1999/12/01 or later.
+%% 
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{bussproofs-extra}
+   [2019/04/04 0.3 Extra commands for bussproofs.sty]
+
+
+\RequirePackage{bussproofs}
+\RequirePackage{tikz}
+
+\newdimen\CenterCorrection
+\newdimen\DiagCorrection
+
+\def\straightDeduce{%
+  \gdef\fDeduce{\tikz\draw[very thick,loosely dotted] (0,0) -- (0,1);}
+  \global\DiagCorrection=0pt
+  \ignorespaces
+}
+
+\def\branchDeduce{%
+  \gdef\fDeduce{\begin{tikzpicture}
+      \draw[very thick,loosely dotted] (0,0) -- (0,1);
+      \draw[very thick,loosely dotted] (-.5,.5) -- (0,0);
+      \draw[very thick,loosely dotted] (.5,.5) -- (0,0);
+  \end{tikzpicture}}
+  \global\DiagCorrection=0pt
+  \ignorespaces
+}
+
+\def\ddotsDeduce{%
+  \gdef\fDeduce{\begin{tikzpicture}
+      \draw[very thick,loosely dotted] (0,1) -- (1,0);
+  \end{tikzpicture}}
+  \setbox\myBoxA=\hbox{\fDeduce}
+  \global\DiagCorrection=-\wd\myBoxA
+  \ignorespaces
+}
+
+\def\dotsdDeduce{%
+  \gdef\fDeduce{\begin{tikzpicture}
+      \draw[very thick,loosely dotted] (1,1) -- (0,0);
+  \end{tikzpicture}}
+  \setbox\myBoxA=\hbox{\fDeduce}
+  \global\DiagCorrection=\wd\myBoxA
+  \ignorespaces
+}
+
+\def\alwaysDeduce{\straightDeduce}
+\straightDeduce
+
+\def\Deduce$#1\fCenter#2${%
+    \prepUnary%
+    \buildConclusion{#1}{#2}%
+    \setbox\myBoxA=\hbox{\fCenter}
+    % if we align at \fCenter, move \fDeduce left by 1/2 width of \fCenter
+    \global\CenterCorrection=-.5\wd\myBoxA
+    \joinDeduce%
+    \resetInferenceDefaults%
+    \ignorespaces%
+}
+
+\def\DeduceC#1{
+    \prepUnary%
+    \buildConclusionC{#1}%
+    % vdot alignment is off by a bit, correct
+    \global\CenterCorrection=-4pt
+    % Align and join the curBox and the new box into one vbox.
+    \joinDeduce%
+    \resetInferenceDefaults%
+    \ignorespaces%
+}
+
+\def\joinDeduce{%
+    \global\advance\curCenter by -\hypKernAmt%
+    \ifnum\curCenter<\newCenter%
+        \displace=\newCenter%
+        \advance \displace by -\curCenter%
+        \kernUpperBox%
+    \else%
+        \displace=\curCenter%
+        \advance \displace by -\newCenter%
+        \kernLowerBox%
+    \fi%
+    \ifnum\DiagCorrection<0%
+        \displace=-\DiagCorrection
+        \kernLowerBox%
+    \else
+        \displace=\DiagCorrection
+        \kernUpperBox%
+    \fi%
+    \advance\curCenter by-.5\DiagCorrection
+    %\ifnum \newScoreStart < \curScoreStart %
+    %    \global \curScoreStart = \newScoreStart \fi%
+    %\ifnum \curScoreEnd < \newScoreEnd %
+    %    \global \curScoreEnd = \newScoreEnd \fi%
+    % Leave room for the left label.
+    %\ifnum \curScoreStart<\wd\myBoxLL%
+    %    \global\displace = \wd\myBoxLL%
+    %    \global\advance\displace by -\curScoreStart%
+    %    \kernUpperBox%
+    %    \kernLowerBox%
+    %\fi%
+    \buildDeduce%
+    \buildScoreLabels%
+    \ifx\rootAtBottomFlag\myTrue%
+        \buildRootBottom%
+    \else%
+        \buildRootTop%
+    \fi%
+    \global \curScoreStart=\newScoreStart%
+    \global \curScoreEnd=\newScoreEnd%
+    \global \curCenter=\newCenter%
+}
+
+\def\buildDeduce{%
+    \global\setbox \myBoxD =%
+        \hbox{\fDeduce}%
+    \displace = \wd\myBoxD % find width of vdots
+    \global\curScoreStart = \curCenter%
+    \global\advance\curScoreStart by -.5\displace%
+    \global\curScoreEnd = \curCenter%
+    \global\advance\curScoreEnd by .5\displace%
+    \global\advance\curScoreStart by\CenterCorrection
+    \global\advance\curScoreEnd by\CenterCorrection
+}
+
+\def\LeftLineLabel#1{%
+  \global\def\displayLeftLineLabel{%
+    \llap{#1\hskip\ScoreOverhangLeft\hskip\labelSpacing}}
+  \ignorespaces}
+
+\def\RightLineLabel#1{%
+  \global\def\displayRightLineLabel{
+    \rlap{\hskip\ScoreOverhangLeft\hskip\labelSpacing #1}}
+  \ignorespaces}
+
+\global\let\displayLeftLineLabel\relax
+\global\let\displayRightLineLabel\relax
+
+
+\def\LeftSubproofLabel#1{%
+  \global\setbox\curBox =
+<<<<<<< HEAD:bussproofs-extra.dtx
+  \hbox{\vbox to \ht\curBox{\vfil\llap{#1
+        $\left\{\vrule height .5\ht\curBox width 0pt\right.$}\vfil}\box\curBox}%
+=======
+  \hbox{\vbox to \ht\curBox{%
+      \vfil
+      \llap{#1$\left\{\vrule height .5\ht\curBox width 0pt\right.$}%
+      \vfil}\box\curBox}%
+>>>>>>> 4823829694ec2392dad7e3c55cd366f991c7c6db:bpextra.dtx
+}
+
+\def\RightSubproofLabel#1{%
+  \displace=\ht\curBox
+  \global\setbox\curBox =
+<<<<<<< HEAD:bussproofs-extra.dtx
+  \hbox{\box\curBox\vbox to \displace{\vfil
+      \rlap{$\left.\vrule height .5\displace width 0pt\right\}$#1}\vfil}}%
+=======
+  \hbox{\box\curBox\vbox to \displace{%
+      \vfil
+      \rlap{$\left.\vrule height .5\displace width 0pt\right\}$#1}
+      \vfil}}%
+>>>>>>> 4823829694ec2392dad7e3c55cd366f991c7c6db:bpextra.dtx
+}
+
+\def\resetInferenceDefaults{%
+    \global\def\theHypSeparation{\defaultHypSeparation}%
+    \global\setbox\myBoxLL=\hbox{\defaultLeftLabel}%
+    \global\setbox\myBoxRL=\hbox{\defaultRightLabel}%
+    \global\def\buildScore{\alwaysBuildScore}%
+    \global\def\theScoreFiller{\alwaysScoreFiller}%
+    % reset line labels to nothing %bpextra
+    \global\let\displayLeftLineLabel\relax %bpextra
+    \global\let\displayRightLineLabel\relax %bpextra
+    % reset to defaul deduce style %bpextra
+    \alwaysDeduce %bpextra
+    \gdef\hypKernAmt{0pt}% Restore to zero kerning.
+}
+
+\def\Axiom$#1\fCenter#2${%
+    % Get level and correct names set.
+    \prepAxiom%
+    % Define the boxes
+    % bpextra -- add line labels
+    \setbox\myBoxA=\hbox{\displayLeftLineLabel$\mathord{#1}\fCenter\mathord{\relax}$}% %bpextra
+    \setbox\myBoxB=\hbox{$#2$\displayRightLineLabel}% %bpextra
+    \global\setbox\curBox=%
+         \hbox{\hskip\ScoreOverhangLeft\relax%
+        \unhcopy\myBoxA\unhcopy\myBoxB\hskip\ScoreOverhangRight\relax}%
+    % Set the relevant dimensions for the boxes
+    \global\curScoreStart=0pt \relax
+    \global\curScoreEnd=\wd\curBox \relax
+    \global\curCenter=\wd\myBoxA \relax
+    \global\advance \curCenter by \ScoreOverhangLeft%
+    \ignorespaces
+}
+
+\def\AxiomC#1{      % Note argument not in math mode
+    % Get level and correct names set.
+    \prepAxiom%
+        % Define the box.
+    \setbox\myBoxA=\hbox{\displayLeftLineLabel #1\displayRightLineLabel}% %bpextra
+    \global\setbox\curBox =%
+        \hbox{\hskip\ScoreOverhangLeft\relax%
+                        \unhcopy\myBoxA\hskip\ScoreOverhangRight\relax}%
+    % Set the relevant dimensions for the boxes
+        \global\curScoreStart=0pt \relax
+        \global\curScoreEnd=\wd\curBox \relax
+        \global\curCenter=.5\wd\curBox \relax
+        \global\advance \curCenter by \ScoreOverhangLeft%
+    \ignorespaces
+}
+
+\def\buildConclusion#1#2{% Build lower sequent w/ center at \fCenter position.
+    % Define the boxes
+        \setbox\myBoxA=\hbox{\displayLeftLineLabel $\mathord{#1}\fCenter\mathord{\relax}$}% %bpextra
+        \setbox\myBoxB=\hbox{$#2$\displayRightLineLabel}% %bpextra
+    % Put them together in \myBoxC
+    \setbox\myBoxC =%
+          \hbox{\hskip\ScoreOverhangLeft\relax%
+        \unhcopy\myBoxA\unhcopy\myBoxB\hskip\ScoreOverhangRight\relax}%
+    % Calculate the center of the \myBoxC string.
+    \newScoreStart=0pt \relax%
+    \newCenter=\wd\myBoxA \relax%
+    \advance \newCenter by \ScoreOverhangLeft%
+    \newScoreEnd=\wd\myBoxC%
+}
+
+\def\buildConclusionC#1{% Build lower sequent w/o \fCenter present.
+        % Define the box.
+    \setbox\myBoxA=\hbox{\displayLeftLineLabel #1\displayRightLineLabel}% %bpextra
+    \setbox\myBoxC =%
+        \hbox{\hbox{\hskip\ScoreOverhangLeft\relax%
+                        \unhcopy\myBoxA\hskip\ScoreOverhangRight\relax}}%
+    % Calculate kerning to line up centers
+    \newScoreStart=0pt \relax%
+    \newCenter=.5\wd\myBoxC \relax%
+    \newScoreEnd=\wd\myBoxC%
+        \advance \newCenter by \ScoreOverhangLeft%
+}
+\endinput
+%%
+%% End of file `bussproofs-extra.sty'.