diff options
Diffstat (limited to 'Master/texmf-dist/tex/latex/prftree')
| -rw-r--r-- | Master/texmf-dist/tex/latex/prftree/prftree.sty | 159 |
1 files changed, 90 insertions, 69 deletions
diff --git a/Master/texmf-dist/tex/latex/prftree/prftree.sty b/Master/texmf-dist/tex/latex/prftree/prftree.sty index 2bec5c8f07a..425c1493d71 100644 --- a/Master/texmf-dist/tex/latex/prftree/prftree.sty +++ b/Master/texmf-dist/tex/latex/prftree/prftree.sty @@ -1,7 +1,7 @@ % % prftree.sty -% by Marco Benini - 31st October 2015 -% v1.2 +% by Marco Benini - 11th January 2016 +% v1.4 % % A package to typeset natural deduction proofs, or sequent proofs, or % tableau proofs @@ -10,16 +10,20 @@ % \NeedsTeXFormat{LaTeX2e} -\ProvidesPackage{prftree}[2015/10/31 Natural Deduction Proofs] +\ProvidesPackage{prftree}[2016/01/11 Natural Deduction Proofs] % Package options: deactivated by default \newif\ifprf@NDOption\prf@NDOptionfalse \newif\ifprf@SEQOption\prf@SEQOptionfalse \newif\ifprfIMPOption\prfIMPOptionfalse +\newif\ifprfSTRUToption\prfSTRUToptiontrue +\newif\ifprfSTRUTlabeloption\prfSTRUTlabeloptiontrue \DeclareOption{ND}{\prf@NDOptiontrue} \DeclareOption{SEQ}{\prf@SEQOptiontrue} \DeclareOption{IMP}{\prfIMPOptiontrue} +\DeclareOption{Strut}{\prfSTRUToptionfalse} +\DeclareOption{StrutLabel}{\prfSTRUTlabeloptionfalse} \ProcessOptions\relax %-------------------------------------------------------------------- @@ -121,10 +125,13 @@ % future version of the package. %-------------------------------------------------------------------- -% \prflinepad default 0.3ex -% the space between the baseline of assumptions and the proof line and -% also the space between the proof line and the top of the conclusion -\newdimen\prflinepad\prflinepad.3ex +% \prflinepadbefore default 0.3ex +% the space between the bottom of assumptions and the proof line +\newdimen\prflinepadbefore\prflinepadbefore.3ex + +% \prflinepadafter default 0.3ex +% the space between the proof line and the top of the conclusion +\newdimen\prflinepadafter\prflinepadafter.3ex % \prflineextra default 0.3em % the length which extends on the left and on the right the proof line @@ -181,20 +188,24 @@ % \prfConclusionBox % the command to draw the conclusion box \def\prfConclusionBox#1{% - \hbox{$\displaystyle\begingroup#1\endgroup\mathstrut$}} + \hbox{$\displaystyle\begingroup#1\endgroup% + \ifprfSTRUToption\mathstrut\fi$}} % \prfAssumptionBox % the command to draw the assumption box \def\prfAssumptionBox#1{% - \hbox{$\displaystyle\begingroup#1\endgroup\mathstrut$}} + \hbox{$\displaystyle\begingroup#1\endgroup% + \ifprfSTRUToption\mathstrut\fi$}} % \prfRuleNameBox % the command to draw the rule name box. -\def\prfRuleNameBox#1{\hbox{\begingroup#1\endgroup\strut}} +\def\prfRuleNameBox#1{\hbox{\begingroup#1\endgroup% + \ifprfSTRUTlabeloption\strut\fi}} % \prfLabelBox % the command to draw the label box. -\def\prfLabelBox#1{\hbox{\begingroup#1\endgroup\strut}} +\def\prfLabelBox#1{\hbox{\begingroup#1\endgroup% + \ifprfSTRUTlabeloption\strut\fi}} % \prfdiscargedassumption % the command to draw a discharged assumption in a custom way. @@ -326,9 +337,9 @@ \newif\ifprf@lbl@fnsymbol\prf@lbl@fnsymbolfalse \newif\ifprf@lbl@label\prf@lbl@labelfalse -% The prooftree environment is used to define the scope of the +% The prftree environment is used to define the scope of the % assumption references -\newenvironment{prooftree}% +\newenvironment{prfenv}% {\setcounter{prfassumptioncounter}{0}}% {\setcounter{prfassumptioncounter}{0}} @@ -336,15 +347,23 @@ \def\ifprf@undefref<#1>{% \expandafter\ifx\csname prf@ref@@#1\endcsname\relax} +% Test whether a reference has never been referenced before +\def\ifprf@unrefref<#1>{% + \expandafter\ifx\csname prf@refref@@#1\endcsname\relax} + % Test whether a reference has been written in the .aux file \def\ifprf@unwrittenref<#1>{% \expandafter\ifx\csname prf@w@ref@#1\endcsname\relax} % Write a reference +\newif\ifprf@refhack\prf@refhacktrue \protected\def\prfref<#1>{% \ifprf@undefref<#1>\relax\mbox{??}% - \PackageWarningNoLine{prftree}{Undefined reference <#1>}\relax% - \else\csname prf@ref@@#1\endcsname\relax\fi\relax} + \ifprf@refhack\label{prf@ref@hack}% to force recompilation + \global\prf@refhackfalse\fi% + \PackageWarningNoLine{prftree}{Undefined reference <#1>}% + \expandafter\gdef\csname prf@ref@@#1\endcsname{\mbox{??}}\else% + \csname prf@ref@@#1\endcsname\fi\relax} % Create the anchor from what stored in the .aux file \def\prfauxlabel#1#2{% @@ -682,7 +701,9 @@ % #1 the line options % #2 the rule name \def\prf@@NNtree#1#2{% - \edef\prf@choice{\ifprf@label{#1}{#2}\else{#1}{#2}{}\fi}% + \def\prf@hackpar{#2}% + \edef\prf@choice{\ifprf@label{#1}{\noexpand\prf@hackpar}\else% + {#1}{\noexpand\prf@hackpar}{}\fi}% \expandafter\prf@tree\prf@choice} % We collect the first assumption, if any, or the conclusion otherwise @@ -735,6 +756,7 @@ % #6 the list of assumptions %-------------------------------------------------------------------- +\newbox\prf@@@@proofbox \def\prf@draw#1#2#3#4#5#6{% % We construct the boxes which will constitute the proof \ifprf@first\prf@push{1}\else\prf@push{0}\fi% @@ -878,7 +900,6 @@ % the centre of the rule name and the rule box gets attached to the % proof line box. \prf@linedp\z@% - \ifprf@noline\setbox\prf@fancybox\hbox to2\prf@linewd{}\fi% \ifprf@rule\advance\prf@linedp.5\ht\prf@fancybox% \advance\prf@linedp-.5\ht\prf@rulenamebox% \advance\prf@linedp.5\dp\prf@rulenamebox% @@ -904,8 +925,8 @@ \hbox{\hskip\prf@temp\raise\dp\prf@linebox\box\prf@linebox}% % We need to calculate the distance between the assumptions and the % proofline: if there are no assumptions, it is zero; if there are - % assumptions but no rule name, it is \prflinepad; otherwise it is - % \linepad plus half of the "real" line's height + % assumptions but no rule name, it is \prflinepadbefore; otherwise + % it is \linepadbefore plus half of the "real" line's height \prf@tmp\z@% \ifprf@assum% \ifprf@rule\prf@tmp-.5\ht\prf@linebox% @@ -915,17 +936,17 @@ \prf@tmp-.5\ht\prf@linebox% \advance\prf@tmp.5\ht\prf@fancybox% \advance\prf@tmp.5\dp\prf@fancybox\fi\fi% - \advance\prf@tmp\prflinepad% + \advance\prf@tmp\prflinepadbefore% \setbox\prf@assumptionsbox% \vbox{\box\prf@assumptionsbox\nointerlineskip\vskip\prf@tmp}\fi% % We need to calculate the distance between the proofline and the % conclusion: it is slightly complex to explain... try to draw the % whole thing to make it clear!! - \prf@temp\prflinepad% + \prf@temp\prflinepadafter% \ifprf@noline% \ifprf@assum% - \advance\prf@temp\prfemptylinethickness\fi% - \advance\prf@temp-\prflinepad\fi% + \advance\prf@temp\prfemptylinethickness\else% + \advance\prf@temp-\prflinepadafter\fi\fi% \ifprf@rule% \advance\prf@temp-.5\ht\prf@linebox% \advance\prf@temp.5\ht\prf@fancybox% @@ -968,61 +989,61 @@ \def\NDDL#1{\prfboundedassumption<#1>} \def\NDP{\prftree} \def\NDANDI{\prftree[by]{$\scriptstyle\mathord{\wedge}% - \noexpand\textup{I}$}} + \textup{I}$}} \def\NDANDEL{\prftree[by]{$\scriptstyle\mathord{\wedge}% - \noexpand\textup{E}_1$}} + \textup{E}_1$}} \def\NDANDER{\prftree[by]{$\scriptstyle\mathord{\wedge}% - \noexpand\textup{E}_2$}} + \textup{E}_2$}} \def\NDANDE{\prftree[by]{$\scriptstyle\mathord{\wedge}% - \noexpand\textup{E}$}} + \textup{E}$}} \def\NDORIL{\prftree[by]{$\scriptstyle\mathord{\vee}% - \noexpand\textup{I}_1$}} + \textup{I}_1$}} \def\NDORIR{\prftree[by]{$\scriptstyle\mathord{\vee}% - \noexpand\textup{I}_2$}} + \textup{I}_2$}} \def\NDORI{\prftree[by]{$\scriptstyle\mathord{\vee}% - \noexpand\textup{I}$}} + \textup{I}$}} \def\NDORE{\prftree[by]{$\scriptstyle\mathord{\vee}% - \noexpand\textup{E}$}} + \textup{E}$}} \def\NDOREL#1{\prftree[by]{$\scriptstyle{\vee}% - {\noexpand\textup{E}}^{\noexpand\prfref<#1>}$}} + {\textup{E}}^{\prfref<#1>}$}} \ifprfIMPOption \def\NDIMPI{\prftree[by]{$\scriptstyle\mathord{\supset}% - \noexpand\textup{I}$}} + \textup{I}$}} \def\NDIMPE{\prftree[by]{$\scriptstyle\mathord{\supset}% - \noexpand\textup{E}$}} + \textup{E}$}} \def\NDIMPIL#1{\prftree[by]{$\scriptstyle\mathord{\supset}% - \noexpand\textup{I}^{\noexpand\prfref<#1>}$}} + \textup{I}^{\prfref<#1>}$}} \else \def\NDIMPI{\prftree[by]{$\scriptstyle\mathord{\rightarrow}% - \noexpand\textup{I}$}} + \textup{I}$}} \def\NDIMPE{\prftree[by]{$\scriptstyle\mathord{\rightarrow}% - \noexpand\textup{E}$}} + \textup{E}$}} \def\NDIMPIL#1{% \prftree[by]{$\scriptstyle\mathord{\rightarrow}% - \noexpand\textup{I}^{\noexpand\prfref<#1>}$}}\fi + \textup{I}^{\prfref<#1>}$}}\fi \def\NDNOTI{\prftree[by]{$\scriptstyle\mathord{\neg}% - \noexpand\textup{I}$}} + \textup{I}$}} \def\NDNOTIL#1{\prftree[by]{$\scriptstyle{\neg}% - \noexpand\textup{I}^{\noexpand\prfref<#1>}$}} + \textup{I}^{\prfref<#1>}$}} \def\NDNOTE{\prftree[by]{$\scriptstyle\mathord{\neg}% - \noexpand\textup{E}$}} + \textup{E}$}} \def\NDALLI{\prftree[by]{$\scriptstyle\mathord{\forall}% - \noexpand\textup{I}$}} + \textup{I}$}} \def\NDALLE{\prftree[by]{$\scriptstyle\mathord{\forall}% - \noexpand\textup{E}$}} + \textup{E}$}} \def\NDEXI{\prftree[by]{$\scriptstyle\mathord{\exists}% - \noexpand\textup{I}$}} + \textup{I}$}} \def\NDEXE{\prftree[by]{$\scriptstyle\mathord{\exists}% - \noexpand\textup{E}$}} + \textup{E}$}} \def\NDEXEL#1{% \prftree[by]{$\scriptstyle\mathord{\exists}% - \noexpand\textup{E}^{\noexpand\prfref<#1>}$}} + \textup{E}^{\prfref<#1>}$}} \def\NDTI{\prftree[by]{$\scriptstyle\mathord{\top}% - \noexpand\textup{I}$}} + \textup{I}$}} \def\NDFE{\prftree[by]{$\scriptstyle\mathord{\bot}% - \noexpand\textup{E}$}} - \def\NDLEM{\prftree[by]{$\scriptstyle\noexpand\textup{lem}$}} - \def\NDAX{\prftree[by]{$\scriptstyle\noexpand\textup{ax}$}} + \textup{E}$}} + \def\NDLEM{\prftree[by]{$\scriptstyle\textup{lem}$}} + \def\NDAX{\prftree[by]{$\scriptstyle\textup{ax}$}} \fi % ------------------------------------------------------------------- @@ -1035,40 +1056,40 @@ \def\SEQA{\prfassumption} \def\SEQD{\prfboundedassumption} \def\SEQP{\prftree} - \def\SEQAX{\prftree[by]{$\scriptstyle\noexpand\textup{Ax}$}} - \def\SEQLF{\prftree[by]{$\scriptstyle\noexpand\textup{L}\bot$}} - \def\SEQLW{\prftree[by]{$\scriptstyle\noexpand\textup{LW}$}} - \def\SEQRW{\prftree[by]{$\scriptstyle\noexpand\textup{RW}$}} - \def\SEQLC{\prftree[by]{$\scriptstyle\noexpand\textup{LC}$}} - \def\SEQRC{\prftree[by]{$\scriptstyle\noexpand\textup{RC}$}} - \def\SEQLAND{\prftree[by]{$\scriptstyle\noexpand\textup{L}% + \def\SEQAX{\prftree[by]{$\scriptstyle\textup{Ax}$}} + \def\SEQLF{\prftree[by]{$\scriptstyle\textup{L}\bot$}} + \def\SEQLW{\prftree[by]{$\scriptstyle\textup{LW}$}} + \def\SEQRW{\prftree[by]{$\scriptstyle\textup{RW}$}} + \def\SEQLC{\prftree[by]{$\scriptstyle\textup{LC}$}} + \def\SEQRC{\prftree[by]{$\scriptstyle\textup{RC}$}} + \def\SEQLAND{\prftree[by]{$\scriptstyle\textup{L}% \mathord{\wedge}$}} - \def\SEQRAND{\prftree[by]{$\scriptstyle\noexpand\textup{R}% + \def\SEQRAND{\prftree[by]{$\scriptstyle\textup{R}% \mathord{\wedge}$}} - \def\SEQLOR{\prftree[by]{$\scriptstyle\noexpand\textup{L}% + \def\SEQLOR{\prftree[by]{$\scriptstyle\textup{L}% \mathord{\vee}$}} - \def\SEQROR{\prftree[by]{$\scriptstyle\noexpand\textup{R}% + \def\SEQROR{\prftree[by]{$\scriptstyle\textup{R}% \mathord{\vee}$}} \ifprfIMPOption - \def\SEQLIMP{\prftree[by]{$\scriptstyle\noexpand\textup{L}% + \def\SEQLIMP{\prftree[by]{$\scriptstyle\textup{L}% \mathord{\supset}$}} - \def\SEQRIMP{\prftree[by]{$\scriptstyle\noexpand\textup{R}% + \def\SEQRIMP{\prftree[by]{$\scriptstyle\textup{R}% \mathord{\supset}$}} \else - \def\SEQLIMP{\prftree[by]{$\scriptstyle\noexpand\textup{L}% + \def\SEQLIMP{\prftree[by]{$\scriptstyle\textup{L}% \mathord{\rightarrow}$}} - \def\SEQRIMP{\prftree[by]{$\scriptstyle\noexpand\textup{R}% + \def\SEQRIMP{\prftree[by]{$\scriptstyle\textup{R}% \mathord{\rightarrow}$}} \fi - \def\SEQLALL{\prftree[by]{$\scriptstyle\noexpand\textup{L}% + \def\SEQLALL{\prftree[by]{$\scriptstyle\textup{L}% \mathord{\forall}$}} - \def\SEQRALL{\prftree[by]{$\scriptstyle\noexpand\textup{R}% + \def\SEQRALL{\prftree[by]{$\scriptstyle\textup{R}% \mathord{\forall}$}} - \def\SEQLEX{\prftree[by]{$\scriptstyle\noexpand\textup{L}% + \def\SEQLEX{\prftree[by]{$\scriptstyle\textup{L}% \mathord{\exists}$}} - \def\SEQREX{\prftree[by]{$\scriptstyle\noexpand\textup{R}% + \def\SEQREX{\prftree[by]{$\scriptstyle\textup{R}% \mathord{\exists}$}} - \def\SEQCUT{\prftree[by]{$\scriptstyle\noexpand\textup{Cut}$}} + \def\SEQCUT{\prftree[by]{$\scriptstyle\textup{Cut}$}} \fi % ------------------------------------------------------------------- |