summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/tex/latex/bussproofs-extra
diff options
context:
space:
mode:
authorKarl Berry <karl@freefriends.org>2019-06-02 21:47:32 +0000
committerKarl Berry <karl@freefriends.org>2019-06-02 21:47:32 +0000
commit7e9446ab7f75aff4dd715dba944a43a3e9aa069a (patch)
treeb52f1f9dca75579eb383bc946bf039752ecd1d48 /Master/texmf-dist/tex/latex/bussproofs-extra
parentdf91712c3f10cc96b788f31dd2762ea255b1dd80 (diff)
bussproofs-extra (2jun19)
git-svn-id: svn://tug.org/texlive/trunk@51299 c570f23f-e606-0410-a88d-b1316a301751
Diffstat (limited to 'Master/texmf-dist/tex/latex/bussproofs-extra')
-rw-r--r--Master/texmf-dist/tex/latex/bussproofs-extra/bussproofs-extra.sty151
1 files changed, 90 insertions, 61 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
index e740e1ef218..64e474c91fd 100644
--- a/Master/texmf-dist/tex/latex/bussproofs-extra/bussproofs-extra.sty
+++ b/Master/texmf-dist/tex/latex/bussproofs-extra/bussproofs-extra.sty
@@ -22,26 +22,34 @@
%%
\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{bussproofs-extra}
- [2019/04/04 0.3 Extra commands for bussproofs.sty]
-
+ [2019/05/31 0.4 Extra commands for bussproofs.sty]
\RequirePackage{bussproofs}
\RequirePackage{tikz}
-
\newdimen\CenterCorrection
\newdimen\DiagCorrection
+\newbox\myBoxLLL
+\newbox\myBoxRLL
+\tikzset{
+ deduceLine/.style = {line width=1.1pt, loosely dotted}}
\def\straightDeduce{%
- \gdef\fDeduce{\tikz\draw[very thick,loosely dotted] (0,0) -- (0,1);}
+ \gdef\fDeduce{\tikz\draw[deduceLine] (0,0) -- (0,1);}
+ \global\DiagCorrection=0pt
+ \ignorespaces
+}
+
+\def\shortDeduce{%
+ \gdef\fDeduce{\tikz\draw[deduceLine] (0,0) -- (0,.5);}
\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);
+ \draw[deduceLine] (0,0) -- (0,1);
+ \draw[deduceLine] (-.5,.5) -- (0,0);
+ \draw[deduceLine] (.5,.5) -- (0,0);
\end{tikzpicture}}
\global\DiagCorrection=0pt
\ignorespaces
@@ -49,7 +57,7 @@
\def\ddotsDeduce{%
\gdef\fDeduce{\begin{tikzpicture}
- \draw[very thick,loosely dotted] (0,1) -- (1,0);
+ \draw[deduceLine] (0,1) -- (1,0);
\end{tikzpicture}}
\setbox\myBoxA=\hbox{\fDeduce}
\global\DiagCorrection=-\wd\myBoxA
@@ -58,21 +66,18 @@
\def\dotsdDeduce{%
\gdef\fDeduce{\begin{tikzpicture}
- \draw[very thick,loosely dotted] (1,1) -- (0,0);
+ \draw[deduceLine] (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
+ \setbox\myBoxA=\hbox{\fCenter}%
\global\CenterCorrection=-.5\wd\myBoxA
\joinDeduce%
\resetInferenceDefaults%
@@ -82,9 +87,7 @@
\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.
+ \global\CenterCorrection=0pt
\joinDeduce%
\resetInferenceDefaults%
\ignorespaces%
@@ -109,17 +112,6 @@
\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%
@@ -146,45 +138,33 @@
\def\LeftLineLabel#1{%
\global\def\displayLeftLineLabel{%
- \llap{#1\hskip\ScoreOverhangLeft\hskip\labelSpacing}}
+ {#1\hskip\labelSpacing}}
\ignorespaces}
\def\RightLineLabel#1{%
- \global\def\displayRightLineLabel{
- \rlap{\hskip\ScoreOverhangLeft\hskip\labelSpacing #1}}
+ \global\def\displayRightLineLabel{%
+ {\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}
+ \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}%
@@ -204,16 +184,29 @@
\prepAxiom%
% Define the boxes
% bpextra -- add line labels
- \setbox\myBoxA=\hbox{\displayLeftLineLabel$\mathord{#1}\fCenter\mathord{\relax}$}% %bpextra
- \setbox\myBoxB=\hbox{$#2$\displayRightLineLabel}% %bpextra
+ \setbox\myBoxA=\hbox{$\mathord{#1}\fCenter\mathord{\relax}$}%
+ \setbox\myBoxB=\hbox{$#2$}% %bpextra
+ \setbox\myBoxLLL=\hbox{\displayLeftLineLabel}% %bpextra
+ \setbox\myBoxRLL=\hbox{\displayRightLineLabel}% %bpextra
\global\setbox\curBox=%
- \hbox{\hskip\ScoreOverhangLeft\relax%
- \unhcopy\myBoxA\unhcopy\myBoxB\hskip\ScoreOverhangRight\relax}%
+ \hbox{\unhcopy\myBoxLLL%bpextra
+ \hskip\ScoreOverhangLeft\relax
+ \unhcopy\myBoxA
+ \unhcopy\myBoxB
+ \hskip\ScoreOverhangRight
+ \unhcopy\myBoxRLL}%bpextra
% Set the relevant dimensions for the boxes
\global\curScoreStart=0pt \relax
\global\curScoreEnd=\wd\curBox \relax
- \global\curCenter=\wd\myBoxA \relax
+ \global\curCenter=\wd\myBoxA \relax %bpextra
\global\advance \curCenter by \ScoreOverhangLeft%
+ % bpextra adjust by dimensions of labels
+ \global\advance \curCenter by \wd\myBoxLLL%bpextra
+ \global\advance\curScoreStart by \wd\myBoxLLL%bpextra
+ \global\advance\curScoreEnd by -\wd\myBoxRLL%bpextra
+ % reset line labels to nothing %bpextra
+ \global\let\displayLeftLineLabel\relax %bpextra
+ \global\let\displayRightLineLabel\relax %bpextra
\ignorespaces
}
@@ -221,44 +214,80 @@
% Get level and correct names set.
\prepAxiom%
% Define the box.
- \setbox\myBoxA=\hbox{\displayLeftLineLabel #1\displayRightLineLabel}% %bpextra
+ \setbox\myBoxA=\hbox{#1}%
+ \setbox\myBoxLLL=\hbox{\displayLeftLineLabel}% %bpextra
+ \setbox\myBoxRLL=\hbox{\displayRightLineLabel}% %bpextra
\global\setbox\curBox =%
- \hbox{\hskip\ScoreOverhangLeft\relax%
- \unhcopy\myBoxA\hskip\ScoreOverhangRight\relax}%
+ \hbox{\unhcopy\myBoxLLL%bpextra
+ \hskip\ScoreOverhangLeft\relax%
+ \unhcopy\myBoxA
+ \hskip\ScoreOverhangRight\relax
+ \unhcopy\myBoxRLL}% %bpextra
% Set the relevant dimensions for the boxes
\global\curScoreStart=0pt \relax
\global\curScoreEnd=\wd\curBox \relax
- \global\curCenter=.5\wd\curBox \relax
+ \global\curCenter=.5\wd\myBoxA \relax %bpextra
\global\advance \curCenter by \ScoreOverhangLeft%
+ % bpextra adjust by dimensions of labels
+ \global\advance \curCenter by \wd\myBoxLLL%bpextra
+ \global\advance\curScoreStart by \wd\myBoxLLL%bpextra
+ \global\advance\curScoreEnd by -\wd\myBoxRLL%bpextra
+ % reset line labels to nothing %bpextra
+ \global\let\displayLeftLineLabel\relax %bpextra
+ \global\let\displayRightLineLabel\relax %bpextra
\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
+ \setbox\myBoxA=\hbox{$\mathord{#1}\fCenter\mathord{\relax}$}%
+ \setbox\myBoxB=\hbox{$#2$}%
+ \setbox\myBoxLLL=\hbox{\displayLeftLineLabel}% %bpextra
+ \setbox\myBoxRLL=\hbox{\displayRightLineLabel}% %bpextra
% Put them together in \myBoxC
\setbox\myBoxC =%
- \hbox{\hskip\ScoreOverhangLeft\relax%
- \unhcopy\myBoxA\unhcopy\myBoxB\hskip\ScoreOverhangRight\relax}%
+ \hbox{\unhcopy\myBoxLLL%bpextra
+ \hskip\ScoreOverhangLeft\relax%
+ \unhcopy\myBoxA\unhcopy\myBoxB
+ \hskip\ScoreOverhangRight
+ \unhcopy\myBoxRLL}% %bpextra
% Calculate the center of the \myBoxC string.
\newScoreStart=0pt \relax%
\newCenter=\wd\myBoxA \relax%
\advance \newCenter by \ScoreOverhangLeft%
\newScoreEnd=\wd\myBoxC%
+ % bpextra adjust by dimensions of labels
+ \global\advance\newCenter by \wd\myBoxLLL%bpextra
+ \global\advance\newScoreStart by \wd\myBoxLLL%bpextra
+ \global\advance\newScoreEnd by -\wd\myBoxRLL%bpextra
+ % reset line labels to nothing %bpextra
+ \global\let\displayLeftLineLabel\relax %bpextra
+ \global\let\displayRightLineLabel\relax %bpextra
}
\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}}%
+ \setbox\myBoxA=\hbox{#1}%
+ \setbox\myBoxLLL=\hbox{\displayLeftLineLabel}% %bpextra
+ \setbox\myBoxRLL=\hbox{\displayRightLineLabel}% %bpextra
+\setbox\myBoxC =%
+ \hbox{\unhcopy\myBoxLLL%bpextra
+ \hskip\ScoreOverhangLeft\relax%
+ \unhcopy\myBoxA
+ \hskip\ScoreOverhangRight
+ \unhcopy\myBoxRLL}%bpextra
% Calculate kerning to line up centers
\newScoreStart=0pt \relax%
- \newCenter=.5\wd\myBoxC \relax%
+ \newCenter=.5\wd\myBoxA \relax% bpextra
\newScoreEnd=\wd\myBoxC%
\advance \newCenter by \ScoreOverhangLeft%
+ % bpextra adjust by dimensions of labels
+ \global\advance\newCenter by \wd\myBoxLLL%bpextra
+ \global\advance\newScoreStart by \wd\myBoxLLL%bpextra
+ \global\advance\newScoreEnd by -\wd\myBoxRLL%bpextra
+ % reset line labels to nothing %bpextra
+ \global\let\displayLeftLineLabel\relax %bpextra
+ \global\let\displayRightLineLabel\relax %bpextra
}
\endinput
%%