prftree (11jan16)

git-svn-id: svn://tug.org/texlive/trunk@39356 c570f23f-e606-0410-a88d-b1316a301751

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
 
 % -------------------------------------------------------------------