texlive[51299] Master/texmf-dist: bussproofs-extra (2jun19)
commits+karl at tug.org
commits+karl at tug.org
Sun Jun 2 23:47:33 CEST 2019
Revision: 51299
http://tug.org/svn/texlive?view=revision&revision=51299
Author: karl
Date: 2019-06-02 23:47:32 +0200 (Sun, 02 Jun 2019)
Log Message:
-----------
bussproofs-extra (2jun19)
Modified Paths:
--------------
trunk/Master/texmf-dist/doc/latex/bussproofs-extra/README.md
trunk/Master/texmf-dist/doc/latex/bussproofs-extra/bussproofs-extra.pdf
trunk/Master/texmf-dist/source/latex/bussproofs-extra/bussproofs-extra.dtx
trunk/Master/texmf-dist/tex/latex/bussproofs-extra/bussproofs-extra.sty
Added Paths:
-----------
trunk/Master/texmf-dist/doc/latex/bussproofs-extra/LICENSE.txt
Removed Paths:
-------------
trunk/Master/texmf-dist/source/latex/bussproofs-extra/Makefile
Added: trunk/Master/texmf-dist/doc/latex/bussproofs-extra/LICENSE.txt
===================================================================
--- trunk/Master/texmf-dist/doc/latex/bussproofs-extra/LICENSE.txt (rev 0)
+++ trunk/Master/texmf-dist/doc/latex/bussproofs-extra/LICENSE.txt 2019-06-02 21:47:32 UTC (rev 51299)
@@ -0,0 +1,416 @@
+The LaTeX Project Public License
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
+
+LPPL Version 1.3c 2008-05-04
+
+Copyright 1999 2002-2008 LaTeX3 Project
+ Everyone is allowed to distribute verbatim copies of this
+ license document, but modification of it is not allowed.
+
+
+PREAMBLE
+========
+
+The LaTeX Project Public License (LPPL) is the primary license under
+which the LaTeX kernel and the base LaTeX packages are distributed.
+
+You may use this license for any work of which you hold the copyright
+and which you wish to distribute. This license may be particularly
+suitable if your work is TeX-related (such as a LaTeX package), but
+it is written in such a way that you can use it even if your work is
+unrelated to TeX.
+
+The section `WHETHER AND HOW TO DISTRIBUTE WORKS UNDER THIS LICENSE',
+below, gives instructions, examples, and recommendations for authors
+who are considering distributing their works under this license.
+
+This license gives conditions under which a work may be distributed
+and modified, as well as conditions under which modified versions of
+that work may be distributed.
+
+We, the LaTeX3 Project, believe that the conditions below give you
+the freedom to make and distribute modified versions of your work
+that conform with whatever technical specifications you wish while
+maintaining the availability, integrity, and reliability of
+that work. If you do not see how to achieve your goal while
+meeting these conditions, then read the document `cfgguide.tex'
+and `modguide.tex' in the base LaTeX distribution for suggestions.
+
+
+DEFINITIONS
+===========
+
+In this license document the following terms are used:
+
+ `Work'
+ Any work being distributed under this License.
+
+ `Derived Work'
+ Any work that under any applicable law is derived from the Work.
+
+ `Modification'
+ Any procedure that produces a Derived Work under any applicable
+ law -- for example, the production of a file containing an
+ original file associated with the Work or a significant portion of
+ such a file, either verbatim or with modifications and/or
+ translated into another language.
+
+ `Modify'
+ To apply any procedure that produces a Derived Work under any
+ applicable law.
+
+ `Distribution'
+ Making copies of the Work available from one person to another, in
+ whole or in part. Distribution includes (but is not limited to)
+ making any electronic components of the Work accessible by
+ file transfer protocols such as FTP or HTTP or by shared file
+ systems such as Sun's Network File System (NFS).
+
+ `Compiled Work'
+ A version of the Work that has been processed into a form where it
+ is directly usable on a computer system. This processing may
+ include using installation facilities provided by the Work,
+ transformations of the Work, copying of components of the Work, or
+ other activities. Note that modification of any installation
+ facilities provided by the Work constitutes modification of the Work.
+
+ `Current Maintainer'
+ A person or persons nominated as such within the Work. If there is
+ no such explicit nomination then it is the `Copyright Holder' under
+ any applicable law.
+
+ `Base Interpreter'
+ A program or process that is normally needed for running or
+ interpreting a part or the whole of the Work.
+
+ A Base Interpreter may depend on external components but these
+ are not considered part of the Base Interpreter provided that each
+ external component clearly identifies itself whenever it is used
+ interactively. Unless explicitly specified when applying the
+ license to the Work, the only applicable Base Interpreter is a
+ `LaTeX-Format' or in the case of files belonging to the
+ `LaTeX-format' a program implementing the `TeX language'.
+
+
+
+CONDITIONS ON DISTRIBUTION AND MODIFICATION
+===========================================
+
+1. Activities other than distribution and/or modification of the Work
+are not covered by this license; they are outside its scope. In
+particular, the act of running the Work is not restricted and no
+requirements are made concerning any offers of support for the Work.
+
+2. You may distribute a complete, unmodified copy of the Work as you
+received it. Distribution of only part of the Work is considered
+modification of the Work, and no right to distribute such a Derived
+Work may be assumed under the terms of this clause.
+
+3. You may distribute a Compiled Work that has been generated from a
+complete, unmodified copy of the Work as distributed under Clause 2
+above, as long as that Compiled Work is distributed in such a way that
+the recipients may install the Compiled Work on their system exactly
+as it would have been installed if they generated a Compiled Work
+directly from the Work.
+
+4. If you are the Current Maintainer of the Work, you may, without
+restriction, modify the Work, thus creating a Derived Work. You may
+also distribute the Derived Work without restriction, including
+Compiled Works generated from the Derived Work. Derived Works
+distributed in this manner by the Current Maintainer are considered to
+be updated versions of the Work.
+
+5. If you are not the Current Maintainer of the Work, you may modify
+your copy of the Work, thus creating a Derived Work based on the Work,
+and compile this Derived Work, thus creating a Compiled Work based on
+the Derived Work.
+
+6. If you are not the Current Maintainer of the Work, you may
+distribute a Derived Work provided the following conditions are met
+for every component of the Work unless that component clearly states
+in the copyright notice that it is exempt from that condition. Only
+the Current Maintainer is allowed to add such statements of exemption
+to a component of the Work.
+
+ a. If a component of this Derived Work can be a direct replacement
+ for a component of the Work when that component is used with the
+ Base Interpreter, then, wherever this component of the Work
+ identifies itself to the user when used interactively with that
+ Base Interpreter, the replacement component of this Derived Work
+ clearly and unambiguously identifies itself as a modified version
+ of this component to the user when used interactively with that
+ Base Interpreter.
+
+ b. Every component of the Derived Work contains prominent notices
+ detailing the nature of the changes to that component, or a
+ prominent reference to another file that is distributed as part
+ of the Derived Work and that contains a complete and accurate log
+ of the changes.
+
+ c. No information in the Derived Work implies that any persons,
+ including (but not limited to) the authors of the original version
+ of the Work, provide any support, including (but not limited to)
+ the reporting and handling of errors, to recipients of the
+ Derived Work unless those persons have stated explicitly that
+ they do provide such support for the Derived Work.
+
+ d. You distribute at least one of the following with the Derived Work:
+
+ 1. A complete, unmodified copy of the Work;
+ if your distribution of a modified component is made by
+ offering access to copy the modified component from a
+ designated place, then offering equivalent access to copy
+ the Work from the same or some similar place meets this
+ condition, even though third parties are not compelled to
+ copy the Work along with the modified component;
+
+ 2. Information that is sufficient to obtain a complete,
+ unmodified copy of the Work.
+
+7. If you are not the Current Maintainer of the Work, you may
+distribute a Compiled Work generated from a Derived Work, as long as
+the Derived Work is distributed to all recipients of the Compiled
+Work, and as long as the conditions of Clause 6, above, are met with
+regard to the Derived Work.
+
+8. The conditions above are not intended to prohibit, and hence do not
+apply to, the modification, by any method, of any component so that it
+becomes identical to an updated version of that component of the Work as
+it is distributed by the Current Maintainer under Clause 4, above.
+
+9. Distribution of the Work or any Derived Work in an alternative
+format, where the Work or that Derived Work (in whole or in part) is
+then produced by applying some process to that format, does not relax or
+nullify any sections of this license as they pertain to the results of
+applying that process.
+
+10. a. A Derived Work may be distributed under a different license
+ provided that license itself honors the conditions listed in
+ Clause 6 above, in regard to the Work, though it does not have
+ to honor the rest of the conditions in this license.
+
+ b. If a Derived Work is distributed under a different license, that
+ Derived Work must provide sufficient documentation as part of
+ itself to allow each recipient of that Derived Work to honor the
+ restrictions in Clause 6 above, concerning changes from the Work.
+
+11. This license places no restrictions on works that are unrelated to
+the Work, nor does this license place any restrictions on aggregating
+such works with the Work by any means.
+
+12. Nothing in this license is intended to, or may be used to, prevent
+complete compliance by all parties with all applicable laws.
+
+
+NO WARRANTY
+===========
+
+There is no warranty for the Work. Except when otherwise stated in
+writing, the Copyright Holder provides the Work `as is', without
+warranty of any kind, either expressed or implied, including, but not
+limited to, the implied warranties of merchantability and fitness for a
+particular purpose. The entire risk as to the quality and performance
+of the Work is with you. Should the Work prove defective, you assume
+the cost of all necessary servicing, repair, or correction.
+
+In no event unless required by applicable law or agreed to in writing
+will The Copyright Holder, or any author named in the components of the
+Work, or any other party who may distribute and/or modify the Work as
+permitted above, be liable to you for damages, including any general,
+special, incidental or consequential damages arising out of any use of
+the Work or out of inability to use the Work (including, but not limited
+to, loss of data, data being rendered inaccurate, or losses sustained by
+anyone as a result of any failure of the Work to operate with any other
+programs), even if the Copyright Holder or said author or said other
+party has been advised of the possibility of such damages.
+
+
+MAINTENANCE OF THE WORK
+=======================
+
+The Work has the status `author-maintained' if the Copyright Holder
+explicitly and prominently states near the primary copyright notice in
+the Work that the Work can only be maintained by the Copyright Holder
+or simply that it is `author-maintained'.
+
+The Work has the status `maintained' if there is a Current Maintainer
+who has indicated in the Work that they are willing to receive error
+reports for the Work (for example, by supplying a valid e-mail
+address). It is not required for the Current Maintainer to acknowledge
+or act upon these error reports.
+
+The Work changes from status `maintained' to `unmaintained' if there
+is no Current Maintainer, or the person stated to be Current
+Maintainer of the work cannot be reached through the indicated means
+of communication for a period of six months, and there are no other
+significant signs of active maintenance.
+
+You can become the Current Maintainer of the Work by agreement with
+any existing Current Maintainer to take over this role.
+
+If the Work is unmaintained, you can become the Current Maintainer of
+the Work through the following steps:
+
+ 1. Make a reasonable attempt to trace the Current Maintainer (and
+ the Copyright Holder, if the two differ) through the means of
+ an Internet or similar search.
+
+ 2. If this search is successful, then enquire whether the Work
+ is still maintained.
+
+ a. If it is being maintained, then ask the Current Maintainer
+ to update their communication data within one month.
+
+ b. If the search is unsuccessful or no action to resume active
+ maintenance is taken by the Current Maintainer, then announce
+ within the pertinent community your intention to take over
+ maintenance. (If the Work is a LaTeX work, this could be
+ done, for example, by posting to comp.text.tex.)
+
+ 3a. If the Current Maintainer is reachable and agrees to pass
+ maintenance of the Work to you, then this takes effect
+ immediately upon announcement.
+
+ b. If the Current Maintainer is not reachable and the Copyright
+ Holder agrees that maintenance of the Work be passed to you,
+ then this takes effect immediately upon announcement.
+
+ 4. If you make an `intention announcement' as described in 2b. above
+ and after three months your intention is challenged neither by
+ the Current Maintainer nor by the Copyright Holder nor by other
+ people, then you may arrange for the Work to be changed so as
+ to name you as the (new) Current Maintainer.
+
+ 5. If the previously unreachable Current Maintainer becomes
+ reachable once more within three months of a change completed
+ under the terms of 3b) or 4), then that Current Maintainer must
+ become or remain the Current Maintainer upon request provided
+ they then update their communication data within one month.
+
+A change in the Current Maintainer does not, of itself, alter the fact
+that the Work is distributed under the LPPL license.
+
+If you become the Current Maintainer of the Work, you should
+immediately provide, within the Work, a prominent and unambiguous
+statement of your status as Current Maintainer. You should also
+announce your new status to the same pertinent community as
+in 2b) above.
+
+
+WHETHER AND HOW TO DISTRIBUTE WORKS UNDER THIS LICENSE
+======================================================
+
+This section contains important instructions, examples, and
+recommendations for authors who are considering distributing their
+works under this license. These authors are addressed as `you' in
+this section.
+
+Choosing This License or Another License
+----------------------------------------
+
+If for any part of your work you want or need to use *distribution*
+conditions that differ significantly from those in this license, then
+do not refer to this license anywhere in your work but, instead,
+distribute your work under a different license. You may use the text
+of this license as a model for your own license, but your license
+should not refer to the LPPL or otherwise give the impression that
+your work is distributed under the LPPL.
+
+The document `modguide.tex' in the base LaTeX distribution explains
+the motivation behind the conditions of this license. It explains,
+for example, why distributing LaTeX under the GNU General Public
+License (GPL) was considered inappropriate. Even if your work is
+unrelated to LaTeX, the discussion in `modguide.tex' may still be
+relevant, and authors intending to distribute their works under any
+license are encouraged to read it.
+
+A Recommendation on Modification Without Distribution
+-----------------------------------------------------
+
+It is wise never to modify a component of the Work, even for your own
+personal use, without also meeting the above conditions for
+distributing the modified component. While you might intend that such
+modifications will never be distributed, often this will happen by
+accident -- you may forget that you have modified that component; or
+it may not occur to you when allowing others to access the modified
+version that you are thus distributing it and violating the conditions
+of this license in ways that could have legal implications and, worse,
+cause problems for the community. It is therefore usually in your
+best interest to keep your copy of the Work identical with the public
+one. Many works provide ways to control the behavior of that work
+without altering any of its licensed components.
+
+How to Use This License
+-----------------------
+
+To use this license, place in each of the components of your work both
+an explicit copyright notice including your name and the year the work
+was authored and/or last substantially modified. Include also a
+statement that the distribution and/or modification of that
+component is constrained by the conditions in this license.
+
+Here is an example of such a notice and statement:
+
+ %% pig.dtx
+ %% Copyright 2005 M. Y. Name
+ %
+ % 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 M. Y. Name.
+ %
+ % This work consists of the files pig.dtx and pig.ins
+ % and the derived file pig.sty.
+
+Given such a notice and statement in a file, the conditions
+given in this license document would apply, with the `Work' referring
+to the three files `pig.dtx', `pig.ins', and `pig.sty' (the last being
+generated from `pig.dtx' using `pig.ins'), the `Base Interpreter'
+referring to any `LaTeX-Format', and both `Copyright Holder' and
+`Current Maintainer' referring to the person `M. Y. Name'.
+
+If you do not want the Maintenance section of LPPL to apply to your
+Work, change `maintained' above into `author-maintained'.
+However, we recommend that you use `maintained', as the Maintenance
+section was added in order to ensure that your Work remains useful to
+the community even when you can no longer maintain and support it
+yourself.
+
+Derived Works That Are Not Replacements
+---------------------------------------
+
+Several clauses of the LPPL specify means to provide reliability and
+stability for the user community. They therefore concern themselves
+with the case that a Derived Work is intended to be used as a
+(compatible or incompatible) replacement of the original Work. If
+this is not the case (e.g., if a few lines of code are reused for a
+completely different task), then clauses 6b and 6d shall not apply.
+
+
+Important Recommendations
+-------------------------
+
+ Defining What Constitutes the Work
+
+ The LPPL requires that distributions of the Work contain all the
+ files of the Work. It is therefore important that you provide a
+ way for the licensee to determine which files constitute the Work.
+ This could, for example, be achieved by explicitly listing all the
+ files of the Work near the copyright notice of each file or by
+ using a line such as:
+
+ % This work consists of all files listed in manifest.txt.
+
+ in that place. In the absence of an unequivocal list it might be
+ impossible for the licensee to determine what is considered by you
+ to comprise the Work and, in such a case, the licensee would be
+ entitled to make reasonable conjectures as to which files comprise
+ the Work.
+
Property changes on: trunk/Master/texmf-dist/doc/latex/bussproofs-extra/LICENSE.txt
___________________________________________________________________
Added: svn:eol-style
## -0,0 +1 ##
+native
\ No newline at end of property
Modified: trunk/Master/texmf-dist/doc/latex/bussproofs-extra/README.md
===================================================================
--- trunk/Master/texmf-dist/doc/latex/bussproofs-extra/README.md 2019-06-02 21:42:55 UTC (rev 51298)
+++ trunk/Master/texmf-dist/doc/latex/bussproofs-extra/README.md 2019-06-02 21:47:32 UTC (rev 51299)
@@ -11,9 +11,6 @@
To generate the documentation, run
```
pdflatex bussproofs-extra.dtx
-makeindex -s gglo.ist -o bussproofs-extra.gls bussproofs-extra.glo
-pdflatex bussproofs-extra.dtx
-pdflatex bussproofs-extra.dtx
```
This package is distributed under the terms of the LPPL 1.3c
Modified: trunk/Master/texmf-dist/doc/latex/bussproofs-extra/bussproofs-extra.pdf
===================================================================
(Binary files differ)
Deleted: trunk/Master/texmf-dist/source/latex/bussproofs-extra/Makefile
===================================================================
--- trunk/Master/texmf-dist/source/latex/bussproofs-extra/Makefile 2019-06-02 21:42:55 UTC (rev 51298)
+++ trunk/Master/texmf-dist/source/latex/bussproofs-extra/Makefile 2019-06-02 21:47:32 UTC (rev 51299)
@@ -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
Modified: trunk/Master/texmf-dist/source/latex/bussproofs-extra/bussproofs-extra.dtx
===================================================================
--- trunk/Master/texmf-dist/source/latex/bussproofs-extra/bussproofs-extra.dtx 2019-06-02 21:42:55 UTC (rev 51298)
+++ trunk/Master/texmf-dist/source/latex/bussproofs-extra/bussproofs-extra.dtx 2019-06-02 21:47:32 UTC (rev 51299)
@@ -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,9 +250,62 @@
% \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}
@@ -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
Modified: trunk/Master/texmf-dist/tex/latex/bussproofs-extra/bussproofs-extra.sty
===================================================================
--- trunk/Master/texmf-dist/tex/latex/bussproofs-extra/bussproofs-extra.sty 2019-06-02 21:42:55 UTC (rev 51298)
+++ trunk/Master/texmf-dist/tex/latex/bussproofs-extra/bussproofs-extra.sty 2019-06-02 21:47:32 UTC (rev 51299)
@@ -22,26 +22,34 @@
%%
\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{bussproofs-extra}
- [2019/04/04 0.3 Extra commands for bussproofs.sty]
+ [2019/05/31 0.4 Extra commands for bussproofs.sty]
-
\RequirePackage{bussproofs}
\RequirePackage{tikz}
-
\newdimen\CenterCorrection
\newdimen\DiagCorrection
+\newbox\myBoxLLL
+\newbox\myBoxRLL
+\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
@@ -49,7 +57,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
@@ -58,21 +66,18 @@
\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
}
-
\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
+ \setbox\myBoxA=\hbox{\fCenter}%
\global\CenterCorrection=-.5\wd\myBoxA
\joinDeduce%
\resetInferenceDefaults%
@@ -82,9 +87,7 @@
\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%
@@ -109,17 +112,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%
\buildDeduce%
\buildScoreLabels%
\ifx\rootAtBottomFlag\myTrue%
@@ -146,45 +138,33 @@
\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
-
\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
}
-
\def\resetInferenceDefaults{%
\global\def\theHypSeparation{\defaultHypSeparation}%
\global\setbox\myBoxLL=\hbox{\defaultLeftLabel}%
@@ -204,16 +184,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
}
@@ -221,44 +214,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
}
\endinput
%%
More information about the tex-live-commits
mailing list