texlive[41985] Master/texmf-dist: prftree (3sep16)

commits+karl at tug.org commits+karl at tug.org
Sat Sep 3 23:36:10 CEST 2016

Revision: 41985
Author:   karl
Date:     2016-09-03 23:36:10 +0200 (Sat, 03 Sep 2016)
Log Message:
prftree (3sep16)

Modified Paths:

Modified: trunk/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf
(Binary files differ)

Modified: trunk/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex
--- trunk/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex	2016-09-03 21:35:58 UTC (rev 41984)
+++ trunk/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex	2016-09-03 21:36:10 UTC (rev 41985)
@@ -115,11 +115,13 @@
 assumption may contain a proof tree, which is typeset independently:
 the order allows to use indentation to help reading the source. The
 conclusion is mandatory, and it is supposed to be a
-formula. Assumptions and the conclusion are typeset in a display style
-math environment. Options control the way the proof is generated: in
-the example, the \verb|r| option has been used to signal that the
-first argument of \verb|\prftree| is the name of the inference rule.
+Assumptions and the conclusion are typeset in a display style math
+environment. Options control the way the proof is generated: in the
+example, the \verb|r| option has been used to signal that the first
+argument of \verb|\prftree| is the name of the inference rule.  
 The available options are:
 \item\ [\textbf{r}], [\textbf{rule}], [\textbf{by rule}],
@@ -294,7 +296,7 @@
   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
   (direct) assumptions;
-\item\ \verb|\prflinethickness| (default 0.2pt): the thickness of the
+\item\ \verb|\prflinethickness| (default 0.12ex): the thickness of the
   proof line;
 \item\ \verb|\prfemptylinethickness| (default 4 times the line
   thickness): in the rare case when the line is empty, but there are
@@ -304,15 +306,15 @@
   proof line and the rule name; 
 \item\ \verb|\prflabelskip| (default 0.2em): the space between the
   proof label and the proof line; 
-\item\ \verb|\prfinterspace| (default .6em): the space between two
+\item\ \verb|\prfinterspace| (default .8em): the space between two
   subsequent assumptions in the assumption list;
-\item\ \verb|\prfdoublelineinterspace| (default 1.2pt): the space
+\item\ \verb|\prfdoublelineinterspace| (default 0.06ex): the space
   between the two lines of a double line.
 For example, 
-  \prflinepadafter=.7ex
+  \prflinepadafter=0ex
@@ -324,7 +326,7 @@
 is typeset by
-  \prflinepadafter=.7ex
+  \prflinepadafter=0ex
@@ -704,6 +706,7 @@
   defined. This is used to generate a labelled assumption sharing the
   label with another one, which declares the value and the format.
 Except for \textbf{l} and \textbf{label}, all the options are used to
 format the anchor following the standard \LaTeX{} way available for
 counters. No multiple options are allowed.
@@ -737,8 +740,10 @@
 The same example can be used to show how the other options work:
+  \renewcommand{\arraystretch}{6}
+      \prfinterspace=.6em
       {\prfsummary{\Gamma}{A \vee B}}
@@ -749,6 +754,7 @@
     \end{prfenv} &
+      \prfinterspace=.6em
       {\prfsummary{\Gamma}{A \vee B}}
@@ -759,6 +765,7 @@
     \end{prfenv} &
+      \prfinterspace=.6em
       {\prfsummary{\Gamma}{A \vee B}}
@@ -769,6 +776,7 @@
     \end{prfenv} \\
+      \prfinterspace=.6em
       {\prfsummary{\Gamma}{A \vee B}}
@@ -779,6 +787,7 @@
     \end{prfenv} &
+      \prfinterspace=.6em
       {\prfsummary{\Gamma}{A \vee B}}
@@ -789,6 +798,7 @@
     \end{prfenv} &
+      \prfinterspace=.6em
       {\prfsummary{\Gamma}{A \vee B}}
@@ -806,6 +816,7 @@
+      \prfinterspace=.6em
@@ -817,6 +828,7 @@
     \end{prfenv} &
+      \prfinterspace=.6em
@@ -828,6 +840,7 @@
     \end{prfenv} &
+      \prfinterspace=.6em
@@ -1327,6 +1340,7 @@
 The disjunction elimination rule, with various line options:
+  \renewcommand{\arraystretch}{3.7}
       \prftree{\prfsummary{\Gamma}{A \vee B}}
@@ -1639,6 +1653,38 @@
 % -------------------------------------
+The package works with any font. It uses the current math fonts for
+typesetting proofs, while it uses the current text font to typeset
+labels and rule names. 
+Care has been taken to ensure that the various dimensions and
+parameters in Section~\ref{sec:parameters} are relative to the current
+font, that is, technically, they are expressed with units \texttt{ex}
+for vertical lengths, and \texttt{em} for horizontal lengths. Dashes
+are \TeX\ rules with thickness \verb|\prflinethickness|.
+For unknown reasons, the \texttt{fontenc} package modifies slightly
+the values for \texttt{ex} and \texttt{em}, thus the graphical
+appearance of proof trees may vary when comparing the results obtained
+by compiling with and without this package.
+In most cases, the graphical appearance of proofs is acceptable, even
+changing font and size. But using fonts whose body is particularly
+heavy, may result in proof lines which are too thin. In this case, the
+user of the package should increment the value of
+The package, up to version 1.5, was designed to work with the Computer
+Modern family of fonts. It worked also with other fonts, without any
+major problem, but, as kindly signalled by D{\'e}mi Nollet at ENS Lyon
+and universit{\'e} Paris-Diderot, dashed and dotted lines do not
+behave correctly, as dashes overlap. Please, update to the latest
+version of the package if you plan to use fonts different from
+Computer Modern.
+% -------------------------------------
 A proof tree is typeset as a \TeX{} box in horizontal mode. This means
 that wherever a character can stay, so does a proof: in principle,
@@ -1780,4 +1826,9 @@
 of a real \TeX{} magician.
+Although the package has been tested for a long time, by now, it is
+possible that a few bugs are still present. To signal a bug, please,
+write an email to the author (see below), possibly attaching a sample
+document which exhibit the misbehaviour, to help tracking and fixing.

Modified: trunk/Master/texmf-dist/tex/latex/prftree/prftree.sty
--- trunk/Master/texmf-dist/tex/latex/prftree/prftree.sty	2016-09-03 21:35:58 UTC (rev 41984)
+++ trunk/Master/texmf-dist/tex/latex/prftree/prftree.sty	2016-09-03 21:36:10 UTC (rev 41985)
@@ -1,7 +1,7 @@
 % prftree.sty
-% by Marco Benini - 11th January 2016
-% v1.4
+% by Marco Benini - 3rd September 2016
+% v1.5
 % A package to typeset natural deduction proofs, or sequent proofs, or
 % tableau proofs
@@ -10,7 +10,7 @@
-\ProvidesPackage{prftree}[2016/01/11 Natural Deduction Proofs]
+\ProvidesPackage{prftree}[2016/09/03 Natural Deduction Proofs]
 % Package options: deactivated by default
 \newif\ifprf at NDOption\prf at NDOptionfalse
@@ -139,9 +139,9 @@
 % conclusion and the list of (direct) assumptions
-% \prflinethickness          default 0.2pt
+% \prflinethickness          default 0.12ex
 % the thickness of the proof line
 % \prfemptylinethickness     default 4 times the linethickness
 % the thickness of the proof line which has to be drawn but it is empty
@@ -155,13 +155,13 @@
 % the space between the label and the proof line
-% \prfinterspace             default .6em
+% \prfinterspace             default .8em
 % the space between two subsequent assumptions
 % \prfdoublelineinterspace   default 1.2pt
 % the space between a double line
 % \prfboundedstyle           default 0
 % defines the style of bounded (discharged) assumptions:
@@ -183,7 +183,7 @@
 % \prffancyline
 % the command to draw "fancy" lines
 \def\prffancyline{\cleaders\hbox to .63em%
-  {\hss\raisebox{-.5ex}[.2ex][0pt]{$\sim$}\hss}\hfill}
+  {\hss\raisebox{-.4ex}[.2ex][0pt]{$\sim$}\hss}\hfill}
 % \prfConclusionBox
 % the command to draw the conclusion box
@@ -565,7 +565,7 @@
     \setbox\prf at summarybox\hbox{$\cdot$}%
     %\prf at tmp\wd\prf at summarybox%
     \setbox\prf at summarybox%
-      \vbox to5.2ex{\cleaders\hbox{$\cdot$}\vfill}%
+      \vbox to4.2ex{\cleaders\hbox{$\cdot$}\vfill}%
     \setbox\prf at summarybox\hbox{\usebox{\prf at summarybox}%
       \hbox{\ \box\prf at summary@label}}%
     %\wd\prf at summarybox\prf at tmp%
@@ -854,13 +854,22 @@
       \setbox\prf at fancybox\hbox to2\prf at linewd{\prffancyline}\else%
       \ifprf at dashedline%
       \setbox\prf at fancybox%
-      \hbox to2\prf at linewd{\cleaders\hbox to.5em{\hss\_\hss}\hfill}\else%
+%      \hbox to2\prf at linewd{\cleaders\hbox
+%      to.5em{\hss\_\hss}\hfill}\else% 
+      \hbox to2\prf at linewd{\cleaders\hbox to.5em{%
+          \hss\vrule height\prflinethickness%
+          width.3em depth0pt\hss}\hfill}%
+      \setbox\prf at fancybox\hbox to2\prf at linewd{%
+        \raise.4ex\box\prf at fancybox}\else%
       \ifprf at dottedline%
       \setbox\prf at fancybox%
-      \hbox to2\prf at linewd{\cleaders\hbox to.33em{\hss.\hss}\hfill}\else% 
+      \hbox to2\prf at linewd{\cleaders\hbox%
+        to.33em{\hss$\cdot$\hss}\hfill}\else%  
    % it must be a straight line!
       \setbox\prf at fancybox\hbox{\vrule width2\prf at linewd%
-        height\prflinethickness}\fi\fi\fi%
+        height\prflinethickness}%
+      \setbox\prf at fancybox\hbox{\raise.4ex%
+        \box\prf at fancybox}\fi\fi\fi%
   % If the line is double, we draw it twice with enough
   % (doublelineinterspace) space between the two copies. 
     \ifprf at doubleline%

More information about the tex-live-commits mailing list