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
http://tug.org/svn/texlive?view=revision&revision=41985
Author: karl
Date: 2016-09-03 23:36:10 +0200 (Sat, 03 Sep 2016)
Log Message:
-----------
prftree (3sep16)
Modified Paths:
--------------
trunk/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf
trunk/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex
trunk/Master/texmf-dist/tex/latex/prftree/prftree.sty
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.
+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}
\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.
\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 @@
\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 @@
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 @@
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 @@
{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 @@
{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 @@
{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 @@
{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 @@
{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 @@
\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 @@
{C}
\end{prfenv} &
\begin{prfenv}
+ \prfinterspace=.6em
\prfboundedstyle=1
\prfsummarystyle=4
\prftree[r]{$\vee\mathrm{E}_{\prfref<assum:BorE>}$}
@@ -828,6 +840,7 @@
{C}
\end{prfenv} &
\begin{prfenv}
+ \prfinterspace=.6em
\prfboundedstyle=2
\prfsummarystyle=4
\prftree[r]{$\vee\mathrm{E}_{\prfref<assum:CorE>}$}
@@ -1327,6 +1340,7 @@
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 @@
% -------------------------------------
\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 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}
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 @@
%
\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 at NDOption\prf at 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 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