diff options
Diffstat (limited to 'Master')
| -rw-r--r-- | Master/texmf-dist/doc/latex/ebproof/README | 22 | ||||
| -rw-r--r-- | Master/texmf-dist/doc/latex/ebproof/ebproof.pdf | bin | 196387 -> 198863 bytes | |||
| -rw-r--r-- | Master/texmf-dist/doc/latex/ebproof/ebproof.tex | 64 | ||||
| -rw-r--r-- | Master/texmf-dist/tex/latex/ebproof/ebproof.sty | 99 |
4 files changed, 128 insertions, 57 deletions
diff --git a/Master/texmf-dist/doc/latex/ebproof/README b/Master/texmf-dist/doc/latex/ebproof/README index a64bac6f41f..e3893221e98 100644 --- a/Master/texmf-dist/doc/latex/ebproof/README +++ b/Master/texmf-dist/doc/latex/ebproof/README @@ -1,3 +1,5 @@ +== Presentation == + The ebproofs package provides commands to typeset proof trees, in the style of sequent calculus and related systems. The commands allow for writing inferences with any number of premisses and alignment of successive formulas @@ -12,5 +14,21 @@ The distribution includes the following files: The package requires pgfkeys (from TikZ/PGF) for the option system. -This package is written by Emmanuel Beffara <manu@beffara.org> -It is subject to the LaTeX Project Public License. + +== License == + +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. diff --git a/Master/texmf-dist/doc/latex/ebproof/ebproof.pdf b/Master/texmf-dist/doc/latex/ebproof/ebproof.pdf Binary files differindex e58d9616168..f273cfa8b67 100644 --- a/Master/texmf-dist/doc/latex/ebproof/ebproof.pdf +++ b/Master/texmf-dist/doc/latex/ebproof/ebproof.pdf diff --git a/Master/texmf-dist/doc/latex/ebproof/ebproof.tex b/Master/texmf-dist/doc/latex/ebproof/ebproof.tex index acb05d56759..194a02827b0 100644 --- a/Master/texmf-dist/doc/latex/ebproof/ebproof.tex +++ b/Master/texmf-dist/doc/latex/ebproof/ebproof.tex @@ -1,10 +1,27 @@ +%% 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. + \documentclass{article} \DeclareRobustCommand\package[1]{\texttt{#1}} \title{The \package{ebproof} package} \author{Emmanuel Beffara \\ \url{manu@beffara.org}} -\date{Version 1.0 \\ February 3, 2015} +\date{Version 1.1 \\ March 13, 2015} \usepackage{amssymb} \usepackage{color} @@ -440,24 +457,24 @@ following command: \subsection{Format of conclusions} \begin{csdoc}{% - \opt{template=}\meta{macro} \\ - \opt{left template=}\meta{macro} \\ - \opt{right template=}\meta{macro}} + \opt{template=}\meta{code} \\ + \opt{left template=}\meta{code} \\ + \opt{right template=}\meta{code}} Defines how conclusions are formatted. - The macros are arbitrary \TeX\ code, composed in horizontal mode, with the - macro argument \verb|#1| standing for the actual text passed to the + The code is arbitrary \TeX\ code, composed in horizontal mode. + The macro \cs{inserttext} can be used inside the actual text passed to the \cs{Hypo} and \cs{Infer} statements. The \opt{template} value is used for conclusions with no alignment mark. The \opt{left template} and \opt{right template} values are used on the left and right side of the alignment mark when it is present. - The default value for \opt{template} is simply \verb|$#1$|, so that + The default value for \opt{template} is simply \verb|$\inserttext$|, so that conclusions are set in math mode. The default values for \opt{left template} and \opt{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. \begin{example}{gobble=4} - \begin{prooftree}[template=(\textbf{#1})] + \begin{prooftree}[template=(\textbf\inserttext)] \Hypo{ foo } \Hypo{ bar } \Infer1{ baz } @@ -477,11 +494,14 @@ following command: the \env{right label} option with the value of that argument. \end{csdoc} \begin{csdoc}{% - \opt{left label template=}\meta{macro} \\ - \opt{right label template=}\meta{macro}} - These macros are used to typeset the text of labels on the left and right of - inference lines. - The default values are \verb|#1| so that labels are set in plain text mode. + \opt{left label template=}\meta{code} \\ + \opt{right label template=}\meta{code}} + Defines how rule labels are formatted. + The code is arbitrary \TeX\ code, composed in horizontal mode. + The macro \cs{inserttext} can be used to insert the actual label text, as + defined by the options above. + The default values are simply \cs{inserttext} so that labels are set in + plain text mode. \end{csdoc} \begin{csdoc}{\opt{label separation=}\meta{dimension}} @@ -490,4 +510,22 @@ following command: \end{csdoc} +\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}. + \end{document} 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\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 |