From c5a40679707809a67789ed63672bd9b73fd31c41 Mon Sep 17 00:00:00 2001 From: Karl Berry Date: Thu, 4 Apr 2019 20:59:56 +0000 Subject: bussproofs-extra (4apr19) git-svn-id: svn://tug.org/texlive/trunk@50760 c570f23f-e606-0410-a88d-b1316a301751 --- .../latex/bussproofs-extra/bussproofs-extra.sty | 265 +++++++++++++++++++++ 1 file changed, 265 insertions(+) create mode 100644 Master/texmf-dist/tex/latex/bussproofs-extra/bussproofs-extra.sty (limited to 'Master/texmf-dist/tex') 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 +%% +%% 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'. -- cgit v1.2.3