From da01f156c51c5a5b7b85040fbfccd492c5036e8a Mon Sep 17 00:00:00 2001 From: Karl Berry Date: Thu, 20 Aug 2020 21:09:58 +0000 Subject: ebproof (20aug20) git-svn-id: svn://tug.org/texlive/trunk@56139 c570f23f-e606-0410-a88d-b1316a301751 --- Master/texmf-dist/source/latex/ebproof/ebproof.dtx | 1629 ++++++++++++++++++++ Master/texmf-dist/source/latex/ebproof/ebproof.ins | 15 + 2 files changed, 1644 insertions(+) create mode 100644 Master/texmf-dist/source/latex/ebproof/ebproof.dtx create mode 100644 Master/texmf-dist/source/latex/ebproof/ebproof.ins (limited to 'Master/texmf-dist/source/latex/ebproof') diff --git a/Master/texmf-dist/source/latex/ebproof/ebproof.dtx b/Master/texmf-dist/source/latex/ebproof/ebproof.dtx new file mode 100644 index 00000000000..71735ffc007 --- /dev/null +++ b/Master/texmf-dist/source/latex/ebproof/ebproof.dtx @@ -0,0 +1,1629 @@ +% \iffalse meta-comment +% +% Copyright (C) 2015-2020 by Emmanuel Beffara +% +% 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 +% 2005/12/01 or later. +% +%<*driver> +\documentclass[full]{l3doc} +\usepackage{ebproof} +\usepackage{multicol} +\usepackage{tikz} +\usetikzlibrary{decorations.pathmorphing} +\EnableCrossrefs +\newenvironment{example}{% + \VerbatimEnvironment + \begin{VerbatimOut}{example.tex}}{% + \end{VerbatimOut} + \begin{center} + \begin{minipage}{.4\textwidth} + \input{example.tex} + \end{minipage}% + \begin{minipage}{.6\textwidth} + \small\VerbatimInput[gobble=0]{example.tex} + \end{minipage}% + \end{center} +} +\begin{document} + \DocInput{\jobname.dtx} +\end{document} +% +% \fi +% +% \title{^^A +% The \pkg{ebproof} package \\ +% Formal proofs in the style of sequent calculus^^A +% } +% +% \author{^^A +% Emmanuel Beffara\thanks +% {^^A +% E-mail: \href{mailto:manu@beffara.org}{manu@beffara.org}^^A +% }^^A +% } +% +% \date{Version 2.1 -- Released 2020-08-19} +% +% \maketitle +% +% \setcounter{tocdepth}{2} +% \begin{multicols}{2} +% \tableofcontents +% \end{multicols} +% +% \begin{documentation} +% +% \section{Introduction} +% +% The \pkg{ebproof} package provides commands to typeset proof trees, in the +% style of sequent calculus and related systems: +% +% \begin{example} +% \begin{prooftree} +% \hypo{ \Gamma, A &\vdash B } +% \infer1[abs]{ \Gamma &\vdash A\to B } +% \hypo{ \Gamma \vdash A } +% \infer2[app]{ \Gamma \vdash B } +% \end{prooftree} +% \end{example} +% +% The structure is very much inspired by the +% \href{http://math.ucsd.edu/~sbuss/ResearchWeb/bussproofs/}{\pkg{bussproofs}} +% package, in particular for the postfix notation. +% I actually wrote \pkg{ebproof} because there were some limitations in +% \pkg{bussproofs} that I did not know how to lift, and also because I did +% not like some choices in that package (and also because it was fun to write). +% +% Any feedback is welcome, in the form of bug reports, feature requests or +% suggestions, through the web page of the project at \url{https://framagit.org/manu/ebproof}. +% +% \section{Environments} +% +% \begin{function}{prooftree,prooftree*} +% \begin{syntax} +% \verb|\begin{prooftree}|\oarg{options} +% ~ \meta{statements} +% \verb|\end{prooftree}| +% \end{syntax} +% The package provides the \env{prooftree} environment, in standard and +% starred variants. +% This typesets the proof tree described by the \meta{statements}, as +% described in section~\ref{sec:statements}. +% The \meta{options} provide default formatting options for the proof tree, +% available options are described in section~\ref{sec:options}. +% +% Following the conventions of \pkg{amsmath} for alignment environments, the +% non-starred version produces a proof tree at the current position in the +% text flow (it can be used in math mode or text mode) while the starred +% version typesets the proof on a line of its own, like a displayed formula. +% \end{function} +% +% \begin{example} +% \[ +% \begin{prooftree} +% \infer0{ \vdash A } +% \hypo{ \vdash B } \infer1{ \vdash B, C } +% \infer2{ \vdash A\wedge B, C } +% \end{prooftree} +% \quad \rightsquigarrow \quad +% \begin{prooftree} +% \infer0{ \vdash A } \hypo{ \vdash B } +% \infer2{ \vdash A\wedge B } +% \infer1{ \vdash A\wedge B, C } +% \end{prooftree} +% \] +% \end{example} +% +% \section{Statements} +% \label{sec:statements} +% +% Statements describe proofs in postfix notation: when typesetting a proof tree +% whose last rule has, say, two premisses, you will first write statements for +% the subtree of the first premiss, then statements for the subtree of the +% second premiss, then a statement like \cs{infer2}\{\meta{conclusion}\} to +% build an inference with these two subtrees as premisses and the given text as +% conclusion. +% +% Hence statements operate on a stack of proof trees. +% At the beginning of a \env{prooftree} environment, the stack is empty. +% At the end, it must contain exactly one tree, which is the one that will be +% printed. +% +% Note that the commands defined in this section only exist right inside +% \env{prooftree} environments. +% If you have a macro with the same name as one of the statements, for instance +% \cs{hypo}, then this macro will keep its meaning outside \env{prooftree} +% environments as well as inside the arguments of a statement. +% If you really need to access the statements in another context, you can can +% always call them by prefixing their names with \texttt{ebproof}, for instance as +% \cs{ebproofhypo}. +% +% \subsection{Basic statements} +% +% The basic statements for building proofs are the following, where +% \meta{options} stands for arbitrary options as described in +% section~\ref{sec:options}. +% +% \begin{function}{\hypo} +% \begin{syntax} +% \cs{hypo}\oarg{options}\marg{text} +% \end{syntax} +% The statement \cs{hypo} pushes a new proof tree consisting only in one +% conclusion line, with no premiss and no line above, in other words a tree +% with only a leaf (\cs{hypo} stands for \emph{hypothesis}). +% \end{function} +% +% \begin{function}{\infer} +% \begin{syntax} +% \cs{infer}\oarg{options}\meta{arity}\oarg{label}\marg{text} +% \end{syntax} +% The statement \cs{infer} builds an inference step by taking some proof +% trees from the top of the stack, assembling them with a rule joining their +% conclusions and putting a new conclusion below. +% The \meta{arity} is the number of sub-proofs, it may be any number +% including 0 (in this case there will be a line above the conclusion but no +% sub-proof). +% If \meta{label} is present, it is used as the label on the right of the +% inference line; it is equivalent to using the \cmd{right label} option. +% \end{function} +% +% \medskip +% +% The \meta{text} in these statements is the contents of the conclusion at the +% root of the tree that the statements create. +% It is typeset in math mode by default but any kind of formatting can be used +% instead, using the \cmd{template} option. +% The \meta{label} text is formatted in horizontal text mode by default. +% +% Each proof tree has a vertical axis, used for alignment of successive steps. +% The position of the axis is deduced from the text of the conclusion at the +% root of the tree: if \meta{text} contains the alignment character \verb|&| +% then the axis is set at that position, otherwise the axis is set at the center +% of the conclusion text. +% The \cs{infer} statement makes sure that the axis of the premiss is at the +% same position as the axis of the conclusion. +% If there are several premisses, it places the axis at the center between the +% left of the leftmost conclusion and the right of the rightmost conclusion: +% +% \begin{example} +% \begin{prooftree} +% \hypo{ &\vdash A, B, C } +% \infer1{ A &\vdash B, C } +% \infer1{ A, B &\vdash C } +% \hypo{ D &\vdash E } +% \infer2{ A, B, D &\vdash C, E } +% \infer1{ A, B &\vdash C, D, E } +% \infer1{ A &\vdash B, C, D, E } +% \end{prooftree} +% \end{example} +% +% \begin{function}{\ellipsis} +% \begin{syntax} +% \cs{ellipsis}\marg{label}\marg{text} +% \end{syntax} +% The statement \cs{ellipsis} typesets vertical dots, with a label on the right, +% and a new conclusion. No inference lines are inserted. +% \end{function} +% +% \begin{example} +% \begin{prooftree} +% \hypo{ \Gamma &\vdash A } +% \ellipsis{foo}{ \Gamma &\vdash A, B } +% \end{prooftree} +% \end{example} +% +% +% \subsection{Modifying proof trees} +% +% The following additional statements may be used to affect the format of the +% last proof tree on the stack. +% +% \begin{function}{\rewrite} +% \begin{syntax} +% \cs{rewrite}\marg{code} +% \end{syntax} +% The statement \cs{rewrite} is used to modify the proof of the stack while +% preserving its size and alignment. +% The \meta{code} is typeset in horizontal mode, with the following control +% sequences defined: +% \begin{itemize} +% \item \cs{treebox} is a box register that contains the original material, +% \item \cs{treemark}\marg{name} expands as the position of a given mark with +% respect to the left of the box. +% \end{itemize} +% \end{function} +% +% A simple use of this statement is to change the color of a proof tree: +% \begin{example} +% \begin{prooftree} +% \hypo{ \Gamma, A &\vdash B } +% \infer1[abs]{ \Gamma &\vdash A\to B } +% \rewrite{\color{red}\box\treebox} +% \hypo{ \Gamma \vdash A } +% \infer2[app]{ \Gamma \vdash B } +% \end{prooftree} +% \end{example} +% Note the absence of spaces inside the call to \cs{rewrite}, because spaces +% would affect the position of the tree box. +% Note also that explicit use of \cs{treebox} is required to actually draw the +% subtree. +% Not using it will effectively not render the subtree, while still reserving +% its space in the enclosing tree: +% \begin{example} +% \begin{prooftree} +% \hypo{ \Gamma, A &\vdash B } +% \infer1[abs]{ \Gamma &\vdash A\to B } +% \rewrite{} +% \hypo{ \Gamma \vdash A } +% \infer2[app]{ \Gamma \vdash B } +% \end{prooftree} +% \end{example} +% This kind of manipulation is useful for instance in conjunction with the +% \pkg{beamer} package to allow revealing subtrees of a proof tree +% progressively in successive slides of a given frame. +% +% \begin{function}{\delims} +% \begin{syntax} +% \cs{delims}\marg{left}\marg{right} +% \end{syntax} +% The statement \cs{delims} puts left and right delimiters around the whole +% sub-proof, without changing the alignment (the spacing is affected by the +% delimiters, however). +% The \meta{left} text must contain an opening occurrence of \cs{left} and +% the \meta{right} text must contain a matching occurrence of \cs{right}. +% For instance, \verb|\delims{\left(}{\right)}| will put the sub-proof +% between parentheses. +% \end{function} +% +% \begin{example} +% \begin{prooftree} +% \hypo{ A_1 \vee \cdots \vee A_n } +% \hypo{ [A_i] } +% \ellipsis{}{ B } +% \delims{ \left( }{ \right)_{1\leq i\leq n} } +% \infer2{ B } +% \end{prooftree} +% \end{example} +% +% \begin{function}{\overlay} +% \begin{syntax} +% \cs{overlay} +% \end{syntax} +% The statement \cs{overlay} combines the last two proofs on the stack into +% a single one, so that their conclusions are placed at the same point. +% \end{function} +% +% \begin{example} +% \begin{prooftree} +% \hypo{Z} +% \hypo{A} \hypo{B} \infer2{C} \hypo{D} \infer2{D} +% \rewrite{\color{blue}\box\treebox} +% \hypo{E} \hypo{F} \hypo{G} \infer2{H} \infer2{I} +% \rewrite{\color{red}\box\treebox} +% \overlay \hypo{J} \infer3{K} +% \end{prooftree} +% \end{example} +% +% The primary use of this feature is for building animated presentations where +% a subtree in a proof has to be modified without affecting the general +% alignment of the surrounding proof. For instance, the example above could be +% used in Beamer to build successive slides in a given frame with two +% different subtrees: +% +% \begin{verbatim} +% \begin{prooftree} +% \hypo{Z} +% \hypo{A} \hypo{B} \infer2{C} \hypo{D} \infer2{D} +% \only<2>{\rewrite{}} % erases this version on slide 2 +% \hypo{E} \hypo{F} \hypo{G} \infer2{H} \infer2{I} +% \only<1>{\rewrite{}} % erases this version on slide 1 +% \overlay \hypo{J} \infer3{K} +% \end{prooftree} +% \end{verbatim} +% +% \section{Options} +% \label{sec:options} +% +% The formatting of trees, conclusion texts and inference rules is affected by +% options, specified using the \LaTeX3 key-value system. +% All options are in the \texttt{ebproof} module in the key tree. +% They can be set locally for a proof tree or for a single statement using +% optional arguments in the associated commands. +% +% \begin{function}{\ebproofset,\set} +% \begin{syntax} +% \cs{ebproofset}\marg{options} +% \end{syntax} +% The statement \cs{ebproofset} is used to set some options. When used +% inside a \env{prooftree} environment, it can written \cs{set}. +% The options will apply in the current scope; using this in preamble will +% effectively set options globally. +% Specific options may also be specified for each proof tree and for each +% statement in a proof tree, using optional arguments. +% \end{function} +% +% \subsection{General shape} +% +% The options in this section only make sense at the global level and at the +% proof level. +% Changing the proof style inside a \env{proof} environment has undefined +% behaviour. +% +% \begin{variable}{proof style} +% The option \cmd{proof style} sets the general shape for representing proofs. +% The following styles are provided: +% \begin{description} +% \item[upwards] +% This is the default style. +% Proof trees grow upwards, with conclusions below and premisses above. +% \item[downwards] +% Proof trees grow downwards, with conclusions above and premisses below. +% \fvset{gobble=6} +% \begin{example} +% \begin{prooftree}[proof style=downwards] +% \hypo{ \Gamma, A &\vdash B } +% \infer1[abs]{ \Gamma &\vdash A\to B } +% \hypo{ \Gamma \vdash A } +% \infer2[app]{ \Gamma \vdash B } +% \end{prooftree} +% \end{example} +% \end{description} +% \end{variable} +% +% In the optional argument of \env{prooftree} environments, proof styles can +% be specified directly, without prefixing the name by ``\texttt{proof style=}''. +% For instance, the first line of the example above could be written +% \verb|\begin{prooftree}| equivalently. +% +% \begin{variable}{center} +% The option \cmd{center} toggles vertical centering of typeset proofs. +% If set to \texttt{true}, the tree produced by the \env{prooftree} +% environment will be vertically centered around the text line. +% If set to \texttt{false}, the base line of the tree will be the base line +% of the conclusion. +% The default value is \texttt{true}. +% \end{variable} +% +% \begin{example} +% \begin{prooftree}[center=false] +% \infer0{ A \vdash A } +% \end{prooftree} +% \qquad +% \begin{prooftree}[center=false] +% \hypo{ \Gamma, A \vdash B } +% \infer1{ \Gamma \vdash A \to B } +% \end{prooftree} +% \end{example} +% +% \subsection{Spacing} +% +% \begin{variable}{separation} +% Horizontal separation between sub-proofs in an inference is defined by the +% option \cmd{separation}. +% The default value is \texttt{1.5em}. +% \end{variable} +% +% \begin{example} +% \begin{prooftree}[separation=0.5em] +% \hypo{ A } \hypo{ B } \infer2{ C } +% \hypo{ D } \hypo{ E } \hypo{ F } \infer3{ G } +% \hypo{ H } \infer[separation=3em]3{ K } +% \end{prooftree} +% \end{example} +% +% \begin{variable}{rule margin} +% The spacing above and below inference lines is defined by the option +% \cmd{rule margin}. +% The default value is \texttt{0.7ex}. +% \end{variable} +% +% \begin{example} +% \begin{prooftree}[rule margin=2ex] +% \hypo{ \Gamma, A &\vdash B } +% \infer1[abs]{ \Gamma &\vdash A\to B } +% \hypo{ \Gamma \vdash A } +% \infer2[app]{ \Gamma \vdash B } +% \end{prooftree} +% \end{example} +% +% \subsection{Shape of inference lines} +% +% \begin{variable}{rule style} +% The shape of inference lines is set by the option \cmd{rule style}. +% The following values are provided: +% \begin{center} +% \begin{tabular}{@{}l@{\qquad}l@{}} +% \toprule +% \cmd{simple} & a simple line (this is the default style) \\ +% \cmd{no rule} & no rule, only a single space of length \texttt{rule margin} \\ +% \cmd{double} & a double line \\ +% \cmd{dashed} & a single dashed line \\ +% \bottomrule +% \end{tabular} +% \end{center} +% \end{variable} +% +% The precise rendering is influenced by parameters specified below. +% Arbitrary new shapes can defined using the \cs{ebproofnewrulestyle} command +% described in section~\ref{sec:styles}, using \texttt{rule code} option +% described below. +% +% In the optional argument of the \cs{infer} statement, rule styles can be +% specified directly, without prefixing the style name by ``\texttt{rule style=}''. +% For instance, \verb|\infer[dashed]| is equivalent to +% \verb|\infer[rule style=dashed]|. +% +% \begin{example} +% \begin{prooftree} +% \hypo{ \Gamma &\vdash A \to B } +% \infer[no rule]1{ \Gamma &\vdash {!A} \multimap B } +% \hypo{ \Delta &\vdash A } +% \infer[rule thickness=2pt]1{ \Delta &\vdash {!A} } +% \infer0{ B \vdash B } +% \infer[dashed]2{ \Delta, {!A}\multimap B \vdash B } +% \infer2{ \Gamma, \Delta &\vdash B } +% \infer[double]1{ \Gamma \cup \Delta &\vdash B } +% \end{prooftree} +% \end{example} +% +% \begin{variable}{rule thickness,rule separation} +% The thickness of inference lines is defined by option \cmd{rule +% thickness}, it is \texttt{0.4pt} by default. +% The distance between the two lines in the \texttt{double} rule style is +% defined by the \cmd{rule separation} option. +% It is \texttt{2pt} by default. +% \end{variable} +% \begin{variable}{rule dash length,rule dash space} +% For dashed rules, the length of dashes is defined by the option +% \cmd{rule dash length} and the space between dashes is defined by the +% option \cmd{rule dash space}. +% The default values are \texttt{0.2em} and \texttt{0.3em} respectively. +% \end{variable} +% +% \begin{variable}{rule code} +% Arbitrary rule shapes can be optained using the \cmd{rule code} option. +% The argument is code is used to render the rule, it is executed in +% vertical mode in a \cs{vbox} whose \cs{hsize} is set to the width of the +% rule. +% Margins above and below are inserted automatically (they can be removed by +% setting \texttt{rule margin} to \texttt{0pt}). +% \end{variable} +% +% \begin{example} +% \begin{prooftree}[rule code={\hbox{\tikz +% \draw[decorate,decoration={snake,amplitude=.3ex}] +% (0,0) -- (\hsize,0);}}] +% \hypo{ \Gamma &\vdash A } +% \infer1{ \Gamma &\vdash A, \ldots, A } +% \hypo{ \Delta, A, \ldots, A \vdash \Theta } +% \infer2{ \Gamma, \Delta \vdash \Theta } +% \end{prooftree} +% \end{example} +% Note that this example requires the \pkg{tikz} package, with the +% \pkg{decorations.pathmorphing} library for the \texttt{snake} decoration. +% +% \subsection{Format of conclusions and labels} +% +% \begin{variable}{template,left template,right template} +% The format of text in inferences is defined by templates. +% The option \cmd{template} is used for text with no alignment mark, the +% options \cmd{left template} and \cmd{right template} are used for the left +% and right side of the alignment mark when it is present. +% The value of these options is arbitrary \TeX\ code, composed in horizontal mode. +% The macro \cs{inserttext} is used to insert the actual text passed to the +% \cs{hypo} and \cs{infer} statements. +% The default value for \cmd{template} is simply \verb|$\inserttext$|, so +% that conclusions are set in math mode. +% The default values for \cmd{left template} and \cmd{right template} are +% similar, with spacing assuming that a relation symbol is put near the +% alignment mark, so that \verb|\infer1{A &\vdash B}| is spaced correctly. +% \end{variable} +% +% \begin{example} +% \begin{prooftree}[template=(\textbf\inserttext)] +% \hypo{ foo } +% \hypo{ bar } +% \infer1{ baz } +% \infer2{ quux } +% \end{prooftree} +% \end{example} +% +% \begin{variable}{left label,right label} +% The text to use as the labels of the rules, on the left and on the right +% of the inference line, is defined by the options \cmd{left label} and +% \cmd{right label}. +% Using the second optional argument in \cs{infer} is equivalent to setting +% the \env{right label} option with the value of that argument. +% \end{variable} +% +% \begin{example} +% \begin{prooftree} +% \hypo{ \Gamma, A &\vdash B } +% \infer[left label=$\lambda$]1[abs] +% { \Gamma &\vdash A\to B } +% \hypo{ \Gamma \vdash A } +% \infer[left label=@]2[app]{ \Gamma \vdash B } +% \end{prooftree} +% \end{example} +% +% \begin{variable}{left label template,right label template} +% Similarly to conclusions, labels are formatted according to templates. +% The code is arbitrary \TeX\ code, composed in horizontal mode, where the +% macro \cs{inserttext} can be used to insert the actual label text. +% The default values are simply \cs{inserttext} so that labels are set in +% plain text mode. +% \end{variable} +% \begin{variable}{label separation} +% The spacing between an inference line and its labels is defined by the +% option \cmd{label separation}, the default value is \texttt{0.5em}. +% The height of the horizontal axis used for aligning the labels with the +% rules is defined by the option \cmd{label axis}, the default value is +% \texttt{0.5ex}. +% \end{variable} +% +% +% \subsection{Style macros} +% \label{sec:styles} +% +% The following commands allow for the definition of custom styles using the +% basic style options, in a way similar to PGF's ``styles'' and \LaTeX3's +% ``meta-keys''. +% This allows setting a bunch of options with the same values in many proofs +% using a single definition. +% +% \begin{function}{\ebproofnewstyle} +% \begin{syntax} +% \cs{ebproofnewstyle}\marg{name}\marg{options} +% \end{syntax} +% The statement \cs{ebproofnewstyle} defines a new style option with some +% \meta{name} that sets a given set of \meta{options}. +% \end{function} +% For instance, the following code defines a new option \cmd{small} that sets +% various parameters so that proofs are rendered smaller. +% \begin{example} +% \ebproofnewstyle{small}{ +% separation = 1em, rule margin = .5ex, +% template = \footnotesize$\inserttext$ } +% \begin{prooftree}[small] +% \hypo{ \Gamma, A \vdash B } +% \infer1{ \Gamma \vdash A\to B } +% \hypo{ \Gamma \vdash A } \infer2{ \Gamma \vdash B } +% \end{prooftree} +% \end{example} +% +% \begin{function}{\ebproofnewrulestyle} +% \begin{syntax} +% \cs{ebproofnewrulestyle}\marg{name}\marg{options} +% \end{syntax} +% The statement \cs{ebproofnewrulestyle} does the same for rule styles. +% The \meta{options} part includes options used to set how to draw rules in +% the new style. +% \end{function} +% +% The option \cmd{rule code} is useful in this command as it allows to +% define arbitrary rule styles. +% For instance, the squiggly rule example above could be turned into a new +% rule style \texttt{zigzag} with the following code: +% \begin{example} +% \ebproofnewrulestyle{zigzag}{ +% rule code = {\hbox{\tikz +% \draw[decorate,decoration={snake,amplitude=.3ex}] +% (0,0) -- (\hsize,0);}}} +% \begin{prooftree} +% \hypo{ \Gamma &\vdash A } +% \infer1{ \Gamma &\vdash A, \ldots, A } +% \hypo{ \Delta, A, \ldots, A \vdash \Theta } +% \infer[zigzag]2{ \Gamma, \Delta \vdash \Theta } +% \end{prooftree} +% \end{example} +% +% +% \section{License} +% +% 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 +% \begin{center} +% \url{http://www.latex-project.org/lppl.txt} +% \end{center} +% 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 Emmanuel Beffara. +% +% This work consists of the files \texttt{ebproof.sty} and \texttt{ebproof.tex}. +% +% \section{History} +% +% This section lists the principal evolutions of the package, in reverse +% chronological order. +% \begin{description} +% \item[Version 2.1 (2020-08-19)] +% Mostly a bugfix release. +% \begin{itemize} +% \item Makes the \env{prooftree} environment robust to use in tabular +% contexts. +% \item Adds the \cs{overlay} statement. +% \item Fixes a compatibility issue with \LaTeX\ release 2020-10-01. +% \end{itemize} +% \item[Version 2.0 (2017-05-17)] +% A complete rewrite of the code using the \LaTeX3 programming environment. +% The incompatible changes from the user's point of view are the following: +% \begin{itemize} +% \item Proof statements are now writtten in lowercase ({i.e.} \cs{Infer} is +% now written \cs{infer} etc.) but the syntax is otherwise unchanged. +% The old uppercase commands still work but produce a deprecation warning, +% they will be removed in a future version. +% \item New styles are now defined using \cs{ebproofnewstyle} and +% \cs{ebproofnewrulestyle}. The previous method using PGF styles does not +% work anymore (because PGF is not used anymore). +% \end{itemize} +% The new commands and options are the following: +% \begin{itemize} +% \item The statement \cs{rewrite} generalizes \cs{Alter}, +% \item The option \cmd{label axis} controls vertical alignment of labels. +% \end{itemize} +% \item[Version 1.1 (2015-03-13)] +% A bugfix release. +% In \cmd{template} options, one now uses \cs{inserttext} instead of \verb|#1| +% for the text arguments, which improves robustness. +% \item[Version 1.0 (2015-02-04)] +% The first public release. +% \end{description} +% +% \end{documentation} +% +% \clearpage \appendix +% +% \begin{implementation} +% +% \section{Implementation} +% +% \begin{macrocode} +%<*package> +\NeedsTeXFormat{LaTeX2e} +\RequirePackage{expl3} +\RequirePackage{xparse} +\ProvidesExplPackage{ebproof}{2020/08/19}{2.1}{EB's proof trees} +%<@@=ebproof> +% \end{macrocode} +% +% \subsection{Parameters} +% +% We first declare all options. For the meaning of options, see +% section~\ref{sec:options}. +% +% \begin{macrocode} +\keys_define:nn { ebproof } { +center .bool_set:N = \l_@@_center_bool, +proof~style .choice: , +proof~style / upwards .code:n = \bool_set_false:N \l_@@_updown_bool, +proof~style / downwards .code:n = \bool_set_true:N \l_@@_updown_bool, +separation .dim_set:N = \l_@@_separation_dim, +rule~margin .dim_set:N = \l_@@_rule_margin_dim, +rule~thickness .dim_set:N = \l_@@_rule_thickness_dim, +rule~separation .dim_set:N = \l_@@_rule_separation_dim, +rule~dash~length .dim_set:N = \l_@@_rule_dash_length_dim, +rule~dash~space .dim_set:N = \l_@@_rule_dash_space_dim, +rule~code .tl_set:N = \l_@@_rule_code_tl, +rule~style .choice:, +template .tl_set:N = \l_@@_template_tl, +left~template .tl_set:N = \l_@@_left_template_tl, +right~template .tl_set:N = \l_@@_right_template_tl, +left~label .tl_set:N = \l_@@_left_label_tl, +right~label .tl_set:N = \l_@@_right_label_tl, +left~label~template .tl_set:N = \l_@@_left_label_template_tl, +right~label~template .tl_set:N = \l_@@_right_label_template_tl, +label~separation .dim_set:N = \l_@@_label_separation_dim, +label~axis .dim_set:N = \l_@@_label_axis_dim, +} +% \end{macrocode} +% +% \begin{macro}{\ebproofnewrulestyle} +% We then define the document-level macro \cs{ebproofnewrulestyle} and use +% it to define the default styles. This simply consists in defining a +% meta-key. +% \begin{macrocode} +\NewDocumentCommand \ebproofnewrulestyle { mm } { + \keys_define:nn { ebproof } { + rule~style / #1 .meta:nn = { ebproof } { #2 } + } +} +% \end{macrocode} +% \end{macro} +% +% The styles |simple|, |no rule| and |double| are defined in a straightforward +% way. +% +% \begin{macrocode} +\ebproofnewrulestyle { simple } { + rule~code = { \tex_hrule:D height \l_@@_rule_thickness_dim } +} +\ebproofnewrulestyle { no~rule } { + rule~code = +} +\ebproofnewrulestyle { double } { + rule~code = { + \tex_hrule:D height \l_@@_rule_thickness_dim + \skip_vertical:N \l_@@_rule_separation_dim + \tex_hrule:D height \l_@@_rule_thickness_dim + } +} +% \end{macrocode} +% +% The |dashed| style uses leaders and filling for repeating a single dash. We +% use \TeX\ primitives that have no \LaTeX3 counterpart for this. +% +% \begin{macrocode} +\ebproofnewrulestyle { dashed } { + rule~code = { + \hbox_to_wd:nn { \tex_hsize:D } { + \dim_set:Nn \l_tmpa_dim { \l_@@_rule_dash_space_dim / 2 } + \skip_horizontal:n { -\l_tmpa_dim } + \tex_cleaders:D \hbox:n { + \skip_horizontal:N \l_tmpa_dim + \tex_vrule:D + height \l_@@_rule_thickness_dim + width \l_@@_rule_dash_length_dim + \skip_horizontal:N \l_tmpa_dim + } \tex_hfill:D + \skip_horizontal:n { -\l_tmpa_dim } + } + } +} +% \end{macrocode} +% +% Now we can define the default values, including the default rule style. +% +% \begin{macrocode} +\keys_set:nn { ebproof } { + center = true, + proof~style = upwards, + separation = 1.5em, + rule~margin = .7ex, + rule~thickness = .4pt, + rule~separation = 2pt, + rule~dash~length = .2em, + rule~dash~space = .3em, + rule~style = simple, + template = $\inserttext$, + left~template = $\inserttext\mathrel{}$, + right~template = $\mathrel{}\inserttext$, + left~label = , + right~label = , + left~label~template = \inserttext, + right~label~template = \inserttext, + label~separation = 0.5em, + label~axis = 0.5ex +} +% \end{macrocode} +% +% \begin{macro}{\ebproofnewstyle} +% Defining a style simply means defining a meta-key. +% \begin{macrocode} +\NewDocumentCommand \ebproofnewstyle { mm } { + \keys_define:nn { ebproof } { #1 .meta:n = { #2 } } +} +% \end{macrocode} +% \end{macro} +% +% +% \subsection{Proof boxes} +% +% \TeX\ does not actually provide data structures, so we have to encode things. +% We provide an allocator for ``registers'' holding boxes with attributes. Such +% a register consists in a box register and a property list for marks, which +% maps mark names to values as explicit dimensions with units. +% +% \begin{macro}{\@@_new:N} +% Using only public interfaces forces a convoluted approach to allocation: +% we use a global counter \cs{g_ebproof_register_int} to number registers, +% then each allocation creates registers named \cs{g_ebproof_K_N} where K is +% the kind of component (box or marks) and N is the identifier of the +% register. The proof box register itself only contains the identifier used +% for indirection. +% \begin{macrocode} +\int_new:N \g_@@_register_int +\cs_new:Nn \@@_box:N { g__ebproof_box_ \tl_use:N #1 } +\cs_new:Nn \@@_marks:N { g__ebproof_marks_ \tl_use:N #1 } +\cs_new:Nn \@@_new:N { + \tl_new:N #1 + \int_gincr:N \g_@@_register_int + \tl_gset:Nx #1 { \int_to_arabic:n { \g_@@_register_int } } + \box_new:c { \@@_box:N #1 } + \prop_new:c { \@@_marks:N #1 } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_clear:N} +% The box is cleared by setting it to an empty hbox. +% Using \cs{box_clear:N} instead would not work because trying to push this +% box on the stack would not actually append any box. +% \begin{macrocode} +\cs_new:Nn \@@_clear:N { + \hbox_set:cn { \@@_box:N #1 } {} + \prop_clear:c { \@@_marks:N #1 } + \@@_set_mark:Nnn #1 { left } { 0pt } + \@@_set_mark:Nnn #1 { right } { 0pt } + \@@_set_mark:Nnn #1 { axis } { 0pt } +} +% \end{macrocode} +% \end{macro} +% +% \subsubsection{Mark operations} +% +% \begin{macro}{\@@_set_mark:Nnn} +% Setting the value of a mark uses a temporary register to evaluate the +% dimension expression because values are stored textually in a property +% list. +% \begin{macrocode} +\dim_new:N \l_@@_transit_dim +\cs_new:Nn \@@_set_mark:Nnn { + \dim_set:Nn \l_@@_transit_dim { #3 } + \prop_put:cnV { \@@_marks:N #1 } { #2 } + \l_@@_transit_dim +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_mark:Nn} +% Getting the value of a mark simply consists in getting an item in a +% property list. +% \begin{macrocode} +\cs_new:Nn \@@_mark:Nn { + \prop_item:cn { \@@_marks:N #1 } { #2 } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_shift_x:Nn} +% This function shifts the marks by a specified amount, without modifying +% the box. +% \begin{macrocode} +\cs_new:Nn \@@_shift_x:Nn { + \prop_map_inline:cn { \@@_marks:N #1 } { + \@@_set_mark:Nnn #1 { ##1 } { ##2 + #2 } + } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_enlarge_conclusion:NN} +% This function moves the left and right marks of the first tree so that +% they are at least as far from the axis as they are in the second tree. +% For instance we get the following: +% \begin{center} +% \begin{tikzpicture}[y=-3ex] +% \node (L1) at (1,0) {L}; \node (A1) at (2,0) {A}; \node (R1) at (4,0) {R}; +% \node (L2) at (0,1) {L}; \node (A2) at (2,1) {A}; \node (R2) at (3,1) {R}; +% \node (L3) at (0,2) {L}; \node (A3) at (2,2) {A}; \node (R3) at (4,2) {R}; +% \draw (L1) -- (A1) -- (R1); +% \draw (L2) -- (A2) -- (R2); +% \draw (L3) -- (A3) -- (R3); +% \node[anchor=west] at (5,0) {box 1 before}; +% \node[anchor=west] at (5,1) {box 2 before}; +% \node[anchor=west] at (5,2) {box 1 after}; +% \end{tikzpicture} +% \end{center} +% The contents of the trees are unchanged. +% \begin{macrocode} +\cs_new:Nn \@@_enlarge_conclusion:NN { + \dim_set:Nn \l_tmpa_dim { \@@_mark:Nn #1 {axis} + + \@@_mark:Nn #2 {left} - \@@_mark:Nn #2 {axis} } + \dim_compare:nNnT { \l_tmpa_dim } < { \@@_mark:Nn #1 {left} } { + \@@_set_mark:Nnn #1 {left} { \l_tmpa_dim } } + \dim_set:Nn \l_tmpa_dim { \@@_mark:Nn #1 {axis} + + \@@_mark:Nn #2 {right} - \@@_mark:Nn #2 {axis} } + \dim_compare:nNnT { \l_tmpa_dim } > { \@@_mark:Nn #1 {right} } { + \@@_set_mark:Nnn #1 {right} { \l_tmpa_dim } } +} +% \end{macrocode} +% \end{macro} +% +% \subsubsection{Building blocks} +% +% \begin{macro}{\@@_make_simple:Nn} +% Make a tree with explicit material in horizontal mode. Set the left and +% right marks to extremal positions and set the axis in the middle. +% \begin{macrocode} +\cs_new:Nn \@@_make_simple:Nn { + \hbox_set:cn { \@@_box:N #1 } { #2 } + \@@_set_mark:Nnn #1 { left } { 0pt } + \@@_set_mark:Nnn #1 { axis } { \box_wd:c { \@@_box:N #1 } / 2 } + \@@_set_mark:Nnn #1 { right } { \box_wd:c { \@@_box:N #1 } } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_make_split:Nnn} +% Make a tree with explicit material in horizontal mode, split in two parts. +% Set the left and right marks to extremal positions and set the axis +% between the two parts. +% \begin{macrocode} +\cs_new:Nn \@@_make_split:Nnn { + \@@_set_mark:Nnn #1 { left } { 0pt } + \hbox_set:cn { \@@_box:N #1 } { #2 } + \@@_set_mark:Nnn #1 { axis } { \box_wd:c { \@@_box:N #1 } } + \hbox_set:cn { \@@_box:N #1 } { \hbox_unpack:c { \@@_box:N #1 } #3 } + \@@_set_mark:Nnn #1 { right } { \box_wd:c { \@@_box:N #1 } } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_make_vertical:Nnnn} +% Make a tree with explicit material in vertical mode, using an explicit +% width and axis. +% \begin{macrocode} +\cs_new:Nn \@@_make_vertical:Nnnn { + \@@_set_mark:Nnn #1 { left } { 0pt } + \@@_set_mark:Nnn #1 { axis } { #2 } + \@@_set_mark:Nnn #1 { right } { #3 } + \vbox_set:cn { \@@_box:N #1 } { + \dim_set:Nn \tex_hsize:D { \@@_mark:Nn #1 {right} } + #4 + } + \box_set_wd:cn { \@@_box:N #1 } { \@@_mark:Nn #1 {right} } +} +% \end{macrocode} +% \end{macro} +% +% \subsubsection{Assembling boxes} +% +% \begin{macro}{\@@_extend:Nnnnn} +% Extend a tree box. The marks are shifted so that alignment is preserved. +% The arguments are dimensions for the left, top, right and bottom sides +% respectively. +% \begin{macrocode} +\cs_new:Nn \@@_extend:Nnnnn { + \dim_compare:nNnF { #2 } = { 0pt } { + \hbox_set:cn { \@@_box:N #1 } { + \skip_horizontal:n { #2 } + \box_use:c { \@@_box:N #1 } + } + \@@_shift_x:Nn #1 { #2 } + } + \box_set_ht:Nn #1 { \box_ht:c { \@@_box:N #1 } + #3 } + \box_set_wd:Nn #1 { \box_wd:c { \@@_box:N #1 } + #4 } + \box_set_dp:Nn #1 { \box_dp:c { \@@_box:N #1 } + #5 } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_append_right:NnN} +% Append the contents of the second tree to the first one on the right, with +% matching baselines. The marks of both trees are preserved. The middle +% argument specifies the space to insert between boxes. +% \begin{macrocode} +\cs_new:Nn \@@_append_right:NnN { + \hbox_set:cn { \@@_box:N #1 } { + \box_use:c { \@@_box:N #1 } + \dim_compare:nNnF { #2 } = { 0pt } { \skip_horizontal:n { #2 } } + \box_use:c { \@@_box:N #3 } + } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_append_left:NnN} +% Append the contents of the second tree to the first one on the left, with +% matching baselines. The marks of the first tree are shifted accordingly. +% The middle argument specifies the space to insert between boxes. +% \begin{macrocode} +\cs_new:Nn \@@_append_left:NnN { + \@@_shift_x:Nn #1 { \box_wd:c { \@@_box:N #3 } + #2 } + \hbox_set:cn { \@@_box:N #1 } { + \box_use:c { \@@_box:N #3 } + \dim_compare:nNnF { #2 } = { 0pt } { \skip_horizontal:n { #2 } } + \box_use:c { \@@_box:N #1 } + } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_align:NN} +% Shift one of two trees to the right so that their axes match. The marks of +% the one that is shifted are updated accordingly. +% \begin{macrocode} +\cs_new:Nn \@@_align:NN { + \dim_set:Nn \l_tmpa_dim + { \@@_mark:Nn #2 {axis} - \@@_mark:Nn #1 {axis} } + \dim_compare:nNnTF \l_tmpa_dim < { 0pt } { + \@@_extend:Nnnnn #2 { -\l_tmpa_dim } { 0pt } { 0pt } { 0pt } + } { + \@@_extend:Nnnnn #1 { \l_tmpa_dim } { 0pt } { 0pt } { 0pt } + } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_append_above:NN} +% Append the contents of the second tree above the first one, with matching +% axes. The marks of the first tree are preserved. +% \begin{macrocode} +\cs_new:Nn \@@_append_above:NN { + \@@_align:NN #1 #2 + \vbox_set:cn { \@@_box:N #1 } { + \box_use:c { \@@_box:N #2 } + \tex_prevdepth:D -1000pt + \box_use:c { \@@_box:N #1 } + } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_append_below:NN} +% Append the contents of the second tree below the first one, with matching +% axes. The marks of the first tree are preserved. +% \begin{macrocode} +\cs_new:Nn \@@_append_below:NN { + \@@_align:NN #1 #2 + \vbox_set_top:Nn #1 { + \box_use:c { \@@_box:N #1 } + \tex_prevdepth:D -1000pt + \box_use:c { \@@_box:N #2 } + } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_overlay:NN} +% Append the second tree as an overlay over the first one, so that the +% baselines and axes match. The bounding box of the result adjusts to +% contain both trees. +% \begin{macrocode} +\cs_new:Nn \@@_overlay:NN { + \@@_align:NN #1 #2 + \hbox_set:cn { \@@_box:N #1 } { + \hbox_overlap_right:n { \box_use:c { \@@_box:N #1 } } + \box_use:c { \@@_box:N #2 } + \dim_compare:nNnT + { \box_wd:c { \@@_box:N #2 } } < { \box_wd:c { \@@_box:N #1 } } + { \skip_horizontal:n + { \box_wd:c { \@@_box:N #1 } - \box_wd:c { \@@_box:N #2 } } } + } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_vcenter:N} +% Shift the material in a tree vertically so that the height and depth are +% equal (like \TeX's \cs{vcenter} but around the baseline). +% \begin{macrocode} +\cs_new:Nn \@@_vcenter:N { + \dim_set:Nn \l_tmpa_dim + { ( \box_ht:c { \@@_box:N #1 } - \box_dp:c { \@@_box:N #1 } ) / 2 } + \box_set_eq:Nc \l_tmpa_box { \@@_box:N #1 } + \hbox_set:cn { \@@_box:N #1 } + { \box_move_down:nn { \l_tmpa_dim } { \box_use:N \l_tmpa_box } } +} +% \end{macrocode} +% \end{macro} +% +% \subsection{Making inferences} +% +% The following commands use the parameters defined at the beginning of the +% package for actually building proof trees using the commands defined above. +% +% \begin{macro}{\@@_append_vertical:NN} +% Append the contents of the second tree above or below the first one, +% depending on current settings. Axes are aligned and the marks of the first +% tree are preserved. +% \begin{macrocode} +\cs_new:Nn \@@_append_vertical:NN { + \bool_if:NTF \l_@@_updown_bool + { \@@_append_below:NN #1 #2 } + { \@@_append_above:NN #1 #2 } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_make_rule_for:NNN} +% Make a box containing an inference rule with labels, using the current +% settings. The width and axis position are taken as those of the conclusion +% of another tree box. The third argument is used as a temporary register +% for building labels. +% \begin{macrocode} +\cs_new:Nn \@@_make_rule_for:NNN { +% \end{macrocode} +% Build the rule. +% \begin{macrocode} + \@@_make_vertical:Nnnn #1 + { \@@_mark:Nn #2 {axis} - \@@_mark:Nn #2 {left} } + { \@@_mark:Nn #2 {right} - \@@_mark:Nn #2 {left} } + { + \skip_vertical:N \l_@@_rule_margin_dim + \tl_if_empty:NF { \l_@@_rule_code_tl } { + \tl_use:N \l_@@_rule_code_tl + \skip_vertical:N \l_@@_rule_margin_dim + } + } + \@@_vcenter:N #1 +% \end{macrocode} +% Append the left label. +% \begin{macrocode} + \tl_if_blank:VF \l_@@_left_label_tl { + \@@_make_simple:Nn #3 { + \box_move_down:nn { \l_@@_label_axis_dim } { \hbox:n { + \cs_set_eq:NN \inserttext \l_@@_left_label_tl + \tl_use:N \l_@@_left_label_template_tl + } } + } + \box_set_ht:cn { \@@_box:N #3 } { 0pt } + \box_set_dp:cn { \@@_box:N #3 } { 0pt } + \@@_append_left:NnN + \l_@@_c_box \l_@@_label_separation_dim \l_@@_d_box + } +% \end{macrocode} +% Append the right label. +% \begin{macrocode} + \tl_if_blank:VF \l_@@_right_label_tl { + \@@_make_simple:Nn #3 { + \box_move_down:nn { \l_@@_label_axis_dim } { \hbox:n { + \cs_set_eq:NN \inserttext \l_@@_right_label_tl + \tl_use:N \l_@@_right_label_template_tl + } } + } + \box_set_ht:cn { \@@_box:N #3 } { 0pt } + \box_set_dp:cn { \@@_box:N #3 } { 0pt } + \@@_append_right:NnN + \l_@@_c_box \l_@@_label_separation_dim \l_@@_d_box + } +} +% \end{macrocode} +% \end{macro} +% +% \subsection{Stack-based interface} +% +% \subsubsection{The stack} +% +% Logically, box structures are stored on a stack. However, \TeX\ does not +% provide data structures for that and the grouping mechanism is not flexible +% enough, so we encode them using what we actually have. A stack for boxes is +% implemented using a global hbox \cs{g_@@_stack_box} that contains all the +% boxes successively. A sequence \cs{g_@@_stack_seq} is used to store the +% dimensions property lists textually. We maintain a counter +% \cs{g_@@_level_int} with the number of elements on the stack, for +% consistency checks. +% \begin{macrocode} +\int_new:N \g_@@_level_int +\box_new:N \g_@@_stack_box +\seq_new:N \g_@@_stack_seq +% \end{macrocode} +% +% \begin{macro}{\@@_clear_stack:} +% Clear the stack. +% \begin{macrocode} +\cs_new:Nn \@@_clear_stack: { + \int_gset:Nn \g_@@_level_int { 0 } + \hbox_gset:Nn \g_@@_stack_box { } + \seq_gclear:N \g_@@_stack_seq +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_push:N} +% Push the contents of a register on the stack. +% \begin{macrocode} +\cs_new:Nn \@@_push:N { + \int_gincr:N \g_@@_level_int + \hbox_gset:Nn \g_@@_stack_box + { \hbox_unpack:N \g_@@_stack_box \box_use:c { \@@_box:N #1 } } + \seq_gput_left:Nv \g_@@_stack_seq + { \@@_marks:N #1 } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_pop:N} +% Pop the value from the top of the stack into a register. +% \begin{macrocode} +\cs_new:Nn \@@_pop:N { + \int_compare:nNnTF { \g_@@_level_int } > { 0 } { + \int_gdecr:N \g_@@_level_int + \hbox_gset:Nn \g_@@_stack_box { + \hbox_unpack:N \g_@@_stack_box + \box_gset_to_last:N \g_tmpa_box + } + \box_set_eq_clear:cN { \@@_box:N #1 } \g_tmpa_box + \seq_gpop_left:NN \g_@@_stack_seq \l_tmpa_tl + \tl_set_eq:cN { \@@_marks:N #1 } \l_tmpa_tl + } { + \PackageError{ebproof}{Missing~premiss~in~a~proof~tree}{} + \@@_clear:N #1 + } +} +% \end{macrocode} +% \end{macro} +% +% \subsubsection{Assembling trees} +% +% \begin{macrocode} +\@@_new:N \l_@@_a_box +\@@_new:N \l_@@_b_box +\@@_new:N \l_@@_c_box +\@@_new:N \l_@@_d_box +% \end{macrocode} +% +% \begin{macro}{\@@_join_horizontal:n} +% Join horizontally a number of elements at the top of the stack. If several +% trees are joined, use the left mark of the left tree, the right mark of +% the right tree and set the axis in the middle of these marks. +% \begin{macrocode} +\cs_new:Nn \@@_join_horizontal:n { + \int_case:nnF { #1 } { + { 0 } { + \group_begin: + \@@_clear:N \l_@@_a_box + \@@_push:N \l_@@_a_box + \group_end: + } + { 1 } { } + } { + \group_begin: + \@@_pop:N \l_@@_a_box + \prg_replicate:nn { #1 - 1 } { + \@@_pop:N \l_@@_b_box + \@@_append_left:NnN + \l_@@_a_box \l_@@_separation_dim \l_@@_b_box + } + \@@_set_mark:Nnn \l_@@_a_box { left } + { \@@_mark:Nn \l_@@_b_box { left } } + \@@_set_mark:Nnn \l_@@_a_box { axis } + { ( \@@_mark:Nn \l_@@_a_box { left } + + \@@_mark:Nn \l_@@_a_box { right } ) / 2 } + \@@_push:N \l_@@_a_box + \group_end: + } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_join_vertical:} +% Join vertically the two elements at the top of the stack, with a +% horizontal rule of the appropriate size. +% \begin{macrocode} +\cs_new:Nn \@@_join_vertical: { + \group_begin: + \@@_pop:N \l_@@_a_box + \@@_pop:N \l_@@_b_box + \@@_enlarge_conclusion:NN \l_@@_b_box \l_@@_a_box + \@@_make_rule_for:NNN \l_@@_c_box \l_@@_b_box + \l_@@_d_box + \@@_append_vertical:NN \l_@@_a_box \l_@@_c_box + \@@_append_vertical:NN \l_@@_a_box \l_@@_b_box + \@@_push:N \l_@@_a_box + \group_end: +} +% \end{macrocode} +% \end{macro} +% +% \subsubsection{High-level commands} +% +% \begin{macro}{\@@_statement_parse:w} +% An auxiliary function for parsing the argument in +% \cs{@@_push_statement:n}. +% \begin{macrocode} +\cs_new:Npn \@@_statement_parse:w #1 & #2 & #3 \q_stop { + \tl_if_empty:nTF { #3 } { + \@@_make_simple:Nn \l_@@_a_box + { \cs_set:Npn \inserttext { #1 } \tl_use:N \l_@@_template_tl } + } { + \@@_make_split:Nnn \l_@@_a_box + { \cs_set:Npn \inserttext { #1 } \tl_use:N \l_@@_left_template_tl } + { \cs_set:Npn \inserttext { #2 } \tl_use:N \l_@@_right_template_tl } + } + \@@_push:N \l_@@_a_box +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_push_statement:n} +% Push a box with default formatting, using explicit alignment if the code +% contains a |&| character +% \begin{macrocode} +\cs_new:Nn \@@_push_statement:n { + \@@_statement_parse:w #1 & & \q_stop +} +% \end{macrocode} +% \end{macro} +% +% \subsection{Document interface} +% +% \subsubsection{Functions to define statements} +% +% The \cs{g_@@_statements_seq} variable contains the list of all defined +% statements. For each statement |X|, there is a document command \cs{ebproofX} +% and the alias \cs{X} is defined when entering a |prooftree| environment. +% \begin{macrocode} +\seq_new:N \g_@@_statements_seq +% \end{macrocode} +% +% \begin{macro}{\@@_setup_statements:} +% Install the aliases for statements, saving the original value of the control +% sequences. +% \begin{macrocode} +\cs_new:Nn \@@_setup_statements: { + \seq_map_inline:Nn \g_@@_statements_seq { + \cs_set_eq:cc { ebproof_saved_ ##1 } { ##1 } + \cs_set_eq:cc { ##1 } { ebproof ##1 } + } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_restore_statements:} +% Restore the saved meanings of the control sequences. This is useful when +% interpreting user-provided code in statement arguments. The meanings are +% automatically restored when leaving a |prooftree| environment because of +% grouping. +% \begin{macrocode} +\cs_new:Nn \@@_restore_statements: { + \seq_map_inline:Nn \g_@@_statements_seq { + \cs_set_eq:cc { ##1 } { ebproof_saved_ ##1 } + } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_new_statement:nnn} +% Define a new statement. The first argument is the name, the second one is +% an argument specifier as used by |xparse| and the third one is the body of +% the command. +% \begin{macrocode} +\cs_new:Nn \@@_new_statement:nnn { + \exp_args:Nc \NewDocumentCommand { ebproof#1 }{ #2 } { #3 } + \seq_put_right:Nn \g_@@_statements_seq { #1 } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\@@_new_deprecated_statement:nnnn} +% Define a deprecated statement. The syntax is the same as above except that +% an extra argument in third position indicates what should be used instead. +% The effect is the same except that a warning message is issued the first +% time the statement is used. +% \begin{macrocode} +\cs_new:Nn \@@_new_deprecated_statement:nnnn { + \cs_new:cpn { ebproof_#1_warning: } { + \PackageWarning { ebproof } { \token_to_str:c{#1}~is~deprecated,~#3 } + \cs_gset:cn { ebproof_#1_warning: } { } + } + \@@_new_statement:nnn { #1 } { #2 } + { \use:c { ebproof_#1_warning: } #4 } +} +% \end{macrocode} +% \end{macro} +% +% +% \subsubsection{Basic commands} +% +% \begin{macro}{\ebproofset,\set} +% This is a simple wrapper around \cs{keys_set:nn}. +% \begin{macrocode} +\@@_new_statement:nnn { set } { m } { + \keys_set:nn { ebproof } { #1 } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\hypo} +% This is mostly a wrapper around \cs{ebproof_push_statement:n}, with +% material to handle options and the statements macros. +% \begin{macrocode} +\@@_new_statement:nnn { hypo } { O{} m } { + \group_begin: + \@@_restore_statements: + \keys_set:nn { ebproof } { #1 } + \@@_push_statement:n { #2 } + \group_end: +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\infer} +% This is a bit more involved than \cs{hypo} because we have to handle rule +% style options and joining. +% \begin{macrocode} +\@@_new_statement:nnn { infer } { O{} m O{} m } { + \group_begin: + \@@_restore_statements: + \keys_set_known:nnN { ebproof / rule~style } { #1 } \l_tmpa_tl + \keys_set:nV { ebproof } \l_tmpa_tl + \tl_set:Nn \l_@@_right_label_tl { #3 } + \@@_join_horizontal:n { #2 } + \@@_push_statement:n { #4 } + \@@_join_vertical: + \group_end: +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\ellipsis} +% An ellipsis is made by hand using vertical leaders to render the dots +% after rendering the label. +% \begin{macrocode} +\@@_new_statement:nnn { ellipsis } { m m } { + \group_begin: + \@@_restore_statements: + \tl_clear:N \l_@@_rule_code_tl + \@@_make_split:Nnn \l_@@_a_box { } { + \vbox_set:Nn \l_tmpa_box { + \skip_vertical:n { 1.2ex } + \hbox:n { \tex_ignorespaces:D #1 } + \skip_vertical:n { 1.2ex } + } + \vbox_to_ht:nn { \box_ht:N \l_tmpa_box } { + \tex_xleaders:D \vbox_to_ht:nn { .8ex } + { \tex_vss:D \hbox:n { . } \tex_vss:D } + \tex_vfill:D + } + \hbox_overlap_right:n { ~ \box_use:N \l_tmpa_box } + } + \@@_push:N \l_@@_a_box + \@@_join_vertical: + \@@_push_statement:n {#2} + \@@_join_vertical: + \group_end: +} +% \end{macrocode} +% \end{macro} +% +% \subsubsection{Modifying trees} +% +% \begin{macro}{\rewrite} +% Rewrite the box at the top of the stack while preserving its dimensions an +% marks. The code is typeset in horizontal mode, with control sequences to +% access the original box and its marks. +% \begin{macrocode} +\@@_new_statement:nnn { rewrite } { m } { + \group_begin: + \@@_restore_statements: + \@@_pop:N \l_@@_a_box + \box_set_eq:Nc \l_tmpa_box { \@@_box:N \l_@@_a_box } + \hbox_set:Nn \l_tmpb_box { + \cs_set_eq:NN \treebox \l_tmpa_box + \cs_set:Npn \treemark { \@@_mark:Nn \l_@@_a_box } + { #1 } + } + \box_set_wd:Nn \l_tmpb_box { \box_wd:c { \@@_box:N \l_@@_a_box } } + \box_set_ht:Nn \l_tmpb_box { \box_ht:c { \@@_box:N \l_@@_a_box } } + \box_set_dp:Nn \l_tmpb_box { \box_dp:c { \@@_box:N \l_@@_a_box } } + \box_set_eq:cN { \@@_box:N \l_@@_a_box } \l_tmpb_box + \@@_push:N \l_@@_a_box + \group_end: +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\delims} +% Insert \cs{left} and \cs{right} delimiters without changing the alignment. +% \begin{macrocode} +\@@_new_statement:nnn { delims } { m m } { + \group_begin: + \@@_restore_statements: + \@@_pop:N \l_@@_a_box + \hbox_set:Nn \l_tmpa_box + { $ \tex_vcenter:D { \box_use:c { \@@_box:N \l_@@_a_box } } $ } + \dim_set:Nn \l_tmpa_dim + { \box_ht:N \l_tmpa_box - \box_ht:c { \@@_box:N \l_@@_a_box } } + \hbox_set:cn { \@@_box:N \l_@@_a_box } { + $ #1 \tex_vrule:D + height \box_ht:N \l_tmpa_box depth \box_dp:N \l_tmpa_box width 0pt + \tex_right:D . $ + } + \@@_shift_x:Nn \l_@@_a_box + { \box_wd:c { \@@_box:N \l_@@_a_box } } + \hbox_set:cn { \@@_box:N \l_@@_a_box } { + \hbox_unpack:c { \@@_box:N \l_@@_a_box } + $ \tex_left:D . \box_use:N \l_tmpa_box #2 $ + } + \hbox_set:cn { \@@_box:N \l_@@_a_box } + { \box_move_down:nn { \l_tmpa_dim } + { \box_use:c { \@@_box:N \l_@@_a_box } } } + \@@_push:N \l_@@_a_box + \group_end: +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\overlay} +% Pop two trees and append the second tree as an overlay over the first one, +% so that the baselines and axes match. The bounding box of the result +% adjusts to contain both trees. +% \begin{macrocode} +\@@_new_statement:nnn { overlay } { } { + \group_begin: + \@@_pop:N \l_@@_a_box + \@@_pop:N \l_@@_b_box + \@@_overlay:NN \l_@@_a_box \l_@@_b_box + \@@_push:N \l_@@_a_box + \group_end: +} +% \end{macrocode} +% \end{macro} +% +% \subsubsection{Deprecated statements} +% +% These statements were defined in versions 1.x of the package, they are +% preserved for temporary upwards compatibility and will be removed in a +% future version. +% \begin{macrocode} +\@@_new_deprecated_statement:nnnn { Alter } { m } + { use~\token_to_str:c{rewrite}~instead } { \ebproofrewrite{ #1 \box\treebox } } +\@@_new_deprecated_statement:nnnn { Delims } { } + { use~\token_to_str:c{delims}~instead } { \ebproofdelims } +\@@_new_deprecated_statement:nnnn { Ellipsis } { } + { use~\token_to_str:c{ellipsis}~instead } { \ebproofellipsis } +\@@_new_deprecated_statement:nnnn { Hypo } { } + { use~\token_to_str:c{hypo}~instead } { \ebproofhypo } +\@@_new_deprecated_statement:nnnn { Infer } { } + { use~\token_to_str:c{infer}~instead } { \ebproofinfer } +% \end{macrocode} +% +% +% \subsubsection{Environment interface} +% +% The stack is initialised globally. The \env{prooftree} environment does not +% clear the stack, instead it saves the initial level in order to check that +% statements are properly balanced. This allows for nested uses of the +% environment, if it ever happens to be useful. +% +% \begin{macrocode} +\@@_clear_stack: +\tl_new:N \l_@@_start_level_tl +% \end{macrocode} +% +% \begin{macro}{prooftree,prooftree*} +% The \env{prooftree} environment. +% \begin{macrocode} +\NewDocumentEnvironment { prooftree } { s O{} } { + \group_align_safe_begin: + \keys_set_known:nnN { ebproof / proof~style } { #2 } \l_tmpa_tl + \keys_set:nV { ebproof } \l_tmpa_tl + \tl_set:Nx \l_@@_start_level_tl { \int_use:N \g_@@_level_int } + \vbox_set:Nw \l_tmpa_box + \@@_setup_statements: +} { + \vbox_set_end: + \@@_pop:N \l_@@_a_box + \int_compare:nNnF { \g_@@_level_int } = { \tl_use:N \l_@@_start_level_tl } { + \PackageError{ebproof}{Malformed~proof~tree}{ + Some~hypotheses~were~declared~but~not~used~in~this~tree.} + } + \IfBooleanTF { #1 } { + \[ \box_use:c { \@@_box:N \l_@@_a_box } \] + \ignorespacesafterend + } { + \hbox_unpack:N \c_empty_box + \bool_if:NTF \l_@@_center_bool { + \hbox:n { $ \tex_vcenter:D { \box_use:c { \@@_box:N \l_@@_a_box } } $ } + } { + \box_use:c { \@@_box:N \l_@@_a_box } + } + } + \group_align_safe_end: +} +% \end{macrocode} +% A trick for the starred version: +% \begin{macrocode} +\cs_new:cpn { prooftree* } { \prooftree* } +\cs_new:cpn { endprooftree* } { \endprooftree } +% \end{macrocode} +% \end{macro} +% +% \begin{macrocode} +% +% \end{macrocode} +% +% \end{implementation} diff --git a/Master/texmf-dist/source/latex/ebproof/ebproof.ins b/Master/texmf-dist/source/latex/ebproof/ebproof.ins new file mode 100644 index 00000000000..25bcc734965 --- /dev/null +++ b/Master/texmf-dist/source/latex/ebproof/ebproof.ins @@ -0,0 +1,15 @@ +%% Copyright (C) 2015-2018 by Emmanuel Beffara +%% +%% 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 +%% 2005/12/01 or later. + +\input l3docstrip.tex +\keepsilent \askforoverwritefalse +\generate{\file{ebproof.sty}{\from{ebproof.dtx}{package}}} +\endbatchfile -- cgit v1.2.3 From a7b1aa320c5c210f2f287f55af834a8ee8628cfa Mon Sep 17 00:00:00 2001 From: Karl Berry Date: Thu, 28 Jan 2021 22:08:51 +0000 Subject: ebproof (28jan21) git-svn-id: svn://tug.org/texlive/trunk@57544 c570f23f-e606-0410-a88d-b1316a301751 --- Master/texmf-dist/doc/latex/ebproof/README.md | 4 +-- Master/texmf-dist/doc/latex/ebproof/ebproof.pdf | Bin 496470 -> 496893 bytes Master/texmf-dist/source/latex/ebproof/ebproof.dtx | 37 +++++++++++++++------ Master/texmf-dist/source/latex/ebproof/ebproof.ins | 2 +- Master/texmf-dist/tex/latex/ebproof/ebproof.sty | 21 ++++++++---- 5 files changed, 43 insertions(+), 21 deletions(-) (limited to 'Master/texmf-dist/source/latex/ebproof') diff --git a/Master/texmf-dist/doc/latex/ebproof/README.md b/Master/texmf-dist/doc/latex/ebproof/README.md index e794db1feed..4c805330cd0 100644 --- a/Master/texmf-dist/doc/latex/ebproof/README.md +++ b/Master/texmf-dist/doc/latex/ebproof/README.md @@ -15,8 +15,8 @@ styles of inference rules, placement of labels, etc. The distribution includes the following files: - `ebproof.dtx` : the doctrip source for the package and documentation +- `ebproof.ins` : the generation script for producing `ebproof.sty` - `ebproof.pdf` : the compiled documentation -- `ebproof.sty` : the generated package The package requires `expl3` (the LaTeX3 programming environment) which provides many useful programming tools. @@ -25,7 +25,7 @@ provides many useful programming tools. License ------- -Copyright 2015-2020 Emmanuel Beffara +Copyright 2015-2021 Emmanuel Beffara This work may be distributed and/or modified under the conditions of the LaTeX Project Public License, either version 1.3 diff --git a/Master/texmf-dist/doc/latex/ebproof/ebproof.pdf b/Master/texmf-dist/doc/latex/ebproof/ebproof.pdf index 60d433b9fd9..ee5c6afa39f 100644 Binary files a/Master/texmf-dist/doc/latex/ebproof/ebproof.pdf and b/Master/texmf-dist/doc/latex/ebproof/ebproof.pdf differ diff --git a/Master/texmf-dist/source/latex/ebproof/ebproof.dtx b/Master/texmf-dist/source/latex/ebproof/ebproof.dtx index 71735ffc007..df4f11f0cab 100644 --- a/Master/texmf-dist/source/latex/ebproof/ebproof.dtx +++ b/Master/texmf-dist/source/latex/ebproof/ebproof.dtx @@ -1,6 +1,6 @@ % \iffalse meta-comment % -% Copyright (C) 2015-2020 by Emmanuel Beffara +% Copyright (C) 2015-2021 by Emmanuel Beffara % % 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 @@ -49,7 +49,7 @@ % }^^A % } % -% \date{Version 2.1 -- Released 2020-08-19} +% \date{Version 2.1.1 -- Released 2021-01-28} % % \maketitle % @@ -648,6 +648,13 @@ % This section lists the principal evolutions of the package, in reverse % chronological order. % \begin{description} +% \item[Version 2.1.1 (2021-01-28)] +% Bugfix release, no changes in the user interface. +% \begin{itemize} +% \item Fixes a deprecation issue with \LaTeX3 release 2021-01-09 and +% various warnings that appear in \LaTeX3 debugging mode. +% \item Fixes \cmd{proof style=downwards}. +% \end{itemize} % \item[Version 2.1 (2020-08-19)] % Mostly a bugfix release. % \begin{itemize} @@ -694,7 +701,7 @@ \NeedsTeXFormat{LaTeX2e} \RequirePackage{expl3} \RequirePackage{xparse} -\ProvidesExplPackage{ebproof}{2020/08/19}{2.1}{EB's proof trees} +\ProvidesExplPackage{ebproof}{2021/01/28}{2.1.1}{EB's proof trees} %<@@=ebproof> % \end{macrocode} % @@ -704,6 +711,7 @@ % section~\ref{sec:options}. % % \begin{macrocode} +\bool_new:N \l_@@_updown_bool \keys_define:nn { ebproof } { center .bool_set:N = \l_@@_center_bool, proof~style .choice: , @@ -828,18 +836,25 @@ label~axis .dim_set:N = \l_@@_label_axis_dim, % \begin{macro}{\@@_new:N} % Using only public interfaces forces a convoluted approach to allocation: % we use a global counter \cs{g_ebproof_register_int} to number registers, -% then each allocation creates registers named \cs{g_ebproof_K_N} where K is -% the kind of component (box or marks) and N is the identifier of the +% then each allocation creates registers named \cs{S_ebproof_K_N} where +% S is the scope of the register (local or global, deduced from the argument), +% K is the kind of component (box or marks) and N is the identifier of the % register. The proof box register itself only contains the identifier used % for indirection. % \begin{macrocode} \int_new:N \g_@@_register_int -\cs_new:Nn \@@_box:N { g__ebproof_box_ \tl_use:N #1 } -\cs_new:Nn \@@_marks:N { g__ebproof_marks_ \tl_use:N #1 } +\cs_new:Nn \@@_box:N { + \str_item:nn { #1 } { 2 } __ebproof_ \tl_use:N #1 _box +} +\cs_new:Nn \@@_marks:N { + \str_item:nn { #1 } { 2 } __ebproof_ \tl_use:N #1 _prop +} \cs_new:Nn \@@_new:N { \tl_new:N #1 \int_gincr:N \g_@@_register_int - \tl_gset:Nx #1 { \int_to_arabic:n { \g_@@_register_int } } + \str_if_eq:eeTF { \str_item:nn { #1 } { 2 } } { g } + { \tl_gset:Nx #1 { \int_to_arabic:n { \g_@@_register_int } } } + { \tl_set:Nx #1 { \int_to_arabic:n { \g_@@_register_int } } } \box_new:c { \@@_box:N #1 } \prop_new:c { \@@_marks:N #1 } } @@ -1068,7 +1083,7 @@ label~axis .dim_set:N = \l_@@_label_axis_dim, % \begin{macrocode} \cs_new:Nn \@@_append_below:NN { \@@_align:NN #1 #2 - \vbox_set_top:Nn #1 { + \vbox_set_top:cn { \@@_box:N #1 } { \box_use:c { \@@_box:N #1 } \tex_prevdepth:D -1000pt \box_use:c { \@@_box:N #2 } @@ -1235,7 +1250,7 @@ label~axis .dim_set:N = \l_@@_label_axis_dim, \hbox_unpack:N \g_@@_stack_box \box_gset_to_last:N \g_tmpa_box } - \box_set_eq_clear:cN { \@@_box:N #1 } \g_tmpa_box + \box_set_eq_drop:cN { \@@_box:N #1 } \g_tmpa_box \seq_gpop_left:NN \g_@@_stack_seq \l_tmpa_tl \tl_set_eq:cN { \@@_marks:N #1 } \l_tmpa_tl } { @@ -1383,7 +1398,7 @@ label~axis .dim_set:N = \l_@@_label_axis_dim, % \begin{macrocode} \cs_new:Nn \@@_new_statement:nnn { \exp_args:Nc \NewDocumentCommand { ebproof#1 }{ #2 } { #3 } - \seq_put_right:Nn \g_@@_statements_seq { #1 } + \seq_gput_right:Nn \g_@@_statements_seq { #1 } } % \end{macrocode} % \end{macro} diff --git a/Master/texmf-dist/source/latex/ebproof/ebproof.ins b/Master/texmf-dist/source/latex/ebproof/ebproof.ins index 25bcc734965..2a62d0abae9 100644 --- a/Master/texmf-dist/source/latex/ebproof/ebproof.ins +++ b/Master/texmf-dist/source/latex/ebproof/ebproof.ins @@ -1,4 +1,4 @@ -%% Copyright (C) 2015-2018 by Emmanuel Beffara +%% Copyright (C) 2015-2021 by Emmanuel Beffara %% %% 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 diff --git a/Master/texmf-dist/tex/latex/ebproof/ebproof.sty b/Master/texmf-dist/tex/latex/ebproof/ebproof.sty index c2d1d0812e7..e34804f4721 100644 --- a/Master/texmf-dist/tex/latex/ebproof/ebproof.sty +++ b/Master/texmf-dist/tex/latex/ebproof/ebproof.sty @@ -23,7 +23,8 @@ \NeedsTeXFormat{LaTeX2e} \RequirePackage{expl3} \RequirePackage{xparse} -\ProvidesExplPackage{ebproof}{2020/08/19}{2.1}{EB's proof trees} +\ProvidesExplPackage{ebproof}{2021/01/28}{2.1.1}{EB's proof trees} +\bool_new:N \l__ebproof_updown_bool \keys_define:nn { ebproof } { center .bool_set:N = \l__ebproof_center_bool, proof~style .choice: , @@ -105,12 +106,18 @@ label~axis .dim_set:N = \l__ebproof_label_axis_dim, \keys_define:nn { ebproof } { #1 .meta:n = { #2 } } } \int_new:N \g__ebproof_register_int -\cs_new:Nn \__ebproof_box:N { g__ebproof_box_ \tl_use:N #1 } -\cs_new:Nn \__ebproof_marks:N { g__ebproof_marks_ \tl_use:N #1 } +\cs_new:Nn \__ebproof_box:N { + \str_item:nn { #1 } { 2 } __ebproof_ \tl_use:N #1 _box +} +\cs_new:Nn \__ebproof_marks:N { + \str_item:nn { #1 } { 2 } __ebproof_ \tl_use:N #1 _prop +} \cs_new:Nn \__ebproof_new:N { \tl_new:N #1 \int_gincr:N \g__ebproof_register_int - \tl_gset:Nx #1 { \int_to_arabic:n { \g__ebproof_register_int } } + \str_if_eq:eeTF { \str_item:nn { #1 } { 2 } } { g } + { \tl_gset:Nx #1 { \int_to_arabic:n { \g__ebproof_register_int } } } + { \tl_set:Nx #1 { \int_to_arabic:n { \g__ebproof_register_int } } } \box_new:c { \__ebproof_box:N #1 } \prop_new:c { \__ebproof_marks:N #1 } } @@ -214,7 +221,7 @@ label~axis .dim_set:N = \l__ebproof_label_axis_dim, } \cs_new:Nn \__ebproof_append_below:NN { \__ebproof_align:NN #1 #2 - \vbox_set_top:Nn #1 { + \vbox_set_top:cn { \__ebproof_box:N #1 } { \box_use:c { \__ebproof_box:N #1 } \tex_prevdepth:D -1000pt \box_use:c { \__ebproof_box:N #2 } @@ -302,7 +309,7 @@ label~axis .dim_set:N = \l__ebproof_label_axis_dim, \hbox_unpack:N \g__ebproof_stack_box \box_gset_to_last:N \g_tmpa_box } - \box_set_eq_clear:cN { \__ebproof_box:N #1 } \g_tmpa_box + \box_set_eq_drop:cN { \__ebproof_box:N #1 } \g_tmpa_box \seq_gpop_left:NN \g__ebproof_stack_seq \l_tmpa_tl \tl_set_eq:cN { \__ebproof_marks:N #1 } \l_tmpa_tl } { @@ -380,7 +387,7 @@ label~axis .dim_set:N = \l__ebproof_label_axis_dim, } \cs_new:Nn \__ebproof_new_statement:nnn { \exp_args:Nc \NewDocumentCommand { ebproof#1 }{ #2 } { #3 } - \seq_put_right:Nn \g__ebproof_statements_seq { #1 } + \seq_gput_right:Nn \g__ebproof_statements_seq { #1 } } \cs_new:Nn \__ebproof_new_deprecated_statement:nnnn { \cs_new:cpn { ebproof_#1_warning: } { -- cgit v1.2.3