diff options
author | Norbert Preining <norbert@preining.info> | 2019-09-02 13:46:59 +0900 |
---|---|---|
committer | Norbert Preining <norbert@preining.info> | 2019-09-02 13:46:59 +0900 |
commit | e0c6872cf40896c7be36b11dcc744620f10adf1d (patch) | |
tree | 60335e10d2f4354b0674ec22d7b53f0f8abee672 /macros/latex/contrib/bussproofs-extra/bussproofs-extra.dtx |
Initial commit
Diffstat (limited to 'macros/latex/contrib/bussproofs-extra/bussproofs-extra.dtx')
-rw-r--r-- | macros/latex/contrib/bussproofs-extra/bussproofs-extra.dtx | 685 |
1 files changed, 685 insertions, 0 deletions
diff --git a/macros/latex/contrib/bussproofs-extra/bussproofs-extra.dtx b/macros/latex/contrib/bussproofs-extra/bussproofs-extra.dtx new file mode 100644 index 0000000000..a371cff408 --- /dev/null +++ b/macros/latex/contrib/bussproofs-extra/bussproofs-extra.dtx @@ -0,0 +1,685 @@ +% \iffalse meta-comment +% +% +% Copyright (C) 2019 by Richard Zach <rzach@ucalgary.ca> +% ------------------------------------------------------ +% +% This work 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 2005/12/01 or later. +% +% This work has the LPPL maintenance status `maintained'. +% +% The Current Maintainer of this work is Richard Zach. +% +% This work consists of the files bussproofs-pextra.dtx, +% bussproofs-extra.ins, bussproofs-extra.sty +% +% \fi +% +% \iffalse +%<*driver> +\ProvidesFile{bussproofs-extra.dtx} +%</driver> +%<package>\NeedsTeXFormat{LaTeX2e} +%<package>\ProvidesPackage{bussproofs-extra} +%<package> [2019/05/31 0.4 Extra commands for bussproofs.sty] +%<*driver> +\documentclass{ltxdoc} + +\usepackage{bussproofs-extra} +\usepackage[colorlinks,allcolors=blue]{hyperref} +\usepackage{calc} + +\renewcommand{\fCenter}{\ensuremath{\,{\to}\,}} + +\EnableCrossrefs +\RecordChanges +\begin{document} + \DocInput{bussproofs-extra.dtx} + \PrintChanges +\end{document} +%</driver> +% \fi +% +% \CheckSum{0} +% +% \CharacterTable +% {Upper-case \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z +% Lower-case \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z +% Digits \0\1\2\3\4\5\6\7\8\9 +% Exclamation \! Double quote \" Hash (number) \# +% Dollar \$ Percent \% Ampersand \& +% Acute accent \' Left paren \( Right paren \) +% Asterisk \* Plus \+ Comma \, +% Minus \- Point \. Solidus \/ +% Colon \: Semicolon \; Less than \< +% Equals \= Greater than \> Question mark \? +% Commercial at \@ Left bracket \[ Backslash \\ +% Right bracket \] Circumflex \^ Underscore \_ +% Grave accent \` Left brace \{ Vertical bar \| +% Right brace \} Tilde \~} +% +% +% \changes{v0.4}{2019/05/31}{Better implementation of line labels; add +% shortDeduce; style deduce lines} +% \changes{v0.3}{2019/04/04}{Rename to bussproofs-extra.sty} +% \changes{v0.2}{2014/10/16}{Fixed bug in dotsdDeduce, added examples} +% \changes{v0.1}{2014/04/26}{Initial version with deduce, linelabel functionality} +% +% \GetFileInfo{bussproofs-extra.sty} +% +% \DoNotIndex{\newcommand,\newenvironment} +% +% +% \title{The \textsf{bussproofs-extra} package\thanks{This document +% corresponds to \textsf{bussproofs-extra}~\fileversion, dated \filedate.}} +% \author{\href{http://richardzach.org/}{Richard Zach}} +% \date{} +% +% \maketitle +% +% \section{Introduction} +% +% The \textsf{bussproofs-extra} package provides additional functionality for +% the proof tree typesetting package +% \href{http://math.ucsd.edu/~sbuss/ResearchWeb/bussproofs/}{\textsf{bussproofs}} +% by Sam Buss. It is experimental and tested only with v.1.1, and +% only in \LaTeX{} mode with upward-growing trees. +% Functionality provided includes: +% +% \begin{enumerate} +% \item |\Deduce$| and |\DeduceC| commands, which work much +% like |\Infer| commands but indicate missing parts of a proof. +% \item Multiple styles for typesetting the result of |\Deduce|, +% including +% \begin{enumerate} +% \item |\straightDeduce|, which produces vertical dots +% \item |\branchDeduce|, which produces diagonal plus vertical dots +% \item |\ddotsDeduce|, which produces diagonal dots from top left +% to bottom right +% \item |\dotsdDeduce|, which produces diagonal dots from top right +% to bottom left +% \item |\shortDeduce|, which is like |\straightDeduce| but half the length +% \end{enumerate} +% |\straightDeduce| is the default. It can be changed by redefining +% |\alwaysDeduce|. +% \item |\LeftLineLabel| and |\RightLineLabel| commands which +% work like |\LeftLabel| and |\RightLabel| but place a label +% next to the conclusion of an inference/deduction instead of the score +% line. +% \item |\LeftSubproofLabel| and |\RightSubproofLabel| commands which +% work like |\LeftLabel| and |\RightLabel| but place a label +% next to the entire preceding subproof with a curly brace. +% \end{enumerate} +% +% Here's what these deductions look like: +% +% \begin{center} +% \begin{tabular}{@{}cccc@{}} +% \fbox{\AxiomC{$A$} +% \straightDeduce +% \DeduceC{$B$} +% \DisplayProof} & +% \fbox{\AxiomC{$A$} +% \branchDeduce +% \DeduceC{$B$} +% \DisplayProof} & +% \fbox{\AxiomC{$A$} +% \ddotsDeduce +% \DeduceC{$B$} +% \DisplayProof} & +% \fbox{\AxiomC{$A$} +% \dotsdDeduce +% \DeduceC{$B$} +% \DisplayProof} \\ \\ +% \fbox{\Axiom$A \fCenter B$ +% \straightDeduce +% \Deduce$A \lor C \fCenter B$ +% \DisplayProof} & +% \fbox{\Axiom$A \fCenter B$ +% \branchDeduce +% \Deduce$A \lor C \fCenter B$ +% \DisplayProof} & +% \fbox{\Axiom$A \fCenter B$ +% \ddotsDeduce +% \Deduce$A \lor C \fCenter B$ +% \DisplayProof} & +% \fbox{\Axiom$A \fCenter B$ +% \dotsdDeduce +% \Deduce$A \lor C \fCenter B$ +% \DisplayProof} +% \\ \\ +% \texttt{straightDeduce} & +% \texttt{branchDeduce} & +% \texttt{ddotsDeduce} & +% \texttt{dotsdDeduce} +% \end{tabular} +% \end{center} +% +% +% The most up-to-date version of this package is available at the +% \href{https://github.com/OpenLogicProject/bussproofs-extra}{Open Logic +% Project github site}, where you can file bug reports as well. +% +% \subsection{Example} +% +% \begin{verbatim} +% \begin{prooftree} +% \AxiomC{} +% \RightLabel{$\pi_1(a)$} +% \Deduce$\Gamma_1 \fCenter \Theta_1, F(a)$ +% \RightLabel{$\forall$R} +% \UnaryInf$\Gamma_1 \fCenter \Theta_1, \forall x\,F(x)$ +% \ddotsDeduce +% \RightLabel{$\pi_1'$} +% \Deduce$\Gamma \fCenter \Theta, \forall x\,F(x)$ +% \AxiomC{} +% \RightLabel{$\pi_2$} +% \Deduce$F(n), \Delta_1 \fCenter \Lambda_1$ +% \RightLabel{$\forall$L} +% \UnaryInf$\forall x\,F(x), \Delta_1 \fCenter \Lambda_1$ +% \dotsdDeduce +% \RightLabel{$\pi_2'$} +% \Deduce$\forall x\,F(x), \Delta \fCenter \Lambda$ +% \RightLabel{cut} +% \BinaryInf$\Gamma, \Delta \fCenter \Theta, \Lambda$ +% \RightLabel{$\pi_4$} +% \branchDeduce +% \Deduce$\Pi \fCenter \Xi$ +% \end{prooftree} +% \end{verbatim} +% produces this: +% \begin{prooftree} +% \AxiomC{} +% \RightLabel{$\pi_1(a)$} +% \Deduce$\Gamma_1 \fCenter \Theta_1, F(a)$ +% \RightLabel{$\forall$R} +% \UnaryInf$\Gamma_1 \fCenter \Theta_1, \forall x\,F(x)$ +% \ddotsDeduce +% \RightLabel{$\pi_1'$} +% \Deduce$\Gamma \fCenter \Theta, \forall x\,F(x)$ +% \AxiomC{} +% \RightLabel{$\pi_2$} +% \Deduce$F(n), \Delta_1 \fCenter \Lambda_1$ +% \RightLabel{$\forall$L} +% \UnaryInf$\forall x\,F(x), \Delta_1 \fCenter \Lambda_1$ +% \dotsdDeduce +% \RightLabel{$\pi_2'$} +% \Deduce$\forall x\,F(x), \Delta \fCenter \Lambda$ +% \RightLabel{cut} +% \BinaryInf$\Gamma, \Delta \fCenter \Theta, \Lambda$ +% \RightLabel{$\pi_4$} +% \branchDeduce +% \Deduce$\Pi \fCenter \Xi$ +% \end{prooftree} + +% It is also possible to label entire subproofs on the left and on the right. +% \begin{verbatim} +% \begin{prooftree} +% \AxiomC{} +% \Deduce$\Gamma \fCenter \Delta$ +% \LeftLineLabel{$S_1$} +% \Deduce$\Gamma \fCenter \Delta, A$ +% \LeftSubproofLabel{$\pi$} +% \AxiomC{} +% \Deduce$\Gamma' \fCenter \Delta'$ +% \LeftLineLabel{$S_2$} +% \Deduce$A, \Gamma' \fCenter \Delta'$ +% \RightSubproofLabel{$\pi'$} +% \RightLabel{cut} +% \LeftLineLabel{$S_3$} +% \BinaryInf$\Gamma, \Gamma' \fCenter \Delta, \Delta'$ +% \Deduce$\Pi \fCenter \Lambda$ +% \end{prooftree} +% \end{verbatim} +% \begin{prooftree} +% \AxiomC{} +% \Deduce$\Gamma \fCenter \Delta$ +% \Deduce$\Gamma \fCenter \Delta, A$ +% \LeftSubproofLabel{$\pi$} +% \AxiomC{} +% \Deduce$\Gamma' \fCenter \Delta'$ +% \Deduce$A, \Gamma' \fCenter \Delta'$ +% \RightSubproofLabel{$\pi'$} +% \RightLabel{cut} +% \BinaryInf$\Gamma, \Gamma' \fCenter \Delta, \Delta'$ +% \Deduce$\Pi \fCenter \Lambda$ +% \end{prooftree} +% +% The |\LeftLineLabel| and |\RightLineLabel| commands add labels to +% the sequent or formula produced by the following |\Axiom|, |\XxxxInf|, +% and |\Deduce| command. +% \begin{prooftree} +% \LeftLineLabel{$S_1$} +% \RightLineLabel{$S_1$} +% \Axiom$\phantom{A, {}}\Gamma \fCenter \Delta$ +% \LeftLineLabel{$S_2$} +% \RightLineLabel{$S_2$} +% \UnaryInf$A, \Gamma \fCenter \Delta, B$ +% \LeftLineLabel{$S_3$} +% \Deduce$\Pi \fCenter \Lambda$ +% \LeftLineLabel{$S_1'$} +% \AxiomC{\makebox[\widthof{$A \lor B$}][c]{$A$}} +% \LeftLineLabel{$S_2'$} +% \UnaryInfC{$A \lor B$} +% \LeftLineLabel{$S_3'$} +% \DeduceC{$C$} +% \LeftLineLabel{$S_4$} +% \BinaryInf$\Pi \fCenter \Lambda$ +% \RightLineLabel{$S_5$} +% \UnaryInf$\Pi \fCenter \Lambda$ +% \end{prooftree} +% If the sequent or formula is itself a premise of an |\XxxInf| +% command and the conclusion is longer, this may produce a less +% than optimal result, as the label is produced before the score +% line below (compare the left and right labels of the top left +% sequent above). In that case you may want to insert extra space +% using |\phantom|, or use |\makebox| and the |\widthof| command +% of the |calc| package for the |XxxC| variants of the commands +% (see the top right formula below) as in the |\Axiom| commands +% below. +% \begin{verbatim} +% \begin{prooftree} +% \LeftLineLabel{$S_1$} +% \RightLineLabel{$S_1$} +% \Axiom$\phantom{A, {}}\Gamma \fCenter \Delta$ +% \LeftLineLabel{$S_2$} +% \RightLineLabel{$S_2$} +% \UnaryInf$A, \Gamma \fCenter \Delta, B$ +% \LeftLineLabel{$S_3$} +% \Deduce$\Pi \fCenter \Lambda$ +% \LeftLineLabel{$S_1'$} +% \AxiomC{\makebox[\widthof{$A \lor B$}][c]{$A$}} +% \LeftLineLabel{$S_2'$} +% \UnaryInfC{$A \lor B$} +% \LeftLineLabel{$S_3'$} +% \DeduceC{$C$} +% \LeftLineLabel{$S_4$} +% \BinaryInf$\Pi \fCenter \Lambda$ +% \RightLineLabel{$S_5$} +% \UnaryInf$\Pi \fCenter \Lambda$ +% \end{prooftree} +% \end{verbatim} +% +% \StopEventually{} +% +% \section{Implementation} +% +% \subsection{Setup} +% +% We require \textsf{bussproofs} (obviously) and and \textsf{tikz} for +% drawing things. +% +% \begin{macrocode} +\RequirePackage{bussproofs} +\RequirePackage{tikz} +% \end{macrocode} +% \subsection{Dimensions and boxes} +% +% \textsf{bussproofs} aligns sequents at the right end of the sequent +% arrow, so we need to remember by how much to correct to get +% deductions to the middle of sequents. For |\ddotsDeduce| and +% |\dotsdDeduce| (diagonal) styles, the upper and lower sequents will be +% displaced. +% \begin{macrocode} +\newdimen\CenterCorrection +\newdimen\DiagCorrection +% \end{macrocode} +% We need two boxes to hold the left and right line labels. +% \begin{macrocode} +\newbox\myBoxLLL +\newbox\myBoxRLL +% \end{macrocode} +% \subsection{Deduce Styles} +% +% The following commands set the style for the next |\Deduce| +% command. |\straightDeduce| produces a simple vertical line of dots, +% and |\shortDeduce| a line of half that length. +% |\branchDeduce| produces centered branching (Takeuti/Gentzen-style) +% dots, |\ddotsDeduce| left-to-right diagonal dots, and |\dotsdDeduce| +% right-to-left diagonal dots. They do this by redefining the +% |\fDeduce| command which produces the dots and sets up the +% dimensions. The TikZ style |deduceLine| is used as argument to the +% |\draw| command and can be redefined for other line styles as well +% (e.g., smaller dots or closer spacing). +% \begin{macrocode} +\tikzset{ + deduceLine/.style = {line width=1.1pt, loosely dotted}} + +\def\straightDeduce{% + \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[deduceLine] (0,0) -- (0,1); + \draw[deduceLine] (-.5,.5) -- (0,0); + \draw[deduceLine] (.5,.5) -- (0,0); + \end{tikzpicture}} + \global\DiagCorrection=0pt + \ignorespaces +} + +\def\ddotsDeduce{% + \gdef\fDeduce{\begin{tikzpicture} + \draw[deduceLine] (0,1) -- (1,0); + \end{tikzpicture}} + \setbox\myBoxA=\hbox{\fDeduce} + \global\DiagCorrection=-\wd\myBoxA + \ignorespaces +} + +\def\dotsdDeduce{% + \gdef\fDeduce{\begin{tikzpicture} + \draw[deduceLine] (1,1) -- (0,0); + \end{tikzpicture}} + \setbox\myBoxA=\hbox{\fDeduce} + \global\DiagCorrection=\wd\myBoxA + \ignorespaces +} +% \end{macrocode} +% The |\alwaysDeduce| command is used to (re)set the +% deduce style to a default and is executed every time a deduction is +% typeset. It can be redefined to change the default deduce style. +% \begin{macrocode} +\def\alwaysDeduce{\straightDeduce} +\straightDeduce +% \end{macrocode} +% \subsection{\texttt{\textbackslash Deduce\$} and +% \texttt{\textbackslash DeduceC}} +% +% |\Deduce$| and |\DeduceC| are the commands to actually produce the +% deductions. They are used and work just like |\UnaryInf$| and +% |\UnaryInfC|. +% \begin{macrocode} +\def\Deduce$#1\fCenter#2${% + \prepUnary% + \buildConclusion{#1}{#2}% + \setbox\myBoxA=\hbox{\fCenter}% + \global\CenterCorrection=-.5\wd\myBoxA + \joinDeduce% + \resetInferenceDefaults% + \ignorespaces% +} + +\def\DeduceC#1{ + \prepUnary% + \buildConclusionC{#1}% + \global\CenterCorrection=0pt + \joinDeduce% + \resetInferenceDefaults% + \ignorespaces% +} +% \end{macrocode} +% \section{Typesetting the Deduction} +% +% |\joinDeduce| aligns and joins |\curBox| and |\myBoxC| into a single +% |vbox|. |\curBox| holds the upper proof, |\curScoreStart| is +% distance to where the line below the premise would start, +% |\curScoreCenter| is distance from left edge of score to the +% alignment point, and |\curScoreEnd| is width of the score line. +% \begin{macrocode} + +\def\joinDeduce{% + \global\advance\curCenter by -\hypKernAmt% +% \end{macrocode} +% If center of premise is left of center of conclusion move upper box +% to right by difference, else move lower box right by difference +% \begin{macrocode} + \ifnum\curCenter<\newCenter% + \displace=\newCenter% + \advance \displace by -\curCenter% + \kernUpperBox% + \else% + \displace=\curCenter% + \advance \displace by -\newCenter% + \kernLowerBox% + \fi% +% \end{macrocode} +% For |\ddotsDeduce|, move lower box right; for |\dotsdDeduce|, move +% upper box right; then set |\curCenter| to align with horizontal center +% of dots. +% \begin{macrocode} + \ifnum\DiagCorrection<0% + \displace=-\DiagCorrection + \kernLowerBox% + \else + \displace=\DiagCorrection + \kernUpperBox% + \fi% + \advance\curCenter by-.5\DiagCorrection +% \end{macrocode} +% Now we draw the deduction. +% \begin{macrocode} + \buildDeduce% +% \end{macrocode} +% Put the deduction and labels into a box. +% \begin{macrocode} + \buildScoreLabels% +% \end{macrocode} +% Put everything into a new box and compute the dimensions for the +% next |\Deduce| or |\XxxxInf|. +% \begin{macrocode} + \ifx\rootAtBottomFlag\myTrue% + \buildRootBottom% + \else% + \buildRootTop% + \fi% + \global \curScoreStart=\newScoreStart% + \global \curScoreEnd=\newScoreEnd% + \global \curCenter=\newCenter% +} +% \end{macrocode} +% |\buildDeduce| does for |\DeduceX| what |\buildInf| does for +% |\XxxInf|: put the deduction bit (dots) into a box and set the +% dimensions properly. +% \begin{macrocode} + +\def\buildDeduce{% + \global\setbox \myBoxD =% + \hbox{\fDeduce}% + \displace = \wd\myBoxD % find width of vdots +% \end{macrocode} +% set start and end of current score to left and right of the box +% holding the deduction. +% \begin{macrocode} + \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 +} +% \end{macrocode} +% \subsection{Line Labels} +% +% |\LeftLineLabel| and |\RightLineLabel| set the label to place to the +% left or right, respectively, of the conclusion of the next |\Axiom|, +% |\XxxInf| or |\Deduce| command. They are aligned with the text +% produced by |\LeftLabel| and |\RightLabel| (i.e., the distance to +% the line is $|\ScoreOverhang| + |\labelSpacing|$. +% \begin{macrocode} + +\def\LeftLineLabel#1{% + \global\def\displayLeftLineLabel{% + {#1\hskip\labelSpacing}} + \ignorespaces} + +\def\RightLineLabel#1{% + \global\def\displayRightLineLabel{% + {\hskip\labelSpacing #1}} + \ignorespaces} + +\global\let\displayLeftLineLabel\relax +\global\let\displayRightLineLabel\relax +% \end{macrocode} +% +% \subsection{Subproof Labels} +% Sometimes you'd like to lable entire subproofs. This is done with +% commands |\LeftSubproofLabel| and |\RightSubproofLabel|. +% \begin{macrocode} + +\def\LeftSubproofLabel#1{% + \global\setbox\curBox = + \hbox{\vbox to \ht\curBox{% + \vfil + \llap{#1$\left\{\vrule height .5\ht\curBox width 0pt\right.$}% + \vfil}\box\curBox}% +} + +\def\RightSubproofLabel#1{% + \displace=\ht\curBox + \global\setbox\curBox = + \hbox{\box\curBox\vbox to \displace{% + \vfil + \rlap{$\left.\vrule height .5\displace width 0pt\right\}$#1}% + \vfil}}% +} +% \end{macrocode} +% \subsection{Patched commands from \textsf{bussproofs}} +% +% Some commands from \textsf{bussproofs.sty} have to be redefined to include +% |bussproofs-extra| functionality. Added/changed lines are indicated by a +% |%bpextra| comment +% \begin{macrocode} +\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{$\mathord{#1}\fCenter\mathord{\relax}$}% + \setbox\myBoxB=\hbox{$#2$}% %bpextra + \setbox\myBoxLLL=\hbox{\displayLeftLineLabel}% %bpextra + \setbox\myBoxRLL=\hbox{\displayRightLineLabel}% %bpextra + \global\setbox\curBox=% + \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 %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\AxiomC#1{ % Note argument not in math mode + % Get level and correct names set. + \prepAxiom% + % Define the box. + \setbox\myBoxA=\hbox{#1}% + \setbox\myBoxLLL=\hbox{\displayLeftLineLabel}% %bpextra + \setbox\myBoxRLL=\hbox{\displayRightLineLabel}% %bpextra + \global\setbox\curBox =% + \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\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{$\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{\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{#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\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 +} +% \end{macrocode} +% \Finale +% \PrintChanges +\endinput |