prftree (11jan16)

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

3 files changed, 247 insertions, 122 deletions

diff --git a/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf b/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf
index 87e9d490d6a..f92aee2c858 100644
--- a/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf
+++ b/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf
diff --git a/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex b/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex
index b28e254b1d5..9db4c1f9e90 100644
--- a/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex
+++ b/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex
@@ -1,4 +1,6 @@
 \documentclass{amsart}
+\usepackage{color}
+\usepackage{graphics}
 \usepackage[ND,SEQ]{prftree}
 \usepackage{url}
 
@@ -284,9 +286,10 @@ sub-proof basis, as will be done in most examples.\vspace{2ex}
 There are various \TeX{} dimensions that influence how proofs are
 constructed:
 \begin{itemize}
-\item\ \verb|\prflinepad| (default 0.3ex): the space between the
-  bottom line of assumptions and the proof line, and also the space
-  between the proof line and the top of the conclusion;
+\item\ \verb|\prflinepadbefore| (default 0.3ex): the space between the
+  bottom line of assumptions and the proof line
+\item\ \verb|\prflinepadafter| (default 0.3ex): the space between the
+  proof line and the top of the conclusion;
 \item\ \verb|\prflineextra| (default 0.3em): the length which extends
   on the left and on the right the proof line so that it is slightly
   longer than the largest between the conclusion and the list of
@@ -309,7 +312,7 @@ constructed:
 
 For example, 
 \begin{displaymath}
-  \prflinepad=.7ex
+  \prflinepadafter=.7ex
   \prftree[r]{$\supset$I}
   {\prftree[r]{$\supset$I}
     {\prftree[r]{$\supset$E}
@@ -321,7 +324,7 @@ For example,
 \end{displaymath}
 is typeset by
 \begin{verbatim}
-  \prflinepad=.7ex
+  \prflinepadafter=.7ex
   \prftree[r]{$\supset$I}
     {\prftree[r]{$\supset$I}
       {\prftree[r]{$\supset$E}
@@ -496,6 +499,25 @@ sub-proof whose conclusion is $C$, one obtains the more pleasant
     \rightarrow (A \rightarrow C))} 
 \end{displaymath}\vspace{.2ex}
 
+The \verb|Strut| option of the package controls a subtle point about
+spacing around a proof line: assumptions and conclusion are usually
+typeset so that the height and the depth of their box is at least the
+one of \verb|\mathstrut|. In this way, adjacent proofs will have their
+proof lines aligned (well, whenever they don't have huge
+conclusions). But, as signalled by Dominic Hughes, sometimes one wants
+the height and the depth to be the ``real'' ones, especially when
+there are no characters/symbols with a positive depth: this forces the
+perceived space above and below the proof line to be exactly the
+values of \verb|\prflinepadbefore| and \verb|\prflinepadafter|. This
+behaviour can be achieved by calling the package with the \verb|STRUT|
+option. Alternatively, one may use the \verb|\prfSTRUToptionfalse|
+command to locally force this behaviour, and
+\verb|\prfSTRUToptiontrue| to return to the standard one. Similarly,
+the \verb|STRUTlabel| package option, together with the pair of
+commands \verb|\prfSTRUTlabeloptiontrue| and
+\verb|\prfSTRUTlabeloptionfalse|, operate on rule names and rule
+labels.\vspace{2ex}
+
 The rendering of bounded assumptions is modified by
 \verb|\prfboundedstyle|. When $\verb|\prfboundedstyle| = 0$, the
 format of the assumption is $[\mbox{formula}]$, which is the default
@@ -574,12 +596,15 @@ command. This can be modified at will. The package defines it as
 The assumptions, conclusions, labels, and rule names are drawn using
 the following commands, which may be redefined:
 \begin{verbatim}
-  \def\prfConclusionBox#1{\hbox%
-    {$\displaystyle\begingroup#1\endgroup\mathstrut$}}
-  \def\prfAssumptionBox#1{\hbox%
-    {$\displaystyle\begingroup#1\endgroup\mathstrut$}}
-  \def\prfRuleNameBox#1{\hbox{\begingroup#1\endgroup\strut}}
-  \def\prfLabelBox#1{\hbox{\begingroup#1\endgroup\strut}}
+\def\prfConclusionBox#1{%
+  \hbox{$\displaystyle\begingroup#1\endgroup%
+\def\prfAssumptionBox#1{%
+  \hbox{$\displaystyle\begingroup#1\endgroup%
+    \ifprfSTRUToption\mathstrut\fi$}}
+\def\prfRuleNameBox#1{\hbox{\begingroup#1\endgroup%
+    \ifprfSTRUTlabeloption\strut\fi}}
+\def\prfLabelBox#1{\hbox{\begingroup#1\endgroup%
+    \ifprfSTRUTlabeloption\strut\fi}}
 \end{verbatim}
 It is not advisable to change these commands in a radical way, unless
 one understands how the graphical engine works.
@@ -597,7 +622,7 @@ value aside the labelled point of the proof.
 
 For example,
 \begin{displaymath}
-  \begin{prooftree}
+  \begin{prfenv}
     \prftree[r]{$\supset\mathrm{I}_{\prfref<assum:A>}$}
     {\prftree[r]{$\supset\mathrm{I}_{\prfref<assum:not_A>}$}
       {\prftree[r]{$\supset$E}
@@ -606,11 +631,11 @@ For example,
         {\bot}}
       {\neg\neg A}}
     {A \supset \neg\neg A}
-  \end{prooftree}
+  \end{prfenv}
 \end{displaymath}
 is generated by the following code
 \begin{verbatim}
-  \begin{prooftree}
+  \begin{prfenv}
     \prftree[r]{$\supset\mathrm{I}_{\prfref<assum:A>}$}
     {\prftree[r]{$\supset\mathrm{I}_{\prfref<assum:not_A>}$}
       {\prftree[r]{$\supset$E}
@@ -619,17 +644,17 @@ is generated by the following code
         {\bot}}
       {\neg\neg A}}
     {A \supset \neg\neg A}
-  \end{prooftree}
+  \end{prfenv}
 \end{verbatim}
 The labels are \verb|assum:A| and \verb|assum:not_A|, the reference
 values are $1$ and $2$, respectively, and the anchors are these values
 on the discharged assumptions on the top of the proof. The references
 to these labels are the values in the rule names.\vspace{2ex}
 
-The \verb|prooftree| environment delimits the scope of labels: the
-\verb|\end{prooftree}| declaration makes the labels still available
+The \verb|prfenv| environment delimits the scope of labels: the
+\verb|\end{prfenv}| declaration makes the labels still available
 for reference, but numbering of new labels will restart from
-$1$. Enclosing a proof tree in a \verb|prooftree| environment is not
+$1$. Enclosing a proof tree in a \verb|prfenv| environment is not
 mandatory: in such case, labels will be global to the
 document.\vspace{2ex}
 
@@ -687,7 +712,7 @@ For example, the disjunction elimination rule is a perfect way to
 illustrate the reason behind the \textbf{label} option, i.e., the need
 to discharge a pair of assumptions: 
 \begin{displaymath}
-  \begin{prooftree}
+  \begin{prfenv}
     \prfinterspace=1.2em
     \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orE>}$}
     {\prfsummary{\Gamma}{A \vee B}}
@@ -695,7 +720,7 @@ to discharge a pair of assumptions:
         \prfboundedassumption<assum:orE>{A}}{C}}
     {\prfsummary{\Gamma, 
         \prfboundedassumption<[l]assum:orE>{B}}{C}}{C}
-  \end{prooftree}
+  \end{prfenv}
 \end{displaymath}
 \begin{verbatim}
     \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orE>}$}
@@ -713,7 +738,7 @@ may indicate that a label is reused when it should not.
 The same example can be used to show how the other options work:
 \begin{displaymath}
   \begin{array}{@{}ccc@{}}
-    \begin{prooftree}
+    \begin{prfenv}
       \prfsummarystyle=2
       \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEn>}$}
       {\prfsummary{\Gamma}{A \vee B}}
@@ -722,8 +747,8 @@ The same example can be used to show how the other options work:
       {\prfsummary{\Gamma, 
           \prfboundedassumption<[l]assum:orEn>{B}}{C}}
       {C}
-    \end{prooftree} &
-    \begin{prooftree}
+    \end{prfenv} &
+    \begin{prfenv}
       \prfsummarystyle=2
       \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEr>}$}
       {\prfsummary{\Gamma}{A \vee B}}
@@ -732,8 +757,8 @@ The same example can be used to show how the other options work:
       {\prfsummary{\Gamma, 
           \prfboundedassumption<[l]assum:orEr>{B}}{C}}
       {C}
-    \end{prooftree} &
-    \begin{prooftree}
+    \end{prfenv} &
+    \begin{prfenv}
       \prfsummarystyle=2
       \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orER>}$}
       {\prfsummary{\Gamma}{A \vee B}}
@@ -742,8 +767,8 @@ The same example can be used to show how the other options work:
       {\prfsummary{\Gamma, 
           \prfboundedassumption<[l]assum:orER>{B}}{C}}
       {C}
-    \end{prooftree} \\
-    \begin{prooftree}
+    \end{prfenv} \\
+    \begin{prfenv}
       \prfsummarystyle=2
       \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEa>}$}
       {\prfsummary{\Gamma}{A \vee B}}
@@ -752,8 +777,8 @@ The same example can be used to show how the other options work:
       {\prfsummary{\Gamma, 
           \prfboundedassumption<[l]assum:orEa>{B}}{C}}
       {C}
-    \end{prooftree} &
-    \begin{prooftree}
+    \end{prfenv} &
+    \begin{prfenv}
       \prfsummarystyle=2
       \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEA>}$}
       {\prfsummary{\Gamma}{A \vee B}}
@@ -762,8 +787,8 @@ The same example can be used to show how the other options work:
       {\prfsummary{\Gamma, 
           \prfboundedassumption<[l]assum:orEA>{B}}{C}}
       {C}
-    \end{prooftree} &
-    \begin{prooftree}
+    \end{prfenv} &
+    \begin{prfenv}
       \prfsummarystyle=2
       \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEf>}$}
       {\prfsummary{\Gamma}{A \vee B}}
@@ -772,7 +797,7 @@ The same example can be used to show how the other options work:
       {\prfsummary{\Gamma, 
           \prfboundedassumption<[l]assum:orEf>{B}}{C}}
       {C}
-    \end{prooftree}
+    \end{prfenv}
   \end{array}
 \end{displaymath}
 
@@ -780,7 +805,7 @@ Also, as the \verb|\prfboundedstyle| varies, the resulting proof trees
 are: 
 \begin{displaymath}
   \begin{array}{ccc}
-    \begin{prooftree}
+    \begin{prfenv}
       \prfboundedstyle=0
       \prfsummarystyle=4
       \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:AorE>}$}
@@ -790,8 +815,8 @@ are:
       {\prfsummary{\Gamma, 
           \prfboundedassumption<[l]assum:AorE>{B}}{C}}
       {C}
-    \end{prooftree} &
-    \begin{prooftree}
+    \end{prfenv} &
+    \begin{prfenv}
       \prfboundedstyle=1
       \prfsummarystyle=4
       \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:BorE>}$}
@@ -801,8 +826,8 @@ are:
       {\prfsummary{\Gamma, 
           \prfboundedassumption<[l]assum:BorE>{B}}{C}}
       {C}
-    \end{prooftree} &
-    \begin{prooftree}
+    \end{prfenv} &
+    \begin{prfenv}
       \prfboundedstyle=2
       \prfsummarystyle=4
       \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:CorE>}$}
@@ -812,7 +837,7 @@ are:
       {\prfsummary{\Gamma, 
           \prfboundedassumption<[l]assum:CorE>{B}}{C}}
       {C}
-    \end{prooftree}
+    \end{prfenv}
   \end{array}
 \end{displaymath}
 
@@ -821,7 +846,7 @@ generate the assumption values. It contains the last used value, and
 initially, it is set to $0$. By modifying its value, e.g., to
 \verb|\setcounter{prfassumptioncounter}{1}|,
 \begin{displaymath}
-  \begin{prooftree}
+  \begin{prfenv}
     \setcounter{prfassumptioncounter}{1}
     \prfsummarystyle=2
     \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEff>}$}
@@ -831,7 +856,7 @@ initially, it is set to $0$. By modifying its value, e.g., to
     {\prfsummary{\Gamma, 
         \prfboundedassumption<[l]assum:orEff>{B}}{C}}
     {C}
-  \end{prooftree}
+  \end{prfenv}
 \end{displaymath}
 
 A labelled assumption box is graphically constructed by the package
@@ -974,7 +999,7 @@ elimination or disjunction introduction.
 
 For example, the proof
 \begin{displaymath}
-  \begin{prooftree}
+  \begin{prfenv}
     \NDOREL{simp:notA}{\NDLEM{A \vee \neg A}}
     {\NDIMPI{\NDDL{[l]simp:notA}{A}}{\neg\neg A \supset A}}
     {\NDIMPIL{simp:notnotA}
@@ -982,7 +1007,7 @@ For example, the proof
           {\NDDL{simp:notA}{\neg A}}{\bot}}{A}} 
       {\neg\neg A \supset A}}
     {\neg\neg A \supset A}
-  \end{prooftree}
+  \end{prfenv}
 \end{displaymath}
 is typeset in abbreviated form by the following code
 \begin{verbatim}
@@ -996,7 +1021,7 @@ is typeset in abbreviated form by the following code
 \end{verbatim}\vspace{2ex}
 
 Similarly, by loading the package as
-\verb|\usepackage[SEQ]{prooftree.sty}|, the following abbreviations
+\verb|\usepackage[SEQ]{prftree.sty}|, the following abbreviations
 are available, which roughly correspond to the inference rule of
 sequent calculi:
 \begin{itemize}
@@ -1044,7 +1069,7 @@ best.\vspace{2ex}
 
 Consider the proof:
 \begin{displaymath}
-  \begin{prooftree}
+  \begin{prfenv}
     \NDOREL{a:notA}{\NDLEM{A \vee \neg A}}
     {\NDIMPI{\NDDL{a:notA}{A}}{\neg\neg A \supset A}}
     {\NDIMPIL{a:notnotA}
@@ -1052,7 +1077,7 @@ Consider the proof:
           {\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}} 
       {\neg\neg A \supset A}}
     {\neg\neg A \supset A}
-  \end{prooftree}
+  \end{prfenv}
 \end{displaymath}
 the space between the axiom and the sub-proof of the positive case is
 visually much less than the space between the positive and the
@@ -1065,7 +1090,7 @@ negative case closer to the positive one.
 
 The first strategy yields:
 \begin{displaymath}
-  \begin{prooftree}
+  \begin{prfenv}
     \NDOREL{a:notA}{\NDLEM{A \vee \neg A}\hspace{.8em}}
     {\NDIMPI{\NDDL{[l]a:notA}{A}}{\neg\neg A \supset A}}
     {\NDIMPIL{a:notnotA}
@@ -1073,7 +1098,7 @@ The first strategy yields:
           {\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}} 
       {\neg\neg A \supset A}}
     {\neg\neg A \supset A}
-  \end{prooftree}
+  \end{prfenv}
 \end{displaymath}
 and this effect is given by adding an appropriate \verb|\hspace| after
 the axiom, as in
@@ -1091,7 +1116,7 @@ Adding the same space in front of the positive case is equivalent.
 
 The second strategy yields:
 \begin{displaymath}
-  \begin{prooftree}
+  \begin{prfenv}
     \NDOREL{a:notA}{\NDLEM{A \vee \neg A}}
     {\NDIMPI{\NDDL{[l]a:notA}{A}}{\neg\neg A \supset A}}
     {\hspace{-.4em}\NDIMPIL{a:notnotA}
@@ -1099,7 +1124,7 @@ The second strategy yields:
           {\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}} 
       {\neg\neg A \supset A}}
     {\neg\neg A \supset A}
-  \end{prooftree}
+  \end{prfenv}
 \end{displaymath}
 Again, this is obtained by adding a negative \verb|hspace| after the
 positive case, or, equivalently, before the negative one:
@@ -1132,7 +1157,7 @@ align proof trees, as in
 \begin{center}
   \fbox{\prfsummarystyle=1
     \prfsummary{f}{g}{f \wedge g}}\qquad
-  \fbox{$\begin{prooftree}
+  \fbox{$\begin{prfenv}
       \NDOREL{a:notA}{\NDLEM{A \vee \neg A}}
       {\NDIMPI{\NDDL{[l]a:notA}{A}}{\neg\neg A \supset A}}
       {\hspace{-.4em}\NDIMPIL{a:notnotA}
@@ -1140,7 +1165,7 @@ align proof trees, as in
             {\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}} 
         {\neg\neg A \supset A}}
       {\neg\neg A \supset A}
-    \end{prooftree}$}
+    \end{prfenv}$}
 \end{center}
 since this is the natural way to put proofs side by side:
 \begin{verbatim}
@@ -1533,6 +1558,85 @@ A deduction in a sequent calculus:
     \rightarrow B) \rightarrow (A \rightarrow C))}
 \end{displaymath}
 
+Proof tree can be coloured, as kindly pointed out by Dominic Hughes:
+\begin{displaymath}
+  \begin{prfenv}
+    \color{green}\NDIMPIL{ex6:1}
+    {\NDANDI
+      {\color{red}\NDNOTIL{ex6:2}
+        {\NDNOTE
+          {\NDDL{ex6:1}{\neg (A \vee B)}}
+          {\NDORIL
+            {\NDDL{ex6:2}{A}}
+            {A \vee B}}
+          {\bot}}
+        {\neg A}}
+      {\color{blue}\NDNOTIL{ex6:3}
+        {\NDNOTE
+          {\NDDL{[l]ex6:1}{\neg (A \vee B)}}
+          {\NDORIR
+            {\NDDL{ex6:3}{B}}
+            {A \vee B}}
+          {\bot}}
+        {\neg B}}
+      {\neg A \wedge \neg B}}
+    {\neg (A \vee B) \supset \neg A \wedge \neg B}
+  \end{prfenv}
+\end{displaymath}\vspace{.2ex}
+
+Also. all the standard box manipulation commands can be freely applied.
+The following examples are not significant for doing mathematics, but
+the mechanics behind can be occasionally useful, for example, to
+shrink a large proof to fit the page length:
+\begin{displaymath}
+  \rotatebox{15}{\begin{prfenv}
+    \NDIMPIL{ex5:1}
+    {\NDANDI
+      {\NDNOTIL{ex5:2}
+        {\NDNOTE
+          {\NDDL{ex5:1}{\neg (A \vee B)}}
+          {\NDORIL
+            {\NDDL{ex5:2}{A}}
+            {A \vee B}}
+          {\bot}}
+        {\neg A}}
+      {\NDNOTIL{ex5:3}
+        {\NDNOTE
+          {\NDDL{[l]ex5:1}{\neg (A \vee B)}}
+          {\NDORIR
+            {\NDDL{ex5:3}{B}}
+            {A \vee B}}
+          {\bot}}
+        {\neg B}}
+      {\neg A \wedge \neg B}}
+    {\neg (A \vee B) \supset \neg A \wedge \neg B}
+  \end{prfenv}}
+\end{displaymath}
+\begin{displaymath}
+  \begin{prfenv}
+    \NDIMPIL{ex7:1}
+    {\NDANDI
+      {\reflectbox{\NDNOTIL{ex7:2}
+          {\NDNOTE
+            {\NDDL{ex7:1}{\neg (A \vee B)}}
+            {\NDORIL
+              {\NDDL{ex7:2}{A}}
+              {A \vee B}}
+            {\bot}}
+          {\neg A}}}
+      {\resizebox{20em}{!}{\NDNOTIL{ex7:3}
+          {\NDNOTE
+            {\NDDL{[l]ex7:1}{\neg (A \vee B)}}
+            {\scalebox{.7}[1]{\NDORIR
+              {\NDDL{ex7:3}{B}}
+              {A \vee B}}}
+            {\bot}}
+          {\neg B}}}
+      {\neg A \wedge \neg B}}
+    {\neg (A \vee B) \supset \neg A \wedge \neg B}
+  \end{prfenv}
+\end{displaymath}
+
 % -------------------------------------
 \clearpage
 \section{Internals}\label{sec:internals}
@@ -1645,7 +1749,8 @@ occurrence of a reference, which can be resolved.
 Most difficulties in the implementation of references lie in the way
 to construct the boxes to be used in the proof tree. But, the tricky
 part is the interaction with the \LaTeX{} and \TeX{} kernel for error
-reporting.
+reporting. A small hack has been introduced to force recompilation
+when the references in a proof change.
 
 % -------------------------------------
 \clearpage
@@ -1673,7 +1778,6 @@ difficulty is how to represent skylines and how to store them, since
 \TeX{} provides no abstract data structures. Hence, the implementation
 of this feature has been postponed to a remote future, or to the will
 of a real \TeX{} magician.
-
 \vfill
 
 \end{document}
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
 
 % -------------------------------------------------------------------