summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/tex/latex/ebproof
diff options
context:
space:
mode:
authorKarl Berry <karl@freefriends.org>2015-03-22 21:22:17 +0000
committerKarl Berry <karl@freefriends.org>2015-03-22 21:22:17 +0000
commit03b72ee35aae655a0458e281a82a09efbcec318f (patch)
tree5b1b1747757015c9a41bcc189e730ad59673a364 /Master/texmf-dist/tex/latex/ebproof
parente764d74939c2f6a637c75a3c5c87068f275d2678 (diff)
ebproof (22mar15)
git-svn-id: svn://tug.org/texlive/trunk@36595 c570f23f-e606-0410-a88d-b1316a301751
Diffstat (limited to 'Master/texmf-dist/tex/latex/ebproof')
-rw-r--r--Master/texmf-dist/tex/latex/ebproof/ebproof.sty99
1 files changed, 57 insertions, 42 deletions
diff --git a/Master/texmf-dist/tex/latex/ebproof/ebproof.sty b/Master/texmf-dist/tex/latex/ebproof/ebproof.sty
index e8018884a29..33a3f73b916 100644
--- a/Master/texmf-dist/tex/latex/ebproof/ebproof.sty
+++ b/Master/texmf-dist/tex/latex/ebproof/ebproof.sty
@@ -1,29 +1,34 @@
-% This package contains macros for typesetting proof trees.
+% The ebproof package - Formal proofs in the style of sequent calculus
+
+%% ebproof.sty
+%% Copyright 2015 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.
+% The latest version of this license is in
+% http://www.latex-project.org/lppl.txt
+% and version 1.3 or later is part of all distributions of LaTeX
+% version 2005/12/01 or later.
+%
+% This work has the LPPL maintenance status `maintained'.
+%
+% The Current Maintainer of this work is Emmanuel Beffara.
+%
+% This work consists of the files ebproof.sty and ebproof.tex.
\NeedsTeXFormat{LaTeX2e}
-\ProvidesPackage{ebproof}[2015/02/03 v1.0 EB's proof trees]
+\ProvidesPackage{ebproof}[2015/03/13 v1.1 EB's proof trees]
% The |pgfkeys| package is used for the parameters in proof construction.
-% The |ifthen| package is used for some tests.
\RequirePackage{pgfkeys}
-\RequirePackage{ifthen}
%%% Registers and internal parameters
-\newbox\ebproof@leftbox
-\newbox\ebproof@rightbox
\newif\ifebproof@updown \ebproof@updownfalse
\newif\ifebproof@center \ebproof@centertrue
-\def\ebproof@template#1{$#1$}
-\def\ebproof@lefttemplate#1{$#1\mathrel{}$}
-\def\ebproof@righttemplate#1{$\mathrel{}#1$}
-\def\ebproof@leftlabeltemplate#1{#1}
-\def\ebproof@rightlabeltemplate#1{#1}
-\def\ebproof@setleftlabel{\setbox\ebproof@leftbox=\box\voidb@x}
-\def\ebproof@setrightlabel{\setbox\ebproof@rightbox=\box\voidb@x}
-
%%% Parameters
\def\ebproofset#1{\pgfqkeys{/ebproof}{#1}}
@@ -52,20 +57,16 @@ rule code/.initial=,
%
% templates
%
-template/.code={\def\ebproof@template##1{#1}},
-left template/.code={\def\ebproof@lefttemplate##1{#1}},
-right template/.code={\def\ebproof@righttemplate##1{#1}},
+template/.initial=$\inserttext$,
+left template/.initial=$\inserttext\mathrel{}$,
+right template/.initial=$\mathrel{}\inserttext$,
%
% labels
%
-left label/.code={%
- \def\ebproof@setleftlabel{%
- \setbox\ebproof@leftbox=\hbox{\ebproof@leftlabeltemplate{#1}}}},
-right label/.code={%
- \def\ebproof@setrightlabel{%
- \setbox\ebproof@rightbox=\hbox{\ebproof@rightlabeltemplate{#1}}}},
-left label template/.code={\def\ebproof@leftlabeltemplate##1{#1}},
-right label template/.code={\def\ebproof@rightlabeltemplate##1{#1}},
+left label/.initial=,
+right label/.initial=,
+left label template/.initial=\inserttext,
+right label template/.initial=\inserttext,
label separation/.initial=0.5em,
}
@@ -288,8 +289,6 @@ simple % use the 'simple' rule style by default
\def\ebproof@joinv{%
\begingroup
- \ebproof@setleftlabel
- \ebproof@setrightlabel
\ebproof@pop{A}%
\ebproof@pop{B}%
%
@@ -361,9 +360,16 @@ simple % use the 'simple' rule style by default
\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\ebproof@leftbox\else
- \tmp=\wd\ebproof@leftbox
+ \ifvoid\LEFT\else
+ \tmp=\wd\LEFT
\advance\tmp\pgfkeysvalueof{/ebproof/label separation}
\ifdim\tmp>\R@shift
\advance\tmp-\R@shift
@@ -383,14 +389,14 @@ simple % use the 'simple' rule style by default
\advance\R@raise-\ht\RC@box
% Make the complete rule box
\setbox\RC@box=\hbox{%
- \ifvoid\ebproof@leftbox\else
- \copy\ebproof@leftbox
+ \ifvoid\LEFT\else
+ \box\LEFT
\kern\pgfkeysvalueof{/ebproof/label separation}
\fi
\box\RC@box
- \ifvoid\ebproof@rightbox\else
+ \ifvoid\RIGHT\else
\kern\pgfkeysvalueof{/ebproof/label separation}
- \copy\ebproof@rightbox
+ \box\RIGHT
\fi}
% Adapt the dimensions on the right if the total rule width is too large
\tmp=\wd\RC@box
@@ -462,11 +468,17 @@ simple % use the 'simple' rule style by default
% contains a |&| character
\def\ebproof@hypo@parse#1&#2&#3\ebproof@hypo@stop{
- \ifthenelse{\equal{#3}{}}%
- {\ebproof@pushsimple{\ebproof@template{#1}}}%
- {\ebproof@pushsplit
- {\ebproof@lefttemplate{#1}}%
- {\ebproof@righttemplate{#2}}}}
+ {\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}}
@@ -476,12 +488,15 @@ simple % use the 'simple' rule style by default
\def\ebproof@infer{%
\@ifnextchar[{\ebproof@infer@}{\ebproof@infer@[]}}
\def\ebproof@infer@[#1]#2{%
- \@ifnextchar[{\ebproof@infer@@{#1}{#2}}{\ebproof@infer@@{#1}{#2}[]}}
-\def\ebproof@infer@@#1#2[#3]#4{{%
+ \@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{#4}%
- \ifthenelse{\equal{#3}{}}{}{\ebproofset{right label={#3}}}%
+ \ebproof@hypo{#3}%
\ebproof@joinv}}
% Ellipsis with vertical dots