summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/tex/latex
diff options
context:
space:
mode:
Diffstat (limited to 'Master/texmf-dist/tex/latex')
-rw-r--r--Master/texmf-dist/tex/latex/ebproof/ebproof.sty1215
1 files changed, 715 insertions, 500 deletions
diff --git a/Master/texmf-dist/tex/latex/ebproof/ebproof.sty b/Master/texmf-dist/tex/latex/ebproof/ebproof.sty
index 33a3f73b916..7601f8e9e85 100644
--- a/Master/texmf-dist/tex/latex/ebproof/ebproof.sty
+++ b/Master/texmf-dist/tex/latex/ebproof/ebproof.sty
@@ -1,8 +1,8 @@
% The ebproof package - Formal proofs in the style of sequent calculus
%% ebproof.sty
-%% Copyright 2015 Emmanuel Beffara <manu@beffara.org>
-%
+%% Copyright 2017 Emmanuel Beffara <manu@beffara.org>
+
% 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.
@@ -10,543 +10,758 @@
% 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 Emmanuel Beffara.
-%
+
% This work consists of the files ebproof.sty and ebproof.tex.
\NeedsTeXFormat{LaTeX2e}
-\ProvidesPackage{ebproof}[2015/03/13 v1.1 EB's proof trees]
+\RequirePackage{expl3}
+\RequirePackage{xparse}
+\ProvidesExplPackage{ebproof}{2017/05/17}{2.0}{EB's proof trees}
-% The |pgfkeys| package is used for the parameters in proof construction.
-\RequirePackage{pgfkeys}
+%% Parameters
-%%% Registers and internal parameters
+%%% Declaration of the parameters
-\newif\ifebproof@updown \ebproof@updownfalse
-\newif\ifebproof@center \ebproof@centertrue
+\keys_define:nn { ebproof } {
-%%% Parameters
+% general shape
-\def\ebproofset#1{\pgfqkeys{/ebproof}{#1}}
+center .bool_set:N = \l_ebproof_center_bool,
+
+proof~style .choice: ,
+proof~style / upwards .code:n = \bool_set_false:N \l_ebproof_updown_bool,
+proof~style / downwards .code:n = \bool_set_true:N \l_ebproof_updown_bool,
-\ebproofset{
-%
-% general shape
-%
-center/.is if=ebproof@center,
-proof style/.is choice,
-proof style/upwards/.code={\ebproof@updownfalse},
-proof style/downwards/.code={\ebproof@updowntrue},
-%
% spacing
-%
-separation/.initial=1.5em,
-rule margin/.initial=.7ex,
-%
+
+separation .dim_set:N = \l_ebproof_separation_dim,
+rule~margin .dim_set:N = \l_ebproof_rule_margin_dim,
+
% shape of inference lines
-%
-rule thickness/.initial=.4pt,
-rule separation/.initial=2pt,
-rule dash length/.initial=.2em,
-rule dash space/.initial=.3em,
-rule code/.initial=,
-%
+
+rule~thickness .dim_set:N = \l_ebproof_rule_thickness_dim,
+rule~separation .dim_set:N = \l_ebproof_rule_separation_dim,
+rule~dash~length .dim_set:N = \l_ebproof_rule_dash_length_dim,
+rule~dash~space .dim_set:N = \l_ebproof_rule_dash_space_dim,
+rule~code .tl_set:N = \l_ebproof_rule_code_tl,
+
+rule~style .choice:,
+
% templates
-%
-template/.initial=$\inserttext$,
-left template/.initial=$\inserttext\mathrel{}$,
-right template/.initial=$\mathrel{}\inserttext$,
-%
+
+template .tl_set:N = \l_ebproof_template_tl,
+left~template .tl_set:N = \l_ebproof_left_template_tl,
+right~template .tl_set:N = \l_ebproof_right_template_tl,
+
% labels
-%
-left label/.initial=,
-right label/.initial=,
-left label template/.initial=\inserttext,
-right label template/.initial=\inserttext,
-label separation/.initial=0.5em,
+
+left~label .tl_set:N = \l_ebproof_left_label_tl,
+right~label .tl_set:N = \l_ebproof_right_label_tl,
+left~label~template .tl_set:N = \l_ebproof_left_label_template_tl,
+right~label~template .tl_set:N = \l_ebproof_right_label_template_tl,
+label~separation .dim_set:N = \l_ebproof_label_separation_dim,
+label~axis .dim_set:N = \l_ebproof_label_axis_dim,
+
}
-% Rule styles
+%%% Rule styles
-\pgfqkeys{/ebproof/rule style}{
-.is choice,
-.search also=/ebproof,
-simple/.style={/ebproof/rule code={%
- \hrule height \pgfkeysvalueof{/ebproof/rule thickness}\relax
- }},
-%
-no rule/.style={/ebproof/rule code=},
-%
-double/.style={/ebproof/rule code={%
- \hrule height \pgfkeysvalueof{/ebproof/rule thickness}
- \kern\pgfkeysvalueof{/ebproof/rule separation}%
- \hrule height \pgfkeysvalueof{/ebproof/rule thickness}
- }},
-%
-dashed/.style={/ebproof/rule code={%
- \hbox to \hsize{%
- \@tempdima=\pgfkeysvalueof{/ebproof/rule dash space}%
- \divide\@tempdima2%
- \kern-\@tempdima%
- \cleaders\hbox{%
- \kern\@tempdima%
- \vrule
- height \pgfkeysvalueof{/ebproof/rule thickness}
- width \pgfkeysvalueof{/ebproof/rule dash length}%
- \kern\@tempdima
- }\hfill
- \kern-\@tempdima
- }%
- }},
-%
-simple % use the 'simple' rule style by default
+\NewDocumentCommand \ebproofnewrulestyle { mm } {
+ \keys_define:nn { ebproof } {
+ rule~style / #1 .meta:nn = { ebproof } { #2 }
+ }
}
-%%% Storage
+\ebproofnewrulestyle { simple } {
+ rule~code = { \tex_hrule:D height \l_ebproof_rule_thickness_dim }
+}
+
+\ebproofnewrulestyle { no~rule } {
+ rule~code =
+}
+
+\ebproofnewrulestyle { double } {
+ rule~code = {
+ \tex_hrule:D height \l_ebproof_rule_thickness_dim
+ \skip_vertical:N \l_ebproof_rule_separation_dim
+ \tex_hrule:D height \l_ebproof_rule_thickness_dim
+ }
+}
+
+\ebproofnewrulestyle { dashed } {
+ rule~code = {
+ \hbox_to_wd:nn { \tex_hsize:D } {
+ \dim_set:Nn \l_tmpa_dim { \l_ebproof_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_ebproof_rule_thickness_dim
+ width \l_ebproof_rule_dash_length_dim
+ \skip_horizontal:N \l_tmpa_dim
+ }\tex_hfill:D
+ \skip_horizontal:n { -\l_tmpa_dim }
+ }
+ }
+}
+
+%%% Default values
+
+\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
+}
+
+%%% Defining style macros
+
+\NewDocumentCommand \ebproofnewstyle { mm } {
+ \keys_define:nn { ebproof } { #1 .meta:n = { #2 } }
+}
+
+
+%% Proof trees
+
+% Proof trees are represented as a data structure that consists of a box and a
+% set of marks, which are vertical positions in the box (as distances from the
+% left edge). Arbitrary marks can be defined, the folowing are used for
+% alignment:
+% - left : the left of the conclusion
+% - right : the right of the conclusion
+% - axis : the vertical axis of the conclusion
+
+
+%%% Registers
-% Proof trees are represented as a data structure that consists of the
-% following data:
-%
-% - box : the tree itself, as a box, with the base line on that of
-% the conclusion
-% - left : the distance from the left of the box to the left of the
-% conclusion
-% - right : the distance from the right of the box to the right of the
-% conclusion
-% - axis : the distance from the left of the box to the vertical axis
-% of the conclusion
-%
% TeX does not actually provide data structures, so we have to encode things.
-% First we provide local allocators, for temporary allocation of registers in
-% a group. Dimensions are initialized to 0pt.
+% 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.
-\def\ebproof@localdimen#1{%
- \advance\count11\@ne% \count11 is the number of the last allocated \dimen
- \expandafter\dimendef\csname#1\endcsname=\count11%
- \csname#1\endcsname=0pt\relax}
+% Create a new register.
-% For boxes, the allocator must be used as
-%
-% \ebproof@localbox{NAME}=\hbox{...}
+\cs_new:Nn \ebproof_new:N {
+ \box_new:N #1
+ \prop_new:c { l_ebproof_marks_ \__int_value:w #1 _prop }
+}
+
+% Clear a register.
+
+\cs_new:Nn \ebproof_clear:N {
+ \hbox_set:Nn #1 {}
+ % Using \box_clear:N instead would not work because trying to push this box
+ % on the stack would not actually append any box.
+ \prop_clear:c { l_ebproof_marks_ \__int_value:w #1 _prop }
+ \ebproof_set_mark:Nnn #1 { left } { 0pt }
+ \ebproof_set_mark:Nnn #1 { right } { 0pt }
+ \ebproof_set_mark:Nnn #1 { axis } { 0pt }
+}
+
+
+%%% Mark operations
+
+% Set the value of a mark. The third argument is a dimension expression.
+
+\dim_new:N \l_ebproof_transit_dim
+
+\cs_new:Nn \ebproof_set_mark:Nnn {
+ \dim_set:Nn \l_ebproof_transit_dim { #3 }
+ \prop_put:cnV { l_ebproof_marks_ \__int_value:w #1 _prop } { #2 }
+ \l_ebproof_transit_dim
+}
+
+% Get the value of a mark. This is expandable and can be used in expressions.
+
+\cs_new:Nn \ebproof_mark:Nn {
+ \prop_item:cn { l_ebproof_marks_ \__int_value:w #1 _prop } { #2 }
+}
+
+% Shift the marks by a specified amount, without modifying the box.
+
+\cs_new:Nn \ebproof_shift_x:Nn {
+ \prop_map_inline:cn { l_ebproof_marks_ \__int_value:w #1 _prop } {
+ \ebproof_set_mark:Nnn #1 { ##1 } { ##2 + #2 }
+ }
+}
+
+% Move 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 if the marks
+% are set as
+% 1: L---A-------R
+% 2: L-------A---R
+% then the marks of the first tree are then set as
+% 1: L-------A-------R
+% The contents of the tree are unchanged.
+
+\cs_new:Nn \ebproof_enlarge_conclusion:NN {
+ \dim_set:Nn \l_tmpa_dim { \ebproof_mark:Nn #1 {axis}
+ + \ebproof_mark:Nn #2 {left} - \ebproof_mark:Nn #2 {axis} }
+ \dim_compare:nNnT { \l_tmpa_dim } < { \ebproof_mark:Nn #1 {left} } {
+ \ebproof_set_mark:Nnn #1 {left} { \l_tmpa_dim } }
+ \dim_set:Nn \l_tmpa_dim { \ebproof_mark:Nn #1 {axis}
+ + \ebproof_mark:Nn #2 {right} - \ebproof_mark:Nn #2 {axis} }
+ \dim_compare:nNnT { \l_tmpa_dim } > { \ebproof_mark:Nn #1 {right} } {
+ \ebproof_set_mark:Nnn #1 {right} { \l_tmpa_dim } }
+}
+
+
+%%% Building blocks
+
+% 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.
+
+\cs_new:Nn \ebproof_make_simple:Nn {
+ \hbox_set:Nn #1 { #2 }
+ \ebproof_set_mark:Nnn #1 { left } { 0pt }
+ \ebproof_set_mark:Nnn #1 { axis } { \box_wd:N #1 / 2 }
+ \ebproof_set_mark:Nnn #1 { right } { \box_wd:N #1 }
+}
+
+% 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.
+
+\cs_new:Nn \ebproof_make_split:Nnn {
+ \ebproof_set_mark:Nnn #1 { left } { 0pt }
+ \hbox_set:Nn #1 { #2 }
+ \ebproof_set_mark:Nnn #1 { axis } { \box_wd:N #1 }
+ \hbox_set:Nn #1 { \hbox_unpack:N #1 #3 }
+ \ebproof_set_mark:Nnn #1 { right } { \box_wd:N #1 }
+}
+
+% Make a tree with explicit material in vertical mode, using an explicit width
+% and axis.
+
+\cs_new:Nn \ebproof_make_vertical:Nnnn {
+ \ebproof_set_mark:Nnn #1 { left } { 0pt }
+ \ebproof_set_mark:Nnn #1 { axis } { #2 }
+ \ebproof_set_mark:Nnn #1 { right } { #3 }
+ \vbox_set:Nn #1 {
+ \dim_set:Nn \tex_hsize:D { \ebproof_mark:Nn #1 {right} }
+ #4
+ }
+ \box_set_wd:Nn #1 { \ebproof_mark:Nn #1 {right} }
+}
+
+%%% Assembling boxes
+
+% 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.
+
+\cs_new:Nn \ebproof_extend:Nnnnn {
+ \dim_compare:nNnF { #2 } = { 0pt } {
+ \hbox_set:Nn #1 {
+ \skip_horizontal:n { #2 }
+ \box_use:N #1
+ }
+ \ebproof_shift_x:Nn #1 { #2 }
+ }
+ \box_set_ht:Nn #1 { \box_ht:N #1 + #3 }
+ \box_set_wd:Nn #1 { \box_wd:N #1 + #4 }
+ \box_set_dp:Nn #1 { \box_dp:N #1 + #5 }
+}
+
+% 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.
+
+\cs_new:Nn \ebproof_append_right:NnN {
+ \hbox_set:Nn #1 {
+ \box_use:N #1
+ \dim_compare:nNnF { #2 } = { 0pt } { \skip_horizontal:n { #2 } }
+ \box_use:N #3
+ }
+}
+
+% 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.
+
+\cs_new:Nn \ebproof_append_left:NnN {
+ \ebproof_shift_x:Nn #1 { \box_wd:N #3 + #2 }
+ \hbox_set:Nn #1 {
+ \box_use:N #3
+ \dim_compare:nNnF { #2 } = { 0pt } { \skip_horizontal:n { #2 } }
+ \box_use:N #1
+ }
+}
+
+% Shift of two trees to the right so that the axes match. The marks of the one
+% that is shifted are updated accordingly.
+
+\cs_new:Nn \ebproof_align:NN {
+ \dim_set:Nn \l_tmpa_dim
+ { \ebproof_mark:Nn #2 {axis} - \ebproof_mark:Nn #1 {axis} }
+ \dim_compare:nNnTF \l_tmpa_dim < { 0pt } {
+ \ebproof_extend:Nnnnn #2 { -\l_tmpa_dim } { 0pt } { 0pt } { 0pt }
+ } {
+ \ebproof_extend:Nnnnn #1 { \l_tmpa_dim } { 0pt } { 0pt } { 0pt }
+ }
+}
+
+% Append the contents of the second tree above the first one, with matching
+% axes. The marks of the first tree are preserved.
+
+\cs_new:Nn \ebproof_append_above:NN {
+ \ebproof_align:NN #1 #2
+ \vbox_set:Nn #1 {
+ \box_use:N #2
+ \tex_prevdepth:D -1000pt
+ \box_use:N #1
+ }
+}
+
+% Append the contents of the second tree below the first one, with matching
+% axes. The marks of the first tree are preserved.
+
+\cs_new:Nn \ebproof_append_below:NN {
+ \ebproof_align:NN #1 #2
+ \vbox_set_top:Nn #1 {
+ \box_use:N #1
+ \tex_prevdepth:D -1000pt
+ \box_use:N #2
+ }
+}
+
+% Shift the material in a tree vertically so that the height and depth are
+% equal (like TeX's \vcenter but around the baseline).
+
+\cs_new:Nn \ebproof_vcenter:N {
+ \dim_set:Nn \l_tmpa_dim { ( \box_ht:N #1 - \box_dp:N #1 ) / 2 }
+ \box_set_eq:NN \l_tmpa_box #1
+ \hbox_set:Nn #1
+ { \box_move_down:nn { \l_tmpa_dim } { \box_use:N \l_tmpa_box } }
+}
+
+
+%% Making inferences
%
-% in order to set the value of the box.
-
-\def\ebproof@localbox#1{%
- \advance\count14\@ne% \count14 is the number of the last allocated \box
- \expandafter\chardef\csname#1\endcsname\count14%
- \setbox\csname#1\endcsname}
-
-% From this we deduce an allocator for data structures. This allocator
-% receives a base name |A| and defines the registers |\A@box|, |\A@left|,
-% |\A@right| and |\A@axis|. The macro is used like |\ebproof@localbox|, by
-% providing a value for the box.
-
-\def\ebproof@alloc#1{%
- \ebproof@localdimen{#1@left}%
- \ebproof@localdimen{#1@right}%
- \ebproof@localdimen{#1@axis}%
- \ebproof@localbox{#1@box}}
-
-% Logically, such structures are stored on a stack. However, TeX does not
-% provide data structures, so we encode them using what we actually have. A
-% stack for boxes is implemented using a global hbox |\ebproof@box@stack| that
-% contains all the boxes successively, and the |\lastbox| primitive allows us
-% to pop elements from there. A macro |\ebproof@stack| is used to store the
-% dimensions textually: the empty stack is an empty macro, and a non-empty
-% stack is represented as |{left}{right}{axis}{tail}|. We maintain a counter
-% |\ebproof@level| with the number of elements on the stack, for consistency
-% checks.
-
-\newcount\ebproof@level
-\newbox\ebproof@box@stack
-\newbox\ebproof@box@temp
+% The following commands use the parameters defined at the beginning of the
+% package for actually building proof trees using the commands defined above.
+
+% 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.
+
+\cs_new:Nn \ebproof_append_vertical:NN {
+ \bool_if:NTF \l_ebproof_updown_bool
+ { \ebproof_append_below:NN #1 #2 }
+ { \ebproof_append_above:NN #1 #2 }
+}
+
+% 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.
+
+\cs_new:Nn \ebproof_make_rule_for:NNN {
+
+ % Build the rule.
+
+ \ebproof_make_vertical:Nnnn #1
+ { \ebproof_mark:Nn #2 {axis} - \ebproof_mark:Nn #2 {left} }
+ { \ebproof_mark:Nn #2 {right} - \ebproof_mark:Nn #2 {left} }
+ {
+ \skip_vertical:N \l_ebproof_rule_margin_dim
+ \tl_if_empty:NF { \l_ebproof_rule_code_tl } {
+ \tl_use:N \l_ebproof_rule_code_tl
+ \skip_vertical:N \l_ebproof_rule_margin_dim
+ }
+ }
+ \ebproof_vcenter:N #1
+
+ % Append the left label
+
+ \tl_if_blank:VF \l_ebproof_left_label_tl {
+ \ebproof_make_simple:Nn #3 {
+ \box_move_down:nn { \l_ebproof_label_axis_dim } { \hbox:n {
+ \cs_set_eq:NN \inserttext \l_ebproof_left_label_tl
+ \tl_use:N \l_ebproof_left_label_template_tl
+ } }
+ }
+ \box_set_ht:Nn #3 { 0pt }
+ \box_set_dp:Nn #3 { 0pt }
+ \ebproof_append_left:NnN
+ \l_ebproof_c_box \l_ebproof_label_separation_dim \l_ebproof_d_box
+ }
+
+ % Append the right label
+
+ \tl_if_blank:VF \l_ebproof_right_label_tl {
+ \ebproof_make_simple:Nn #3 {
+ \box_move_down:nn { \l_ebproof_label_axis_dim } { \hbox:n {
+ \cs_set_eq:NN \inserttext \l_ebproof_right_label_tl
+ \tl_use:N \l_ebproof_right_label_template_tl
+ } }
+ }
+ \box_set_ht:Nn #3 { 0pt }
+ \box_set_dp:Nn #3 { 0pt }
+ \ebproof_append_right:NnN
+ \l_ebproof_c_box \l_ebproof_label_separation_dim \l_ebproof_d_box
+ }
+
+}
+
+
+%% Stack-based interface
+
+%%% 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 |\g_ebproof_stack_box| that contains all the
+% boxes successively. A sequence |\g_ebproof_stack_seq| is used to store the
+% dimensions property lists textually. We maintain a counter
+% |\g_ebproof_level_int| with the number of elements on the stack, for
+% consistency checks.
+
+\int_new:N \g_ebproof_level_int
+\box_new:N \g_ebproof_stack_box
+\seq_new:N \g_ebproof_stack_seq
% Clear the stack.
-\def\ebproof@clear{%
- \global\ebproof@level=0%
- \global\setbox\ebproof@box@stack=\box\voidb@x%
- \gdef\ebproof@stack{}}
-
-% Push an allocated structure (by name) on the stack.
-
-\def\ebproof@push#1{%
- \global\advance\ebproof@level1\relax
- \global\setbox\ebproof@box@stack=\hbox{%
- \unhbox\ebproof@box@stack\copy\csname#1@box\endcsname}%
- \xdef\ebproof@stack{%
- {\the\csname#1@left\endcsname}%
- {\the\csname#1@right\endcsname}%
- {\the\csname#1@axis\endcsname}%
- {\ebproof@stack}}}
-
-% Allocate a structure and pop its value from the top of the stack.
-
-\def\ebproof@pop#1{%
- \ifnum\ebproof@level>0\relax
- \global\advance\ebproof@level-1\relax
- \global\setbox\ebproof@box@stack=\hbox{%
- \unhbox\ebproof@box@stack
- \global\setbox\ebproof@box@temp=\lastbox}%
- \ebproof@alloc{#1}=\box\ebproof@box@temp%
- \begingroup\def\pop##1##2##3##4{\endgroup%
- \csname#1@left\endcsname=##1\relax
- \csname#1@right\endcsname=##2\relax
- \csname#1@axis\endcsname=##3\relax
- \gdef\ebproof@stack{##4}}%
- \expandafter\pop\ebproof@stack
- \else
- \PackageError{ebproof}{%
- Missing premiss in a proof tree}{}%
- \ebproof@alloc{#1}=\box\voidb@x%
- \fi}
-
-
-%%% Making boxes
-
-% Push a box with the axis in the middle.
-
-\def\ebproof@pushsimple#1{%
- \begingroup
- \ebproof@alloc{A}=\hbox{#1}%
- \A@axis=.5\wd\A@box
- \ebproof@push{A}%
- \endgroup}
-
-% Push a box made of two halves, with the axis between the halves.
-
-\def\ebproof@pushsplit#1#2{%
- \begingroup
- \ebproof@alloc{A}=\hbox{#1}%
- \A@axis=\wd\A@box
- \setbox\A@box=\hbox{\unhbox\A@box#2}%
- \ebproof@push{A}%
- \endgroup}
-
-% Join horizontally the two elements at the top of the stack.
-
-\def\ebproof@joinh{%
- \begingroup
- \ebproof@pop{A}%
- \ebproof@pop{B}%
- \ebproof@alloc{C}=\hbox{%
- \box\B@box
- \kern\pgfkeysvalueof{/ebproof/separation}%
- \box\A@box}%
- \C@left=\B@left
- \C@right=\A@right
- \C@axis=\wd\C@box
- \advance\C@axis\B@left
- \advance\C@axis-\A@right
- \divide\C@axis2\relax
- \ebproof@push{C}%
- \endgroup}
-
-% An $n$-ary version of the horizontal join.
-
-\def\ebproof@joinh@multi#1{%
- \begingroup
- \countdef\c=1
- \c=#1\relax%
- \ifnum\c=0
- \ebproof@alloc{X}=\hbox{}%
- \ebproof@push{X}%
- \else
- \ebproof@joinh@loop
- \fi
- \endgroup}
-\def\ebproof@joinh@loop{%
- \ifnum\c>1
- \ebproof@joinh
- \advance\c-1
- \expandafter\ebproof@joinh@loop
- \fi}
-
-% Append the last element to the right of the previous one, without changing
-% its alignment.
-
-\def\ebproof@joinright{%
- \begingroup
- \ebproof@pop{A}%
- \ebproof@pop{B}%
- \ebproof@alloc{C}=\hbox{%
- \box\B@box
- \kern\pgfkeysvalueof{/ebproof/separation}%
- \copy\A@box}%
- \C@left=\B@left
- \C@right=\B@right
- \advance\C@right\wd\A@box
- \advance\C@right\pgfkeysvalueof{/ebproof/separation}%
- \ebproof@push{C}%
- \endgroup}
+\cs_new:Nn \ebproof_clear_stack: {
+ \int_gset:Nn \g_ebproof_level_int { 0 }
+ \hbox_gset:Nn \g_ebproof_stack_box { }
+ \seq_gclear:N \g_ebproof_stack_seq
+}
-% Join vertically the two elements at the top of the stack, with a horizontal
-% rule of the appropriate size.
+% Push the contents of a register on the stack.
-\def\ebproof@joinv{%
- \begingroup
- \ebproof@pop{A}%
- \ebproof@pop{B}%
- %
- \ebproof@alloc{C}=\box\voidb@x%
- \ebproof@localdimen{A@shift}%
- \ebproof@localdimen{B@shift}%
- \ebproof@localdimen{R@shift}%
- \ebproof@localdimen{R@raise}%
- \ebproof@localdimen{R@width}%
- \ebproof@localdimen{C@width}%
- \ebproof@localdimen{tmp}%
- %
- % The placement of the boxes and the axis of the result
- \ifdim\A@axis>\B@axis
- \A@shift=0pt%
- \B@shift=\A@axis
- \advance\B@shift-\B@axis
- \C@axis=\A@axis
- \else
- \A@shift=\B@axis
- \advance\A@shift-\A@axis
- \B@shift=0pt%
- \C@axis=\B@axis
- \fi
- % The paddings of the result
- \C@left=\A@left
- \advance\C@left\A@shift
- \C@right=\A@right
- \tmp=\wd\B@box
- \advance\tmp\B@shift
- \advance\tmp-\wd\A@box
- \advance\tmp-\A@shift
- \ifdim\tmp>0pt%
- \C@width=\wd\B@box
- \advance\C@width\B@shift
- \advance\C@right\tmp
- \else
- \C@width=\wd\A@box
- \advance\C@width\A@shift
- \fi
- % The position of the rule
- \R@shift=\A@left
- \advance\R@shift\A@shift
- \tmp=\B@left
- \advance\tmp\B@shift
- \ifdim\R@shift>\tmp
- \R@shift=\tmp
- \fi
- % The width of the rule
- \R@width=\wd\A@box
- \advance\R@width\A@shift
- \advance\R@width-\A@right
- \tmp=\wd\B@box
- \advance\tmp\B@shift
- \advance\tmp-\B@right
- \ifdim\tmp>\R@width
- \R@width=\tmp
- \fi
- \advance\R@width-\R@shift
- % Make the rule box
- \ebproof@localbox{R@box}=\vbox{%
- \hsize=\R@width
- \hrule width \R@width height 0pt\relax
- \kern\pgfkeysvalueof{/ebproof/rule margin}%
- \pgfkeysgetvalue{/ebproof/rule code}{\@rulecode}%
- \ifx\@rulecode\@empty\else
- \@rulecode
- \unskip% so that only one margin is inserted if no rule is drawn
- \kern\pgfkeysvalueof{/ebproof/rule margin}%
- \fi
- }%
- % Make the label boxes
- \ebproof@localbox{LEFT}=\hbox{%
- \def\inserttext{\pgfkeysvalueof{/ebproof/left label}}%
- \pgfkeysvalueof{/ebproof/left label template}}%
- \ebproof@localbox{RIGHT}=\hbox{%
- \def\inserttext{\pgfkeysvalueof{/ebproof/right label}}%
- \pgfkeysvalueof{/ebproof/right label template}}%
- % Shift things if the left box is wider than |\R@shift|
- \ifvoid\LEFT\else
- \tmp=\wd\LEFT
- \advance\tmp\pgfkeysvalueof{/ebproof/label separation}
- \ifdim\tmp>\R@shift
- \advance\tmp-\R@shift
- \advance\A@shift\tmp
- \advance\B@shift\tmp
- \advance\C@left\tmp
- \advance\C@axis\tmp
- \advance\C@width\tmp
- \R@shift=0pt\relax
- \else
- \advance\R@shift-\tmp
- \fi
- \fi
- % Compute how the rule box must be shifted so that labels are aligned
- \ebproof@localbox{RC@box}=\hbox{$\vcenter{\copy\R@box}$}%
- \R@raise=\ht\R@box
- \advance\R@raise-\ht\RC@box
- % Make the complete rule box
- \setbox\RC@box=\hbox{%
- \ifvoid\LEFT\else
- \box\LEFT
- \kern\pgfkeysvalueof{/ebproof/label separation}
- \fi
- \box\RC@box
- \ifvoid\RIGHT\else
- \kern\pgfkeysvalueof{/ebproof/label separation}
- \box\RIGHT
- \fi}
- % Adapt the dimensions on the right if the total rule width is too large
- \tmp=\wd\RC@box
- \advance\tmp\R@shift
- \ifdim\tmp>\C@width
- \advance\tmp-\C@width
- \advance\C@right\tmp
- \fi
- % Cancel the labels' height and depth
- \setbox\RC@box=\hbox{\raise\R@raise\box\RC@box}
- \ht\RC@box=\ht\R@box
- \dp\RC@box=\dp\R@box
- % Make the box
- \ifebproof@updown
- \setbox\C@box=\vtop{%
- \moveright\A@shift\box\A@box
- \hrule height 0pt
- \moveright\R@shift\box\RC@box%
- \hrule height 0pt
- \moveright\B@shift\box\B@box}%
- \else
- \setbox\C@box=\vbox{%
- \moveright\B@shift\box\B@box
- \hrule height 0pt
- \moveright\R@shift\box\RC@box%
- \hrule height 0pt
- \moveright\A@shift\box\A@box}%
- \fi
- \ebproof@push{C}%
- \endgroup}
-
-%%% Modifying boxes
-
-% Alter a proof with a command that does not affect the size. Typically useful
-% with |\color| commands.
-
-\def\ebproof@alter#1{%
- \begingroup
- \ebproof@pop{A}%
- \setbox\A@box=\hbox{{#1\box\A@box}}%
- \ebproof@push{A}%
- \endgroup}
+\cs_new:Nn \ebproof_push:N {
+ \int_gincr:N \g_ebproof_level_int
+ \hbox_gset:Nn \g_ebproof_stack_box
+ { \hbox_unpack:N \g_ebproof_stack_box \box_use:N #1 }
+ \seq_gput_left:Nv \g_ebproof_stack_seq
+ { l_ebproof_marks_ \__int_value:w #1 _prop }
+}
-% Insert |\left| and |\right| delimiters without changing the alignment
+% Pop the value from the top of the stack into a register.
+
+\cs_new:Nn \ebproof_pop:N {
+ \int_compare:nNnTF { \g_ebproof_level_int } > { 0 } {
+ \int_gdecr:N \g_ebproof_level_int
+ \hbox_gset:Nn \g_ebproof_stack_box {
+ \hbox_unpack:N \g_ebproof_stack_box
+ \box_gset_to_last:N \g_tmpa_box
+ }
+ \box_set_eq_clear:NN #1 \g_tmpa_box
+ \seq_gpop_left:NN \g_ebproof_stack_seq \l_tmpa_tl
+ \tl_set_eq:cN { l_ebproof_marks_ \__int_value:w #1 _prop } \l_tmpa_tl
+ } {
+ \PackageError{ebproof}{Missing~premiss~in~a~proof~tree}{}
+ \ebproof_clear:N #1
+ }
+}
+
+%%% Assembling trees
+
+\ebproof_new:N \l_ebproof_a_box
+\ebproof_new:N \l_ebproof_b_box
+\ebproof_new:N \l_ebproof_c_box
+\ebproof_new:N \l_ebproof_d_box
+
+% 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.
+
+\cs_new:Nn \ebproof_join_horizontal:n {
+ \int_case:nnF { #1 } {
+ { 0 } {
+ \group_begin:
+ \ebproof_clear:N \l_ebproof_a_box
+ \ebproof_push:N \l_ebproof_a_box
+ \group_end:
+ }
+ { 1 } { }
+ } {
+ \group_begin:
+ \ebproof_pop:N \l_ebproof_a_box
+ \prg_replicate:nn { #1 - 1 } {
+ \ebproof_pop:N \l_ebproof_b_box
+ \ebproof_append_left:NnN
+ \l_ebproof_a_box \l_ebproof_separation_dim \l_ebproof_b_box
+ }
+ \ebproof_set_mark:Nnn \l_ebproof_a_box { left }
+ { \ebproof_mark:Nn \l_ebproof_b_box { left } }
+ \ebproof_set_mark:Nnn \l_ebproof_a_box { axis }
+ { ( \ebproof_mark:Nn \l_ebproof_a_box { left }
+ + \ebproof_mark:Nn \l_ebproof_a_box { right } ) / 2 }
+ \ebproof_push:N \l_ebproof_a_box
+ \group_end:
+ }
+}
-\def\ebproof@delims#1#2{%
- \begingroup
- \ebproof@pop{TREE}%
- \ebproof@localbox{@SHIFTED}=%
- \hbox{$\vcenter{\copy\TREE@box}$}%
- \ebproof@localbox{@LEFT}=%
- \hbox{$#1\vrule height \ht\@SHIFTED depth \dp\@SHIFTED width 0pt\right.$}%
- \ebproof@localbox{@RIGHT}=%
- \hbox{$\left.\vrule height \ht\@SHIFTED depth \dp\@SHIFTED width 0pt#2$}%
- \ebproof@localdimen{dy}
- \dy=\dp\@SHIFTED
- \advance\dy-\dp\TREE@box
- \ebproof@alloc{A}=%
- \hbox{\raise\dy\hbox{\copy\@LEFT\box\@SHIFTED\copy\@RIGHT}}%
- \A@left=\wd\@LEFT \advance\A@left\TREE@left
- \A@right=\wd\@RIGHT \advance\A@right\TREE@right
- \A@axis=\wd\@LEFT \advance\A@axis\TREE@axis
- \ebproof@push{A}%
- \endgroup}
+% Join vertically the two elements at the top of the stack, with a horizontal
+% rule of the appropriate size.
+
+\cs_new:Nn \ebproof_join_vertical: {
+ \group_begin:
+ \ebproof_pop:N \l_ebproof_a_box
+ \ebproof_pop:N \l_ebproof_b_box
+ \ebproof_enlarge_conclusion:NN \l_ebproof_b_box \l_ebproof_a_box
+ \ebproof_make_rule_for:NNN \l_ebproof_c_box \l_ebproof_b_box
+ \l_ebproof_d_box
+ \ebproof_append_vertical:NN \l_ebproof_a_box \l_ebproof_c_box
+ \ebproof_append_vertical:NN \l_ebproof_a_box \l_ebproof_b_box
+ \ebproof_push:N \l_ebproof_a_box
+ \group_end:
+}
%%% High-level commands
% Push a box with default formatting, using explicit alignment if the code
% contains a |&| character
-\def\ebproof@hypo@parse#1&#2&#3\ebproof@hypo@stop{
- {\def\ARG{#3}\ifx\ARG\@empty
- \aftergroup\iftrue\@gobble\fi
- \else\aftergroup\iffalse\@gobble\fi\fi}%
- % The above code has produced \iftrue or \iffalse here.
- \ebproof@pushsimple%
- {\def\inserttext{#1}\pgfkeysvalueof{/ebproof/template}}%
- \else
- \ebproof@pushsplit
- {\def\inserttext{#1}\pgfkeysvalueof{/ebproof/left template}}%
- {\def\inserttext{#2}\pgfkeysvalueof{/ebproof/right template}}%
- \fi}
-
-\newcommand\ebproof@hypo[2][]{%
- {\ebproofset{#1}\ebproof@hypo@parse#2&&\ebproof@hypo@stop}}
-
-% Build a n-ary rule
-
-\def\ebproof@infer{%
- \@ifnextchar[{\ebproof@infer@}{\ebproof@infer@[]}}
-\def\ebproof@infer@[#1]#2{%
- \@ifnextchar[%
- {\ebproof@infer@with@label{#1}{#2}}%
- {\ebproof@infer@@{#1}{#2}}}
-\def\ebproof@infer@with@label#1#2[#3]{%
- \ebproof@infer@@{#1,right label={#3}}{#2}}
-\def\ebproof@infer@@#1#2#3{{%
- \pgfqkeys{/ebproof/rule style}{.search also=/ebproof,#1}%
- \ebproof@joinh@multi{#2}%
- \ebproof@hypo{#3}%
- \ebproof@joinv}}
-
-% Ellipsis with vertical dots
-
-\def\ebproof@ellipsis#1#2{{%
- \ebproofset{rule code=}%
- \ebproof@pushsplit{}{%
- \setbox0=\vbox{\kern1.2ex\hbox{\ignorespaces#1}\hrule height 0pt\kern1.2ex}%
- \vbox to\ht0{\xleaders\vbox to .8ex{\vss\hbox{.}\vss}\vfill}%
- \rlap{ \box0}}%
- \ebproof@joinv
- \ebproof@hypo{#2}%
- \ebproof@joinv}}
+\cs_new:Npn \ebproof_statement_parse:w #1&#2&#3\ebproof_statement_stop: {
+ \tl_if_empty:nTF { #3 } {
+ \ebproof_make_simple:Nn \l_ebproof_a_box
+ { \cs_set:Npn \inserttext { #1 } \tl_use:N \l_ebproof_template_tl }
+ } {
+ \ebproof_make_split:Nnn \l_ebproof_a_box
+ { \cs_set:Npn \inserttext { #1 } \tl_use:N \l_ebproof_left_template_tl }
+ { \cs_set:Npn \inserttext { #2 } \tl_use:N \l_ebproof_right_template_tl }
+ }
+ \ebproof_push:N \l_ebproof_a_box
+}
+
+\cs_new:Nn \ebproof_push_statement:n {
+ \ebproof_statement_parse:w #1&& \ebproof_statement_stop:
+}
+
+
+%% Document interface
+
+%%% Functions to define statements
+
+% The |\g_ebproof_stack_seq| variable contains the list of all defined
+% statements. For each statement |X|, there is a document command |\ebproofX|
+% and the alias |\X| is defined when entering a |prooftree| environment.
+
+\seq_new:N \g_ebproof_statements_seq
+
+% Install the aliases for statements, saving the original value of the control
+% sequences.
+
+\cs_new:Nn \ebproof_setup_statements: {
+ \seq_map_inline:Nn \g_ebproof_statements_seq {
+ \cs_set_eq:cc { ebproof_saved_ ##1 } { ##1 }
+ \cs_set_eq:cc { ##1 } { ebproof ##1 }
+ }
+}
+
+% 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.
+
+\cs_new:Nn \ebproof_restore_statements: {
+ \seq_map_inline:Nn \g_ebproof_statements_seq {
+ \cs_set_eq:cc { ##1 } { ebproof_saved_ ##1 }
+ }
+}
+
+% 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.
+
+\cs_new:Nn \ebproof_new_statement:nnn {
+ \exp_args:Nc \NewDocumentCommand { ebproof#1 }{ #2 } { #3 }
+ \seq_put_right:Nn \g_ebproof_statements_seq { #1 }
+}
+
+% 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.
+
+\cs_new:Nn \ebproof_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: } { }
+ }
+ \ebproof_new_statement:nnn { #1 } { #2 }
+ { \use:c { ebproof_#1_warning: } #4 }
+}
+
+
+%%% Basic commands
+
+\ebproof_new_statement:nnn { set } { m } {
+ \keys_set:nn { ebproof } { #1 }
+}
+
+\ebproof_new_statement:nnn { hypo } { O{} m } {
+ \group_begin:
+ \ebproof_restore_statements:
+ \keys_set:nn { ebproof } { #1 }
+ \ebproof_push_statement:n { #2 }
+ \group_end:
+}
+
+\ebproof_new_statement:nnn { infer } { O{} m O{} m } {
+ \group_begin:
+ \ebproof_restore_statements:
+ \keys_set_known:nnN { ebproof / rule~style } { #1 } \l_tmpa_tl
+ \keys_set:nV { ebproof } \l_tmpa_tl
+ \tl_set:Nn \l_ebproof_right_label_tl { #3 }
+ \ebproof_join_horizontal:n { #2 }
+ \ebproof_push_statement:n { #4 }
+ \ebproof_join_vertical:
+ \group_end:
+}
+
+\ebproof_new_statement:nnn { ellipsis } { m m } {
+ \group_begin:
+ \ebproof_restore_statements:
+ \tl_clear:N \l_ebproof_rule_code_tl
+ \ebproof_make_split:Nnn \l_ebproof_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 }
+ }
+ \ebproof_push:N \l_ebproof_a_box
+ \ebproof_join_vertical:
+ \ebproof_push_statement:n {#2}
+ \ebproof_join_vertical:
+ \group_end:
+}
+
+
+%%% Modifying trees
+
+% 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:
+% - \treebox is a box register with the original material
+% - \treemark{NAME} provides the value of a given mark
+
+\ebproof_new_statement:nnn { rewrite } { m } {
+ \group_begin:
+ \ebproof_restore_statements:
+ \ebproof_pop:N \l_ebproof_a_box
+ \box_set_eq:NN \l_tmpa_box \l_ebproof_a_box
+ \hbox_set:Nn \l_tmpb_box {
+ \cs_set_eq:NN \treebox \l_tmpa_box
+ \cs_set:Npn \treemark { \ebproof_mark:Nn \l_ebproof_a_box }
+ { #1 }
+ }
+ \box_set_wd:Nn \l_tmpb_box { \box_wd:N \l_ebproof_a_box }
+ \box_set_ht:Nn \l_tmpb_box { \box_ht:N \l_ebproof_a_box }
+ \box_set_dp:Nn \l_tmpb_box { \box_dp:N \l_ebproof_a_box }
+ \box_set_eq:NN \l_ebproof_a_box \l_tmpb_box
+ \ebproof_push:N \l_ebproof_a_box
+ \group_end:
+}
+
+% Insert |\left| and |\right| delimiters without changing the alignment
+
+\ebproof_new_statement:nnn { delims } { m m } {
+ \group_begin:
+ \ebproof_restore_statements:
+ \ebproof_pop:N \l_ebproof_a_box
+ \hbox_set:Nn \l_tmpa_box
+ { $ \tex_vcenter:D { \box_use:N \l_ebproof_a_box } $ }
+ \dim_set:Nn \l_tmpa_dim
+ { \box_ht:N \l_tmpa_box - \box_ht:N \l_ebproof_a_box }
+ \hbox_set:Nn \l_ebproof_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 . $
+ }
+ \ebproof_shift_x:Nn \l_ebproof_a_box { \box_wd:N \l_ebproof_a_box }
+ \hbox_set:Nn \l_ebproof_a_box {
+ \hbox_unpack:N \l_ebproof_a_box
+ $ \tex_left:D . \box_use:N \l_tmpa_box #2 $
+ }
+ \hbox_set:Nn \l_ebproof_a_box
+ { \box_move_down:nn { \l_tmpa_dim } { \box_use:N \l_ebproof_a_box } }
+ \ebproof_push:N \l_ebproof_a_box
+ \group_end:
+}
+
+
+%%% 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.
+
+\ebproof_new_deprecated_statement:nnnn { Alter } { m }
+ { use~\token_to_str:c{rewrite}~instead } { \ebproofrewrite{ #1 \box\treebox } }
+\ebproof_new_deprecated_statement:nnnn { Delims } { }
+ { use~\token_to_str:c{delims}~instead } { \ebproofdelims }
+\ebproof_new_deprecated_statement:nnnn { Ellipsis } { }
+ { use~\token_to_str:c{ellipsis}~instead } { \ebproofellipsis }
+\ebproof_new_deprecated_statement:nnnn { Hypo } { }
+ { use~\token_to_str:c{hypo}~instead } { \ebproofhypo }
+\ebproof_new_deprecated_statement:nnnn { Infer } { }
+ { use~\token_to_str:c{infer}~instead } { \ebproofinfer }
+
%%% Environment interface
-\ebproof@clear
-
-\def\ebproof@begin{%
- \edef\ebproof@start@level{\the\ebproof@level}%
- \setbox1=\vbox\bgroup
- \let\Hypo=\ebproof@hypo
- \let\Infer=\ebproof@infer
- \let\Ellipsis=\ebproof@ellipsis
- \let\Alter=\ebproof@alter
- \let\Delims=\ebproof@delims}
-\def\ebproof@end{%
- \egroup
- \ebproof@pop{X}%
- \ifnum\ebproof@level=\ebproof@start@level\else
- \PackageError{ebproof}{Malformed proof tree}{%
- Some hypotheses were declared but not used in this tree.}%
- \fi
- \ifebproof@center
- \hbox{$\vcenter{\hbox{\box\X@box}}$}%
- \else
- \box\X@box
- \fi
- \global\setbox\ebproof@box@temp=\box1}
-
-\newenvironment{prooftree}[1][]{%
- \pgfqkeys{/ebproof/proof style}{.search also=/ebproof,#1}%
- \leavevmode\ebproof@begin
-}{%
- \ebproof@end}
-
-\newenvironment{prooftree*}[1][]{%
- \center
- \pgfqkeys{/ebproof/proof style}{.search also=/ebproof,#1}%
- \leavevmode\ebproof@begin
-}{%
- \ebproof@end
- \endcenter}
+\ebproof_clear_stack:
+
+\tl_new:N \l_ebproof_start_level_tl
+
+\NewDocumentEnvironment { prooftree } { s O{} } {
+ \keys_set_known:nnN { ebproof / proof~style } { #2 } \l_tmpa_tl
+ \keys_set:nV { ebproof } \l_tmpa_tl
+ \tl_set:Nx \l_ebproof_start_level_tl { \int_use:N \g_ebproof_level_int }
+ \vbox_set:Nw \l_tmpa_box
+ \ebproof_setup_statements:
+} {
+ \vbox_set_end:
+ \ebproof_pop:N \l_ebproof_a_box
+ \int_compare:nNnF { \g_ebproof_level_int } = { \tl_use:N \l_ebproof_start_level_tl } {
+ \PackageError{ebproof}{Malformed~proof~tree}{
+ Some~hypotheses~were~declared~but~not~used~in~this~tree.}
+ }
+ \IfBooleanTF { #1 } {
+ \[ \box_use:N \l_ebproof_a_box \]
+ \ignorespacesafterend
+ } {
+ \hbox_unpack:N \c_empty_box
+ \bool_if:NTF \l_ebproof_center_bool {
+ \hbox:n { $ \tex_vcenter:D { \box_use:N \l_ebproof_a_box } $ }
+ } {
+ \box_use:N \l_ebproof_a_box
+ }
+ }
+}
+
+% A trick for the starred version:
+\cs_new:cpn { prooftree* } { \prooftree* }
+\cs_new:cpn { endprooftree* } { \endprooftree }