prftree (3sep16)

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

2 files changed, 60 insertions, 9 deletions

diff --git a/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf b/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf
index f92aee2c858..3e4ed547069 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 9db4c1f9e90..1fe8d227c6c 100644
--- a/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex
+++ b/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex
@@ -115,10 +115,12 @@ Assumptions are optional and there may be any number of them. Each
 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.
+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.  
 
 The available options are:
 \begin{itemize}
@@ -294,7 +296,7 @@ constructed:
   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 @@ constructed:
   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.
 \end{itemize}
 
 For example, 
 \begin{displaymath}
-  \prflinepadafter=.7ex
+  \prflinepadafter=0ex
   \prftree[r]{$\supset$I}
   {\prftree[r]{$\supset$I}
     {\prftree[r]{$\supset$E}
@@ -324,7 +326,7 @@ For example,
 \end{displaymath}
 is typeset by
 \begin{verbatim}
-  \prflinepadafter=.7ex
+  \prflinepadafter=0ex
   \prftree[r]{$\supset$I}
     {\prftree[r]{$\supset$I}
       {\prftree[r]{$\supset$E}
@@ -704,6 +706,7 @@ The generation of labels is controlled by the option value:
   defined. This is used to generate a labelled assumption sharing the
   label with another one, which declares the value and the format.
 \end{itemize}
+
 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 @@ 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}
+  \renewcommand{\arraystretch}{6}
   \begin{array}{@{}ccc@{}}
     \begin{prfenv}
+      \prfinterspace=.6em
       \prfsummarystyle=2
       \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEn>}$}
       {\prfsummary{\Gamma}{A \vee B}}
@@ -749,6 +754,7 @@ The same example can be used to show how the other options work:
       {C}
     \end{prfenv} &
     \begin{prfenv}
+      \prfinterspace=.6em
       \prfsummarystyle=2
       \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEr>}$}
       {\prfsummary{\Gamma}{A \vee B}}
@@ -759,6 +765,7 @@ The same example can be used to show how the other options work:
       {C}
     \end{prfenv} &
     \begin{prfenv}
+      \prfinterspace=.6em
       \prfsummarystyle=2
       \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orER>}$}
       {\prfsummary{\Gamma}{A \vee B}}
@@ -769,6 +776,7 @@ The same example can be used to show how the other options work:
       {C}
     \end{prfenv} \\
     \begin{prfenv}
+      \prfinterspace=.6em
       \prfsummarystyle=2
       \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEa>}$}
       {\prfsummary{\Gamma}{A \vee B}}
@@ -779,6 +787,7 @@ The same example can be used to show how the other options work:
       {C}
     \end{prfenv} &
     \begin{prfenv}
+      \prfinterspace=.6em
       \prfsummarystyle=2
       \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEA>}$}
       {\prfsummary{\Gamma}{A \vee B}}
@@ -789,6 +798,7 @@ The same example can be used to show how the other options work:
       {C}
     \end{prfenv} &
     \begin{prfenv}
+      \prfinterspace=.6em
       \prfsummarystyle=2
       \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEf>}$}
       {\prfsummary{\Gamma}{A \vee B}}
@@ -806,6 +816,7 @@ are:
 \begin{displaymath}
   \begin{array}{ccc}
     \begin{prfenv}
+      \prfinterspace=.6em
       \prfboundedstyle=0
       \prfsummarystyle=4
       \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:AorE>}$}
@@ -817,6 +828,7 @@ are:
       {C}
     \end{prfenv} &
     \begin{prfenv}
+      \prfinterspace=.6em
       \prfboundedstyle=1
       \prfsummarystyle=4
       \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:BorE>}$}
@@ -828,6 +840,7 @@ are:
       {C}
     \end{prfenv} &
     \begin{prfenv}
+      \prfinterspace=.6em
       \prfboundedstyle=2
       \prfsummarystyle=4
       \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:CorE>}$}
@@ -1327,6 +1340,7 @@ the previous sections for the description of the features.\vspace{2ex}
 
 The disjunction elimination rule, with various line options:
 \begin{displaymath}
+  \renewcommand{\arraystretch}{3.7}
   \begin{array}{@{}ccc@{}}
     {\prfsummarystyle=1
       \prftree{\prfsummary{\Gamma}{A \vee B}}
@@ -1639,6 +1653,38 @@ shrink a large proof to fit the page length:
 
 % -------------------------------------
 \clearpage
+\section{Fonts}\label{sec:fonts}
+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
+\verb|\prflinethickness|.
+
+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.
+
+% -------------------------------------
+\clearpage
 \section{Internals}\label{sec:internals}
 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 this feature has been postponed to a remote future, or to the will
 of a real \TeX{} magician.
 \vfill
 
+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.
+\vfill
 \end{document}