%% %% 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 %% %% 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'.