From c5a40679707809a67789ed63672bd9b73fd31c41 Mon Sep 17 00:00:00 2001 From: Karl Berry Date: Thu, 4 Apr 2019 20:59:56 +0000 Subject: bussproofs-extra (4apr19) git-svn-id: svn://tug.org/texlive/trunk@50760 c570f23f-e606-0410-a88d-b1316a301751 --- .../doc/latex/bussproofs-extra/README.md | 19 + .../doc/latex/bussproofs-extra/bpextra.sty | 5 + .../latex/bussproofs-extra/bussproofs-extra.pdf | Bin 0 -> 233132 bytes .../source/latex/bussproofs-extra/Makefile | 10 + .../latex/bussproofs-extra/bussproofs-extra.dtx | 592 +++++++++++++++++++++ .../latex/bussproofs-extra/bussproofs-extra.ins | 57 ++ .../latex/bussproofs-extra/bussproofs-extra.sty | 265 +++++++++ Master/tlpkg/bin/tlpkg-ctan-check | 2 +- Master/tlpkg/libexec/ctan2tds | 1 + Master/tlpkg/tlpsrc/bussproofs-extra.tlpsrc | 0 Master/tlpkg/tlpsrc/collection-latexextra.tlpsrc | 1 - Master/tlpkg/tlpsrc/collection-mathscience.tlpsrc | 2 + 12 files changed, 952 insertions(+), 2 deletions(-) create mode 100644 Master/texmf-dist/doc/latex/bussproofs-extra/README.md create mode 100644 Master/texmf-dist/doc/latex/bussproofs-extra/bpextra.sty create mode 100644 Master/texmf-dist/doc/latex/bussproofs-extra/bussproofs-extra.pdf create mode 100644 Master/texmf-dist/source/latex/bussproofs-extra/Makefile create mode 100644 Master/texmf-dist/source/latex/bussproofs-extra/bussproofs-extra.dtx create mode 100644 Master/texmf-dist/source/latex/bussproofs-extra/bussproofs-extra.ins create mode 100644 Master/texmf-dist/tex/latex/bussproofs-extra/bussproofs-extra.sty create mode 100644 Master/tlpkg/tlpsrc/bussproofs-extra.tlpsrc (limited to 'Master') diff --git a/Master/texmf-dist/doc/latex/bussproofs-extra/README.md b/Master/texmf-dist/doc/latex/bussproofs-extra/README.md new file mode 100644 index 00000000000..2b8ed7088ce --- /dev/null +++ b/Master/texmf-dist/doc/latex/bussproofs-extra/README.md @@ -0,0 +1,19 @@ +bussproofs-extra +================ + +Additional functionality for bussproofs.sty. Specifically, it allows +for typesetting of entire (sub)deductions. + +To install, download the files, and run +``` +latex bussproofs-extra.ins +``` +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 diff --git a/Master/texmf-dist/doc/latex/bussproofs-extra/bpextra.sty b/Master/texmf-dist/doc/latex/bussproofs-extra/bpextra.sty new file mode 100644 index 00000000000..e83935d50d6 --- /dev/null +++ b/Master/texmf-dist/doc/latex/bussproofs-extra/bpextra.sty @@ -0,0 +1,5 @@ +% Wrapper for backwards compatibility + +\RequirePackage{bussproofs-extra} +\PackageWarning{bussproofs-extra}{You've loaded bussproofs with + bpextra, but you should use bussproofs-extra instead} diff --git a/Master/texmf-dist/doc/latex/bussproofs-extra/bussproofs-extra.pdf b/Master/texmf-dist/doc/latex/bussproofs-extra/bussproofs-extra.pdf new file mode 100644 index 00000000000..9075a6a8cc2 Binary files /dev/null and b/Master/texmf-dist/doc/latex/bussproofs-extra/bussproofs-extra.pdf differ diff --git a/Master/texmf-dist/source/latex/bussproofs-extra/Makefile b/Master/texmf-dist/source/latex/bussproofs-extra/Makefile new file mode 100644 index 00000000000..3285cb49a3f --- /dev/null +++ b/Master/texmf-dist/source/latex/bussproofs-extra/Makefile @@ -0,0 +1,10 @@ +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 new file mode 100644 index 00000000000..59cc56e7503 --- /dev/null +++ b/Master/texmf-dist/source/latex/bussproofs-extra/bussproofs-extra.dtx @@ -0,0 +1,592 @@ +% \iffalse meta-comment +% +% +% Copyright (C) 2019 by Richard Zach +% ------------------------------------------------------ +% +% 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} +% +%\NeedsTeXFormat{LaTeX2e} +%\ProvidesPackage{bussproofs-extra} +% [2019/04/04 0.3 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 + +\renewcommand{\fCenter}{\ensuremath{\,{\to}\,}} + +\EnableCrossrefs +\CodelineIndex +\RecordChanges +\begin{document} + \DocInput{bussproofs-extra.dtx} + \PrintChanges + \PrintIndex +\end{document} +% +% \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.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://ucalgary.ca/rzach/}{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 +% \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!} +% \end{enumerate} +% +% Here's what these deductions look like: +% +% \begin{center} +% \begin{tabular}{@{}llll@{}} +% \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$ +% \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} +% \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} + + +% +% \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} +% +% \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} +% \subsection{Deduce Styles} +% +% The following commands set the style for the next |\Deduce| +% command. |\straightDeduce| produces a simple vertical line of dots, +% |\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. +% \begin{macrocode} +\def\straightDeduce{% + \gdef\fDeduce{\tikz\draw[very thick,loosely dotted] (0,0) -- (0,1);} + \global\DiagCorrection=0pt + \ignorespaces +} + +\def\branchDeduce{% + \gdef\fDeduce{\begin{tikzpicture} + \draw[very thick,loosely dotted] (0,0) -- (0,1); + \draw[very thick,loosely dotted] (-.5,.5) -- (0,0); + \draw[very thick,loosely dotted] (.5,.5) -- (0,0); + \end{tikzpicture}} + \global\DiagCorrection=0pt + \ignorespaces +} + +\def\ddotsDeduce{% + \gdef\fDeduce{\begin{tikzpicture} + \draw[very thick,loosely dotted] (0,1) -- (1,0); + \end{tikzpicture}} + \setbox\myBoxA=\hbox{\fDeduce} + \global\DiagCorrection=-\wd\myBoxA + \ignorespaces +} + +\def\dotsdDeduce{% + \gdef\fDeduce{\begin{tikzpicture} + \draw[very thick,loosely dotted] (1,1) -- (0,0); + \end{tikzpicture}} + \setbox\myBoxA=\hbox{\fDeduce} + \global\DiagCorrection=\wd\myBoxA + \ignorespaces +} + +\def\alwaysDeduce{\straightDeduce} +\straightDeduce + +% \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} + % if we align at \fCenter, move \fDeduce left by 1/2 width of \fCenter + \global\CenterCorrection=-.5\wd\myBoxA + \joinDeduce% + \resetInferenceDefaults% + \ignorespaces% +} + +\def\DeduceC#1{ + \prepUnary% + \buildConclusionC{#1}% + % vdot alignment is off by a bit, correct + \global\CenterCorrection=-4pt + % Align and join the curBox and the new box into one vbox. + \joinDeduce% + \resetInferenceDefaults% + \ignorespaces% +} + +% \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 + %\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} + \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{% + \llap{#1\hskip\ScoreOverhangLeft\hskip\labelSpacing}} + \ignorespaces} + +\def\RightLineLabel#1{% + \global\def\displayRightLineLabel{ + \rlap{\hskip\ScoreOverhangLeft\hskip\labelSpacing #1}} + \ignorespaces} + +\global\let\displayLeftLineLabel\relax +\global\let\displayRightLineLabel\relax + +% \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 = +<<<<<<< HEAD:bussproofs-extra.dtx + \hbox{\vbox to \ht\curBox{\vfil\llap{#1 + $\left\{\vrule height .5\ht\curBox width 0pt\right.$}\vfil}\box\curBox}% +======= + \hbox{\vbox to \ht\curBox{% + \vfil + \llap{#1$\left\{\vrule height .5\ht\curBox width 0pt\right.$}% + \vfil}\box\curBox}% +>>>>>>> 4823829694ec2392dad7e3c55cd366f991c7c6db:bpextra.dtx +} + +\def\RightSubproofLabel#1{% + \displace=\ht\curBox + \global\setbox\curBox = +<<<<<<< HEAD:bussproofs-extra.dtx + \hbox{\box\curBox\vbox to \displace{\vfil + \rlap{$\left.\vrule height .5\displace width 0pt\right\}$#1}\vfil}}% +======= + \hbox{\box\curBox\vbox to \displace{% + \vfil + \rlap{$\left.\vrule height .5\displace width 0pt\right\}$#1} + \vfil}}% +>>>>>>> 4823829694ec2392dad7e3c55cd366f991c7c6db:bpextra.dtx +} + +% \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{\displayLeftLineLabel$\mathord{#1}\fCenter\mathord{\relax}$}% %bpextra + \setbox\myBoxB=\hbox{$#2$\displayRightLineLabel}% %bpextra + \global\setbox\curBox=% + \hbox{\hskip\ScoreOverhangLeft\relax% + \unhcopy\myBoxA\unhcopy\myBoxB\hskip\ScoreOverhangRight\relax}% + % Set the relevant dimensions for the boxes + \global\curScoreStart=0pt \relax + \global\curScoreEnd=\wd\curBox \relax + \global\curCenter=\wd\myBoxA \relax + \global\advance \curCenter by \ScoreOverhangLeft% + \ignorespaces +} + +\def\AxiomC#1{ % Note argument not in math mode + % Get level and correct names set. + \prepAxiom% + % Define the box. + \setbox\myBoxA=\hbox{\displayLeftLineLabel #1\displayRightLineLabel}% %bpextra + \global\setbox\curBox =% + \hbox{\hskip\ScoreOverhangLeft\relax% + \unhcopy\myBoxA\hskip\ScoreOverhangRight\relax}% + % Set the relevant dimensions for the boxes + \global\curScoreStart=0pt \relax + \global\curScoreEnd=\wd\curBox \relax + \global\curCenter=.5\wd\curBox \relax + \global\advance \curCenter by \ScoreOverhangLeft% + \ignorespaces +} + +\def\buildConclusion#1#2{% Build lower sequent w/ center at \fCenter position. + % Define the boxes + \setbox\myBoxA=\hbox{\displayLeftLineLabel $\mathord{#1}\fCenter\mathord{\relax}$}% %bpextra + \setbox\myBoxB=\hbox{$#2$\displayRightLineLabel}% %bpextra + % Put them together in \myBoxC + \setbox\myBoxC =% + \hbox{\hskip\ScoreOverhangLeft\relax% + \unhcopy\myBoxA\unhcopy\myBoxB\hskip\ScoreOverhangRight\relax}% + % Calculate the center of the \myBoxC string. + \newScoreStart=0pt \relax% + \newCenter=\wd\myBoxA \relax% + \advance \newCenter by \ScoreOverhangLeft% + \newScoreEnd=\wd\myBoxC% +} + +\def\buildConclusionC#1{% Build lower sequent w/o \fCenter present. + % Define the box. + \setbox\myBoxA=\hbox{\displayLeftLineLabel #1\displayRightLineLabel}% %bpextra + \setbox\myBoxC =% + \hbox{\hbox{\hskip\ScoreOverhangLeft\relax% + \unhcopy\myBoxA\hskip\ScoreOverhangRight\relax}}% + % Calculate kerning to line up centers + \newScoreStart=0pt \relax% + \newCenter=.5\wd\myBoxC \relax% + \newScoreEnd=\wd\myBoxC% + \advance \newCenter by \ScoreOverhangLeft% +} +% \end{macrocode} +% \Finale +% \PrintChanges +\endinput diff --git a/Master/texmf-dist/source/latex/bussproofs-extra/bussproofs-extra.ins b/Master/texmf-dist/source/latex/bussproofs-extra/bussproofs-extra.ins new file mode 100644 index 00000000000..e511feff730 --- /dev/null +++ b/Master/texmf-dist/source/latex/bussproofs-extra/bussproofs-extra.ins @@ -0,0 +1,57 @@ +%% +%% Copyright (C) 2019 by Richard Zach +%% +%% This file may be distributed and/or modified under the conditions of +%% the LaTeX Project Public License, either version 1.2 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.2 or later is part of all distributions of LaTeX version +%% 1999/12/01 or later. +%% + +\input docstrip.tex +\keepsilent + +\usedir{tex/latex/bussproofs-extra} + +\preamble + +This is a generated file. + +Copyright (C) 2019 by Richard Zach + +This file may be distributed and/or modified under the conditions of +the LaTeX Project Public License, either version 1.3 of this license +or (at your option) any later version. The latest version of this +license is in: + + http://www.latex-project.org/lppl.txt + +and version 1.3 or later is part of all distributions of LaTeX version +1999/12/01 or later. + +\endpreamble + +\generate{\file{bussproofs-extra.sty}{\from{bussproofs-extra.dtx}{package}}} + +\obeyspaces +\Msg{*************************************************************} +\Msg{* *} +\Msg{* To finish the installation you have to move the following *} +\Msg{* file into a directory searched by TeX: *} +\Msg{* *} +\Msg{* bussproofs-extra.sty *} +\Msg{* *} +\Msg{* To produce the documentation run the file bpextra.dtx *} +\Msg{* through LaTeX, and then *} +\Msg{* makeindex -s gglo.ist -o bussproofs-extra.gls bussproofs-extra.glo *} +\Msg{* Then run LaTeX on bussproofs-extra.dtx again *} +\Msg{* *} +\Msg{* Happy TeXing! *} +\Msg{* *} +\Msg{*************************************************************} + +\endbatchfile diff --git a/Master/texmf-dist/tex/latex/bussproofs-extra/bussproofs-extra.sty b/Master/texmf-dist/tex/latex/bussproofs-extra/bussproofs-extra.sty new file mode 100644 index 00000000000..e740e1ef218 --- /dev/null +++ b/Master/texmf-dist/tex/latex/bussproofs-extra/bussproofs-extra.sty @@ -0,0 +1,265 @@ +%% +%% This is file `bussproofs-extra.sty', +%% generated with the docstrip utility. +%% +%% The original source files were: +%% +%% bussproofs-extra.dtx (with options: `package') +%% +%% This is a generated file. +%% +%% Copyright (C) 2019 by Richard Zach +%% +%% This file may be distributed and/or modified under the conditions of +%% the LaTeX Project Public License, either version 1.3 of this license +%% or (at your option) any later version. The latest version of this +%% license is in: +%% +%% http://www.latex-project.org/lppl.txt +%% +%% and version 1.3 or later is part of all distributions of LaTeX version +%% 1999/12/01 or later. +%% +\NeedsTeXFormat{LaTeX2e} +\ProvidesPackage{bussproofs-extra} + [2019/04/04 0.3 Extra commands for bussproofs.sty] + + +\RequirePackage{bussproofs} +\RequirePackage{tikz} + +\newdimen\CenterCorrection +\newdimen\DiagCorrection + +\def\straightDeduce{% + \gdef\fDeduce{\tikz\draw[very thick,loosely dotted] (0,0) -- (0,1);} + \global\DiagCorrection=0pt + \ignorespaces +} + +\def\branchDeduce{% + \gdef\fDeduce{\begin{tikzpicture} + \draw[very thick,loosely dotted] (0,0) -- (0,1); + \draw[very thick,loosely dotted] (-.5,.5) -- (0,0); + \draw[very thick,loosely dotted] (.5,.5) -- (0,0); + \end{tikzpicture}} + \global\DiagCorrection=0pt + \ignorespaces +} + +\def\ddotsDeduce{% + \gdef\fDeduce{\begin{tikzpicture} + \draw[very thick,loosely dotted] (0,1) -- (1,0); + \end{tikzpicture}} + \setbox\myBoxA=\hbox{\fDeduce} + \global\DiagCorrection=-\wd\myBoxA + \ignorespaces +} + +\def\dotsdDeduce{% + \gdef\fDeduce{\begin{tikzpicture} + \draw[very thick,loosely dotted] (1,1) -- (0,0); + \end{tikzpicture}} + \setbox\myBoxA=\hbox{\fDeduce} + \global\DiagCorrection=\wd\myBoxA + \ignorespaces +} + +\def\alwaysDeduce{\straightDeduce} +\straightDeduce + +\def\Deduce$#1\fCenter#2${% + \prepUnary% + \buildConclusion{#1}{#2}% + \setbox\myBoxA=\hbox{\fCenter} + % if we align at \fCenter, move \fDeduce left by 1/2 width of \fCenter + \global\CenterCorrection=-.5\wd\myBoxA + \joinDeduce% + \resetInferenceDefaults% + \ignorespaces% +} + +\def\DeduceC#1{ + \prepUnary% + \buildConclusionC{#1}% + % vdot alignment is off by a bit, correct + \global\CenterCorrection=-4pt + % Align and join the curBox and the new box into one vbox. + \joinDeduce% + \resetInferenceDefaults% + \ignorespaces% +} + +\def\joinDeduce{% + \global\advance\curCenter by -\hypKernAmt% + \ifnum\curCenter<\newCenter% + \displace=\newCenter% + \advance \displace by -\curCenter% + \kernUpperBox% + \else% + \displace=\curCenter% + \advance \displace by -\newCenter% + \kernLowerBox% + \fi% + \ifnum\DiagCorrection<0% + \displace=-\DiagCorrection + \kernLowerBox% + \else + \displace=\DiagCorrection + \kernUpperBox% + \fi% + \advance\curCenter by-.5\DiagCorrection + %\ifnum \newScoreStart < \curScoreStart % + % \global \curScoreStart = \newScoreStart \fi% + %\ifnum \curScoreEnd < \newScoreEnd % + % \global \curScoreEnd = \newScoreEnd \fi% + % Leave room for the left label. + %\ifnum \curScoreStart<\wd\myBoxLL% + % \global\displace = \wd\myBoxLL% + % \global\advance\displace by -\curScoreStart% + % \kernUpperBox% + % \kernLowerBox% + %\fi% + \buildDeduce% + \buildScoreLabels% + \ifx\rootAtBottomFlag\myTrue% + \buildRootBottom% + \else% + \buildRootTop% + \fi% + \global \curScoreStart=\newScoreStart% + \global \curScoreEnd=\newScoreEnd% + \global \curCenter=\newCenter% +} + +\def\buildDeduce{% + \global\setbox \myBoxD =% + \hbox{\fDeduce}% + \displace = \wd\myBoxD % find width of vdots + \global\curScoreStart = \curCenter% + \global\advance\curScoreStart by -.5\displace% + \global\curScoreEnd = \curCenter% + \global\advance\curScoreEnd by .5\displace% + \global\advance\curScoreStart by\CenterCorrection + \global\advance\curScoreEnd by\CenterCorrection +} + +\def\LeftLineLabel#1{% + \global\def\displayLeftLineLabel{% + \llap{#1\hskip\ScoreOverhangLeft\hskip\labelSpacing}} + \ignorespaces} + +\def\RightLineLabel#1{% + \global\def\displayRightLineLabel{ + \rlap{\hskip\ScoreOverhangLeft\hskip\labelSpacing #1}} + \ignorespaces} + +\global\let\displayLeftLineLabel\relax +\global\let\displayRightLineLabel\relax + + +\def\LeftSubproofLabel#1{% + \global\setbox\curBox = +<<<<<<< HEAD:bussproofs-extra.dtx + \hbox{\vbox to \ht\curBox{\vfil\llap{#1 + $\left\{\vrule height .5\ht\curBox width 0pt\right.$}\vfil}\box\curBox}% +======= + \hbox{\vbox to \ht\curBox{% + \vfil + \llap{#1$\left\{\vrule height .5\ht\curBox width 0pt\right.$}% + \vfil}\box\curBox}% +>>>>>>> 4823829694ec2392dad7e3c55cd366f991c7c6db:bpextra.dtx +} + +\def\RightSubproofLabel#1{% + \displace=\ht\curBox + \global\setbox\curBox = +<<<<<<< HEAD:bussproofs-extra.dtx + \hbox{\box\curBox\vbox to \displace{\vfil + \rlap{$\left.\vrule height .5\displace width 0pt\right\}$#1}\vfil}}% +======= + \hbox{\box\curBox\vbox to \displace{% + \vfil + \rlap{$\left.\vrule height .5\displace width 0pt\right\}$#1} + \vfil}}% +>>>>>>> 4823829694ec2392dad7e3c55cd366f991c7c6db:bpextra.dtx +} + +\def\resetInferenceDefaults{% + \global\def\theHypSeparation{\defaultHypSeparation}% + \global\setbox\myBoxLL=\hbox{\defaultLeftLabel}% + \global\setbox\myBoxRL=\hbox{\defaultRightLabel}% + \global\def\buildScore{\alwaysBuildScore}% + \global\def\theScoreFiller{\alwaysScoreFiller}% + % reset line labels to nothing %bpextra + \global\let\displayLeftLineLabel\relax %bpextra + \global\let\displayRightLineLabel\relax %bpextra + % reset to defaul deduce style %bpextra + \alwaysDeduce %bpextra + \gdef\hypKernAmt{0pt}% Restore to zero kerning. +} + +\def\Axiom$#1\fCenter#2${% + % Get level and correct names set. + \prepAxiom% + % Define the boxes + % bpextra -- add line labels + \setbox\myBoxA=\hbox{\displayLeftLineLabel$\mathord{#1}\fCenter\mathord{\relax}$}% %bpextra + \setbox\myBoxB=\hbox{$#2$\displayRightLineLabel}% %bpextra + \global\setbox\curBox=% + \hbox{\hskip\ScoreOverhangLeft\relax% + \unhcopy\myBoxA\unhcopy\myBoxB\hskip\ScoreOverhangRight\relax}% + % Set the relevant dimensions for the boxes + \global\curScoreStart=0pt \relax + \global\curScoreEnd=\wd\curBox \relax + \global\curCenter=\wd\myBoxA \relax + \global\advance \curCenter by \ScoreOverhangLeft% + \ignorespaces +} + +\def\AxiomC#1{ % Note argument not in math mode + % Get level and correct names set. + \prepAxiom% + % Define the box. + \setbox\myBoxA=\hbox{\displayLeftLineLabel #1\displayRightLineLabel}% %bpextra + \global\setbox\curBox =% + \hbox{\hskip\ScoreOverhangLeft\relax% + \unhcopy\myBoxA\hskip\ScoreOverhangRight\relax}% + % Set the relevant dimensions for the boxes + \global\curScoreStart=0pt \relax + \global\curScoreEnd=\wd\curBox \relax + \global\curCenter=.5\wd\curBox \relax + \global\advance \curCenter by \ScoreOverhangLeft% + \ignorespaces +} + +\def\buildConclusion#1#2{% Build lower sequent w/ center at \fCenter position. + % Define the boxes + \setbox\myBoxA=\hbox{\displayLeftLineLabel $\mathord{#1}\fCenter\mathord{\relax}$}% %bpextra + \setbox\myBoxB=\hbox{$#2$\displayRightLineLabel}% %bpextra + % Put them together in \myBoxC + \setbox\myBoxC =% + \hbox{\hskip\ScoreOverhangLeft\relax% + \unhcopy\myBoxA\unhcopy\myBoxB\hskip\ScoreOverhangRight\relax}% + % Calculate the center of the \myBoxC string. + \newScoreStart=0pt \relax% + \newCenter=\wd\myBoxA \relax% + \advance \newCenter by \ScoreOverhangLeft% + \newScoreEnd=\wd\myBoxC% +} + +\def\buildConclusionC#1{% Build lower sequent w/o \fCenter present. + % Define the box. + \setbox\myBoxA=\hbox{\displayLeftLineLabel #1\displayRightLineLabel}% %bpextra + \setbox\myBoxC =% + \hbox{\hbox{\hskip\ScoreOverhangLeft\relax% + \unhcopy\myBoxA\hskip\ScoreOverhangRight\relax}}% + % Calculate kerning to line up centers + \newScoreStart=0pt \relax% + \newCenter=.5\wd\myBoxC \relax% + \newScoreEnd=\wd\myBoxC% + \advance \newCenter by \ScoreOverhangLeft% +} +\endinput +%% +%% End of file `bussproofs-extra.sty'. diff --git a/Master/tlpkg/bin/tlpkg-ctan-check b/Master/tlpkg/bin/tlpkg-ctan-check index 79eafd062a4..836581a51d6 100755 --- a/Master/tlpkg/bin/tlpkg-ctan-check +++ b/Master/tlpkg/bin/tlpkg-ctan-check @@ -128,7 +128,7 @@ my @TLP_working = qw( br-lex bracketkey braids braille braket brandeis-dissertation brandeis-problemset breakcites breakurl bredzenie breqn bropd brushscr - bullcntr bundledoc burmese businesscard-qrcode bussproofs + bullcntr bundledoc burmese businesscard-qrcode bussproofs bussproofs-extra bxbase bxcalc bxcjkjatype bxdpx-beamer bxdvidriver bxjaholiday bxjaprnind bxpapersize bxpdfver bxeepic bxenclose bxjalipsum bxjscls bxnewfont bxorigcapt bxtexlogo bxwareki bytefield diff --git a/Master/tlpkg/libexec/ctan2tds b/Master/tlpkg/libexec/ctan2tds index d8bad3cc209..1ce7d296eee 100755 --- a/Master/tlpkg/libexec/ctan2tds +++ b/Master/tlpkg/libexec/ctan2tds @@ -1663,6 +1663,7 @@ $standardtex 'blockdraw_mp','NULL', # skip .sty's 'booktabs-de', 'NULL', # doc package 'booktabs-fr', 'NULL', # doc package + 'bussproofs-extra', 'bussproofs-extra.sty', # not bpextra.sty 'breqn', '\.sty|\.sym', 'c-pascal', '^[^d].*\.tex|' . $standardtex, # not demo*.tex 'calxxxx', 'cal.*\.tex', diff --git a/Master/tlpkg/tlpsrc/bussproofs-extra.tlpsrc b/Master/tlpkg/tlpsrc/bussproofs-extra.tlpsrc new file mode 100644 index 00000000000..e69de29bb2d diff --git a/Master/tlpkg/tlpsrc/collection-latexextra.tlpsrc b/Master/tlpkg/tlpsrc/collection-latexextra.tlpsrc index 93457572451..d31e83ed24f 100644 --- a/Master/tlpkg/tlpsrc/collection-latexextra.tlpsrc +++ b/Master/tlpkg/tlpsrc/collection-latexextra.tlpsrc @@ -110,7 +110,6 @@ depend bracketkey depend braket depend breakurl depend bullcntr -depend bussproofs depend bxcalc depend bxdpx-beamer depend bxdvidriver diff --git a/Master/tlpkg/tlpsrc/collection-mathscience.tlpsrc b/Master/tlpkg/tlpsrc/collection-mathscience.tlpsrc index f9abeffdd81..cbf9c645cbb 100644 --- a/Master/tlpkg/tlpsrc/collection-mathscience.tlpsrc +++ b/Master/tlpkg/tlpsrc/collection-mathscience.tlpsrc @@ -27,6 +27,8 @@ depend boldtensors depend bosisio depend bpchem depend bropd +depend bussproofs +depend bussproofs-extra depend bytefield depend calculation depend cascade -- cgit v1.2.3