bussproofs-extra (2jun19)

git-svn-id: svn://tug.org/texlive/trunk@51299 c570f23f-e606-0410-a88d-b1316a301751

2 files changed, 180 insertions, 97 deletions

diff --git a/Master/texmf-dist/source/latex/bussproofs-extra/Makefile b/Master/texmf-dist/source/latex/bussproofs-extra/Makefile
deleted file mode 100644
index 3285cb49a3f..00000000000
--- a/Master/texmf-dist/source/latex/bussproofs-extra/Makefile
+++ /dev/null
@@ -1,10 +0,0 @@
-ALL: bussproofs-extra.sty bussproofs-extra.pdf
-
-bussproofs-extra.sty: bussproofs-extra.dtx bussproofs-extra.ins
-	latex bussproofs-extra.ins
-
-bussproofs-extra.pdf: bussproofs-extra.sty
-	pdflatex bussproofs-extra.dtx
-	makeindex -s gglo.ist -o bussproofs-extra.gls bussproofs-extra.glo
-	pdflatex bussproofs-extra.dtx
-	pdflatex bussproofs-extra.dtx
diff --git a/Master/texmf-dist/source/latex/bussproofs-extra/bussproofs-extra.dtx b/Master/texmf-dist/source/latex/bussproofs-extra/bussproofs-extra.dtx
index 59cc56e7503..a371cff408f 100644
--- a/Master/texmf-dist/source/latex/bussproofs-extra/bussproofs-extra.dtx
+++ b/Master/texmf-dist/source/latex/bussproofs-extra/bussproofs-extra.dtx
@@ -27,27 +27,21 @@
 %</driver>
 %<package>\NeedsTeXFormat{LaTeX2e}
 %<package>\ProvidesPackage{bussproofs-extra}
-%<package>   [2019/04/04 0.3 Extra commands for bussproofs.sty]
+%<package>   [2019/05/31 0.4 Extra commands for bussproofs.sty]
 %<*driver>
 \documentclass{ltxdoc}
 
-<<<<<<< HEAD:bussproofs-extra.dtx
 \usepackage{bussproofs-extra}
-\usepackage[colorlinks]{hyperref}
-=======
-\usepackage{bpextra}
 \usepackage[colorlinks,allcolors=blue]{hyperref}
->>>>>>> 4823829694ec2392dad7e3c55cd366f991c7c6db:bpextra.dtx
+\usepackage{calc}
 
 \renewcommand{\fCenter}{\ensuremath{\,{\to}\,}}
 
 \EnableCrossrefs         
-\CodelineIndex
 \RecordChanges
 \begin{document}
   \DocInput{bussproofs-extra.dtx}
   \PrintChanges
-  \PrintIndex
 \end{document}
 %</driver>
 % \fi
@@ -71,10 +65,11 @@
 %   Right brace   \}     Tilde         \~}
 %
 %
-% \changes{v0.3}{2019/04/04}{Rename to bussproofs-extra.sty}
+% \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}
+% \changes{v0.1}{2014/04/26}{Initial version with deduce, linelabel functionality}
 %
 % \GetFileInfo{bussproofs-extra.sty}
 %
@@ -83,7 +78,7 @@
 %
 % \title{The \textsf{bussproofs-extra} package\thanks{This document
 %   corresponds to \textsf{bussproofs-extra}~\fileversion, dated \filedate.}}
-% \author{\href{http://ucalgary.ca/rzach/}{Richard Zach}}
+% \author{\href{http://richardzach.org/}{Richard Zach}}
 % \date{}
 %
 % \maketitle
@@ -99,7 +94,7 @@
 %
 % \begin{enumerate}
 % \item |\Deduce$| and |\DeduceC| commands, which work much
-%  like |\Infer|, commands but indicate missing parts of a proof.
+%  like |\Infer| commands but indicate missing parts of a proof.
 % \item Multiple styles for typesetting the result of |\Deduce|,
 % including 
 % \begin{enumerate}
@@ -109,19 +104,23 @@
 %  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 intead of the score
-%   line.  \textbf{These don't work properly and may be removed!}
+%   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}{@{}llll@{}}
+% \begin{tabular}{@{}cccc@{}}
 % \fbox{\AxiomC{$A$}
 % \straightDeduce
 % \DeduceC{$B$}
@@ -163,11 +162,10 @@
 % \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}
@@ -225,13 +223,16 @@
 % \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}
@@ -249,8 +250,61 @@
 % \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{}
 %
@@ -264,9 +318,8 @@
 %    \begin{macrocode}
 \RequirePackage{bussproofs}
 \RequirePackage{tikz}
-
 %    \end{macrocode}
-% \subsection{Dimensions}
+% \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
@@ -276,31 +329,45 @@
 %    \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 |\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.
+% 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[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
@@ -308,7 +375,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
@@ -317,16 +384,19 @@
 
 \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
 }
-
+%    \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}}
@@ -338,8 +408,7 @@
 \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%
@@ -349,14 +418,11 @@
 \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%
 }
-
 %    \end{macrocode}
 % \section{Typesetting the Deduction}
 % 
@@ -366,6 +432,7 @@
 % |\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}
@@ -394,17 +461,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%
 %    \end{macrocode}
 % Now we draw the deduction.
 %    \begin{macrocode}
@@ -426,12 +482,12 @@
     \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}%
@@ -447,7 +503,6 @@
     \global\advance\curScoreStart by\CenterCorrection
     \global\advance\curScoreEnd by\CenterCorrection
 }
-
 %    \end{macrocode}
 % \subsection{Line Labels}
 % 
@@ -457,19 +512,19 @@
 % produced by |\LeftLabel| and |\RightLabel| (i.e., the distance to
 % the line is $|\ScoreOverhang| + |\labelSpacing|$.
 %    \begin{macrocode}
+
 \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
-
 %    \end{macrocode}
 %
 % \subsection{Subproof Labels}
@@ -479,31 +534,20 @@
 
 \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
 }
-
 %    \end{macrocode}
 % \subsection{Patched commands from \textsf{bussproofs}}
 %
@@ -530,16 +574,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
 }
 
@@ -547,44 +604,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
 }
 %    \end{macrocode}
 % \Finale