summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/tex/latex/bussproofs-extra
diff options
context:
space:
mode:
authorKarl Berry <karl@freefriends.org>2019-04-04 20:59:56 +0000
committerKarl Berry <karl@freefriends.org>2019-04-04 20:59:56 +0000
commitc5a40679707809a67789ed63672bd9b73fd31c41 (patch)
tree2c98d149af35c10f35e345629339d69a87c48488 /Master/texmf-dist/tex/latex/bussproofs-extra
parent51826e690ad1c167b12b52e25604ed3579a989ba (diff)
bussproofs-extra (4apr19)
git-svn-id: svn://tug.org/texlive/trunk@50760 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.sty265
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'.