From 25b22d051f604243eafddac4e9e54e56f80f0f66 Mon Sep 17 00:00:00 2001 From: Karl Berry Date: Sat, 3 Sep 2016 21:36:10 +0000 Subject: prftree (3sep16) git-svn-id: svn://tug.org/texlive/trunk@41985 c570f23f-e606-0410-a88d-b1316a301751 --- Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf | Bin 278480 -> 280556 bytes Master/texmf-dist/doc/latex/prftree/prftreedoc.tex | 69 ++++++++++++++++++--- Master/texmf-dist/tex/latex/prftree/prftree.sty | 35 +++++++---- 3 files changed, 82 insertions(+), 22 deletions(-) (limited to 'Master/texmf-dist') diff --git a/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf b/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf index f92aee2c858..3e4ed547069 100644 Binary files a/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf and b/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf 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}$} {\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}$} {\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}$} {\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}$} {\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}$} {\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}$} {\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}$} @@ -817,6 +828,7 @@ are: {C} \end{prfenv} & \begin{prfenv} + \prfinterspace=.6em \prfboundedstyle=1 \prfsummarystyle=4 \prftree[r]{$\vee\mathrm{E}_{\prfref}$} @@ -828,6 +840,7 @@ are: {C} \end{prfenv} & \begin{prfenv} + \prfinterspace=.6em \prfboundedstyle=2 \prfsummarystyle=4 \prftree[r]{$\vee\mathrm{E}_{\prfref}$} @@ -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}} @@ -1637,6 +1651,38 @@ shrink a large proof to fit the page length: \end{prfenv} \end{displaymath} +% ------------------------------------- +\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} @@ -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% -- cgit v1.2.3