summaryrefslogtreecommitdiff
path: root/Master/texmf-dist
diff options
context:
space:
mode:
authorKarl Berry <karl@freefriends.org>2016-09-03 21:36:10 +0000
committerKarl Berry <karl@freefriends.org>2016-09-03 21:36:10 +0000
commit25b22d051f604243eafddac4e9e54e56f80f0f66 (patch)
tree3907e07930feef103791ff4b906ee493d9a0c1a3 /Master/texmf-dist
parent69a9e2bb8b63735fde506fd73e535e8f59b4003e (diff)
prftree (3sep16)
git-svn-id: svn://tug.org/texlive/trunk@41985 c570f23f-e606-0410-a88d-b1316a301751
Diffstat (limited to 'Master/texmf-dist')
-rw-r--r--Master/texmf-dist/doc/latex/prftree/prftreedoc.pdfbin278480 -> 280556 bytes
-rw-r--r--Master/texmf-dist/doc/latex/prftree/prftreedoc.tex69
-rw-r--r--Master/texmf-dist/tex/latex/prftree/prftree.sty35
3 files changed, 82 insertions, 22 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
Binary files differ
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}
diff --git a/Master/texmf-dist/tex/latex/prftree/prftree.sty b/Master/texmf-dist/tex/latex/prftree/prftree.sty
index 425c1493d71..8f77541c058 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 - 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 @@
%
\NeedsTeXFormat{LaTeX2e}
-\ProvidesPackage{prftree}[2016/01/11 Natural Deduction Proofs]
+\ProvidesPackage{prftree}[2016/09/03 Natural Deduction Proofs]
% Package options: deactivated by default
\newif\ifprf@NDOption\prf@NDOptionfalse
@@ -139,9 +139,9 @@
% conclusion and the list of (direct) assumptions
\newdimen\prflineextra\prflineextra.3em
-% \prflinethickness default 0.2pt
+% \prflinethickness default 0.12ex
% the thickness of the proof line
-\newdimen\prflinethickness\prflinethickness.2pt
+\newdimen\prflinethickness\prflinethickness.12ex
% \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
\newdimen\prflabelskip\prflabelskip.2em
-% \prfinterspace default .6em
+% \prfinterspace default .8em
% the space between two subsequent assumptions
-\newdimen\prfinterspace\prfinterspace.6em
+\newdimen\prfinterspace\prfinterspace.8em
% \prfdoublelineinterspace default 1.2pt
% the space between a double line
-\newdimen\prfdoublelineinterspace\prfdoublelineinterspace1.2pt
+\newdimen\prfdoublelineinterspace\prfdoublelineinterspace0.06ex
% \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@summarybox\hbox{$\cdot$}%
%\prf@tmp\wd\prf@summarybox%
\setbox\prf@summarybox%
- \vbox to5.2ex{\cleaders\hbox{$\cdot$}\vfill}%
+ \vbox to4.2ex{\cleaders\hbox{$\cdot$}\vfill}%
\setbox\prf@summarybox\hbox{\usebox{\prf@summarybox}%
\hbox{\ \box\prf@summary@label}}%
%\wd\prf@summarybox\prf@tmp%
@@ -854,13 +854,22 @@
\setbox\prf@fancybox\hbox to2\prf@linewd{\prffancyline}\else%
\ifprf@dashedline%
\setbox\prf@fancybox%
- \hbox to2\prf@linewd{\cleaders\hbox to.5em{\hss\_\hss}\hfill}\else%
+% \hbox to2\prf@linewd{\cleaders\hbox
+% to.5em{\hss\_\hss}\hfill}\else%
+ \hbox to2\prf@linewd{\cleaders\hbox to.5em{%
+ \hss\vrule height\prflinethickness%
+ width.3em depth0pt\hss}\hfill}%
+ \setbox\prf@fancybox\hbox to2\prf@linewd{%
+ \raise.4ex\box\prf@fancybox}\else%
\ifprf@dottedline%
\setbox\prf@fancybox%
- \hbox to2\prf@linewd{\cleaders\hbox to.33em{\hss.\hss}\hfill}\else%
+ \hbox to2\prf@linewd{\cleaders\hbox%
+ to.33em{\hss$\cdot$\hss}\hfill}\else%
% it must be a straight line!
\setbox\prf@fancybox\hbox{\vrule width2\prf@linewd%
- height\prflinethickness}\fi\fi\fi%
+ height\prflinethickness}%
+ \setbox\prf@fancybox\hbox{\raise.4ex%
+ \box\prf@fancybox}\fi\fi\fi%
% If the line is double, we draw it twice with enough
% (doublelineinterspace) space between the two copies.
\ifprf@doubleline%