summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/tex
diff options
context:
space:
mode:
Diffstat (limited to 'Master/texmf-dist/tex')
-rw-r--r--Master/texmf-dist/tex/latex/prftree/prftree.sty159
1 files changed, 90 insertions, 69 deletions
diff --git a/Master/texmf-dist/tex/latex/prftree/prftree.sty b/Master/texmf-dist/tex/latex/prftree/prftree.sty
index 2bec5c8f07a..425c1493d71 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 - 31st October 2015
-% v1.2
+% by Marco Benini - 11th January 2016
+% v1.4
%
% A package to typeset natural deduction proofs, or sequent proofs, or
% tableau proofs
@@ -10,16 +10,20 @@
%
\NeedsTeXFormat{LaTeX2e}
-\ProvidesPackage{prftree}[2015/10/31 Natural Deduction Proofs]
+\ProvidesPackage{prftree}[2016/01/11 Natural Deduction Proofs]
% Package options: deactivated by default
\newif\ifprf@NDOption\prf@NDOptionfalse
\newif\ifprf@SEQOption\prf@SEQOptionfalse
\newif\ifprfIMPOption\prfIMPOptionfalse
+\newif\ifprfSTRUToption\prfSTRUToptiontrue
+\newif\ifprfSTRUTlabeloption\prfSTRUTlabeloptiontrue
\DeclareOption{ND}{\prf@NDOptiontrue}
\DeclareOption{SEQ}{\prf@SEQOptiontrue}
\DeclareOption{IMP}{\prfIMPOptiontrue}
+\DeclareOption{Strut}{\prfSTRUToptionfalse}
+\DeclareOption{StrutLabel}{\prfSTRUTlabeloptionfalse}
\ProcessOptions\relax
%--------------------------------------------------------------------
@@ -121,10 +125,13 @@
% future version of the package.
%--------------------------------------------------------------------
-% \prflinepad default 0.3ex
-% the space between the baseline of assumptions and the proof line and
-% also the space between the proof line and the top of the conclusion
-\newdimen\prflinepad\prflinepad.3ex
+% \prflinepadbefore default 0.3ex
+% the space between the bottom of assumptions and the proof line
+\newdimen\prflinepadbefore\prflinepadbefore.3ex
+
+% \prflinepadafter default 0.3ex
+% the space between the proof line and the top of the conclusion
+\newdimen\prflinepadafter\prflinepadafter.3ex
% \prflineextra default 0.3em
% the length which extends on the left and on the right the proof line
@@ -181,20 +188,24 @@
% \prfConclusionBox
% the command to draw the conclusion box
\def\prfConclusionBox#1{%
- \hbox{$\displaystyle\begingroup#1\endgroup\mathstrut$}}
+ \hbox{$\displaystyle\begingroup#1\endgroup%
+ \ifprfSTRUToption\mathstrut\fi$}}
% \prfAssumptionBox
% the command to draw the assumption box
\def\prfAssumptionBox#1{%
- \hbox{$\displaystyle\begingroup#1\endgroup\mathstrut$}}
+ \hbox{$\displaystyle\begingroup#1\endgroup%
+ \ifprfSTRUToption\mathstrut\fi$}}
% \prfRuleNameBox
% the command to draw the rule name box.
-\def\prfRuleNameBox#1{\hbox{\begingroup#1\endgroup\strut}}
+\def\prfRuleNameBox#1{\hbox{\begingroup#1\endgroup%
+ \ifprfSTRUTlabeloption\strut\fi}}
% \prfLabelBox
% the command to draw the label box.
-\def\prfLabelBox#1{\hbox{\begingroup#1\endgroup\strut}}
+\def\prfLabelBox#1{\hbox{\begingroup#1\endgroup%
+ \ifprfSTRUTlabeloption\strut\fi}}
% \prfdiscargedassumption
% the command to draw a discharged assumption in a custom way.
@@ -326,9 +337,9 @@
\newif\ifprf@lbl@fnsymbol\prf@lbl@fnsymbolfalse
\newif\ifprf@lbl@label\prf@lbl@labelfalse
-% The prooftree environment is used to define the scope of the
+% The prftree environment is used to define the scope of the
% assumption references
-\newenvironment{prooftree}%
+\newenvironment{prfenv}%
{\setcounter{prfassumptioncounter}{0}}%
{\setcounter{prfassumptioncounter}{0}}
@@ -336,15 +347,23 @@
\def\ifprf@undefref<#1>{%
\expandafter\ifx\csname prf@ref@@#1\endcsname\relax}
+% Test whether a reference has never been referenced before
+\def\ifprf@unrefref<#1>{%
+ \expandafter\ifx\csname prf@refref@@#1\endcsname\relax}
+
% Test whether a reference has been written in the .aux file
\def\ifprf@unwrittenref<#1>{%
\expandafter\ifx\csname prf@w@ref@#1\endcsname\relax}
% Write a reference
+\newif\ifprf@refhack\prf@refhacktrue
\protected\def\prfref<#1>{%
\ifprf@undefref<#1>\relax\mbox{??}%
- \PackageWarningNoLine{prftree}{Undefined reference <#1>}\relax%
- \else\csname prf@ref@@#1\endcsname\relax\fi\relax}
+ \ifprf@refhack\label{prf@ref@hack}% to force recompilation
+ \global\prf@refhackfalse\fi%
+ \PackageWarningNoLine{prftree}{Undefined reference <#1>}%
+ \expandafter\gdef\csname prf@ref@@#1\endcsname{\mbox{??}}\else%
+ \csname prf@ref@@#1\endcsname\fi\relax}
% Create the anchor from what stored in the .aux file
\def\prfauxlabel#1#2{%
@@ -682,7 +701,9 @@
% #1 the line options
% #2 the rule name
\def\prf@@NNtree#1#2{%
- \edef\prf@choice{\ifprf@label{#1}{#2}\else{#1}{#2}{}\fi}%
+ \def\prf@hackpar{#2}%
+ \edef\prf@choice{\ifprf@label{#1}{\noexpand\prf@hackpar}\else%
+ {#1}{\noexpand\prf@hackpar}{}\fi}%
\expandafter\prf@tree\prf@choice}
% We collect the first assumption, if any, or the conclusion otherwise
@@ -735,6 +756,7 @@
% #6 the list of assumptions
%--------------------------------------------------------------------
+\newbox\prf@@@@proofbox
\def\prf@draw#1#2#3#4#5#6{%
% We construct the boxes which will constitute the proof
\ifprf@first\prf@push{1}\else\prf@push{0}\fi%
@@ -878,7 +900,6 @@
% the centre of the rule name and the rule box gets attached to the
% proof line box.
\prf@linedp\z@%
- \ifprf@noline\setbox\prf@fancybox\hbox to2\prf@linewd{}\fi%
\ifprf@rule\advance\prf@linedp.5\ht\prf@fancybox%
\advance\prf@linedp-.5\ht\prf@rulenamebox%
\advance\prf@linedp.5\dp\prf@rulenamebox%
@@ -904,8 +925,8 @@
\hbox{\hskip\prf@temp\raise\dp\prf@linebox\box\prf@linebox}%
% We need to calculate the distance between the assumptions and the
% proofline: if there are no assumptions, it is zero; if there are
- % assumptions but no rule name, it is \prflinepad; otherwise it is
- % \linepad plus half of the "real" line's height
+ % assumptions but no rule name, it is \prflinepadbefore; otherwise
+ % it is \linepadbefore plus half of the "real" line's height
\prf@tmp\z@%
\ifprf@assum%
\ifprf@rule\prf@tmp-.5\ht\prf@linebox%
@@ -915,17 +936,17 @@
\prf@tmp-.5\ht\prf@linebox%
\advance\prf@tmp.5\ht\prf@fancybox%
\advance\prf@tmp.5\dp\prf@fancybox\fi\fi%
- \advance\prf@tmp\prflinepad%
+ \advance\prf@tmp\prflinepadbefore%
\setbox\prf@assumptionsbox%
\vbox{\box\prf@assumptionsbox\nointerlineskip\vskip\prf@tmp}\fi%
% We need to calculate the distance between the proofline and the
% conclusion: it is slightly complex to explain... try to draw the
% whole thing to make it clear!!
- \prf@temp\prflinepad%
+ \prf@temp\prflinepadafter%
\ifprf@noline%
\ifprf@assum%
- \advance\prf@temp\prfemptylinethickness\fi%
- \advance\prf@temp-\prflinepad\fi%
+ \advance\prf@temp\prfemptylinethickness\else%
+ \advance\prf@temp-\prflinepadafter\fi\fi%
\ifprf@rule%
\advance\prf@temp-.5\ht\prf@linebox%
\advance\prf@temp.5\ht\prf@fancybox%
@@ -968,61 +989,61 @@
\def\NDDL#1{\prfboundedassumption<#1>}
\def\NDP{\prftree}
\def\NDANDI{\prftree[by]{$\scriptstyle\mathord{\wedge}%
- \noexpand\textup{I}$}}
+ \textup{I}$}}
\def\NDANDEL{\prftree[by]{$\scriptstyle\mathord{\wedge}%
- \noexpand\textup{E}_1$}}
+ \textup{E}_1$}}
\def\NDANDER{\prftree[by]{$\scriptstyle\mathord{\wedge}%
- \noexpand\textup{E}_2$}}
+ \textup{E}_2$}}
\def\NDANDE{\prftree[by]{$\scriptstyle\mathord{\wedge}%
- \noexpand\textup{E}$}}
+ \textup{E}$}}
\def\NDORIL{\prftree[by]{$\scriptstyle\mathord{\vee}%
- \noexpand\textup{I}_1$}}
+ \textup{I}_1$}}
\def\NDORIR{\prftree[by]{$\scriptstyle\mathord{\vee}%
- \noexpand\textup{I}_2$}}
+ \textup{I}_2$}}
\def\NDORI{\prftree[by]{$\scriptstyle\mathord{\vee}%
- \noexpand\textup{I}$}}
+ \textup{I}$}}
\def\NDORE{\prftree[by]{$\scriptstyle\mathord{\vee}%
- \noexpand\textup{E}$}}
+ \textup{E}$}}
\def\NDOREL#1{\prftree[by]{$\scriptstyle{\vee}%
- {\noexpand\textup{E}}^{\noexpand\prfref<#1>}$}}
+ {\textup{E}}^{\prfref<#1>}$}}
\ifprfIMPOption
\def\NDIMPI{\prftree[by]{$\scriptstyle\mathord{\supset}%
- \noexpand\textup{I}$}}
+ \textup{I}$}}
\def\NDIMPE{\prftree[by]{$\scriptstyle\mathord{\supset}%
- \noexpand\textup{E}$}}
+ \textup{E}$}}
\def\NDIMPIL#1{\prftree[by]{$\scriptstyle\mathord{\supset}%
- \noexpand\textup{I}^{\noexpand\prfref<#1>}$}}
+ \textup{I}^{\prfref<#1>}$}}
\else
\def\NDIMPI{\prftree[by]{$\scriptstyle\mathord{\rightarrow}%
- \noexpand\textup{I}$}}
+ \textup{I}$}}
\def\NDIMPE{\prftree[by]{$\scriptstyle\mathord{\rightarrow}%
- \noexpand\textup{E}$}}
+ \textup{E}$}}
\def\NDIMPIL#1{%
\prftree[by]{$\scriptstyle\mathord{\rightarrow}%
- \noexpand\textup{I}^{\noexpand\prfref<#1>}$}}\fi
+ \textup{I}^{\prfref<#1>}$}}\fi
\def\NDNOTI{\prftree[by]{$\scriptstyle\mathord{\neg}%
- \noexpand\textup{I}$}}
+ \textup{I}$}}
\def\NDNOTIL#1{\prftree[by]{$\scriptstyle{\neg}%
- \noexpand\textup{I}^{\noexpand\prfref<#1>}$}}
+ \textup{I}^{\prfref<#1>}$}}
\def\NDNOTE{\prftree[by]{$\scriptstyle\mathord{\neg}%
- \noexpand\textup{E}$}}
+ \textup{E}$}}
\def\NDALLI{\prftree[by]{$\scriptstyle\mathord{\forall}%
- \noexpand\textup{I}$}}
+ \textup{I}$}}
\def\NDALLE{\prftree[by]{$\scriptstyle\mathord{\forall}%
- \noexpand\textup{E}$}}
+ \textup{E}$}}
\def\NDEXI{\prftree[by]{$\scriptstyle\mathord{\exists}%
- \noexpand\textup{I}$}}
+ \textup{I}$}}
\def\NDEXE{\prftree[by]{$\scriptstyle\mathord{\exists}%
- \noexpand\textup{E}$}}
+ \textup{E}$}}
\def\NDEXEL#1{%
\prftree[by]{$\scriptstyle\mathord{\exists}%
- \noexpand\textup{E}^{\noexpand\prfref<#1>}$}}
+ \textup{E}^{\prfref<#1>}$}}
\def\NDTI{\prftree[by]{$\scriptstyle\mathord{\top}%
- \noexpand\textup{I}$}}
+ \textup{I}$}}
\def\NDFE{\prftree[by]{$\scriptstyle\mathord{\bot}%
- \noexpand\textup{E}$}}
- \def\NDLEM{\prftree[by]{$\scriptstyle\noexpand\textup{lem}$}}
- \def\NDAX{\prftree[by]{$\scriptstyle\noexpand\textup{ax}$}}
+ \textup{E}$}}
+ \def\NDLEM{\prftree[by]{$\scriptstyle\textup{lem}$}}
+ \def\NDAX{\prftree[by]{$\scriptstyle\textup{ax}$}}
\fi
% -------------------------------------------------------------------
@@ -1035,40 +1056,40 @@
\def\SEQA{\prfassumption}
\def\SEQD{\prfboundedassumption}
\def\SEQP{\prftree}
- \def\SEQAX{\prftree[by]{$\scriptstyle\noexpand\textup{Ax}$}}
- \def\SEQLF{\prftree[by]{$\scriptstyle\noexpand\textup{L}\bot$}}
- \def\SEQLW{\prftree[by]{$\scriptstyle\noexpand\textup{LW}$}}
- \def\SEQRW{\prftree[by]{$\scriptstyle\noexpand\textup{RW}$}}
- \def\SEQLC{\prftree[by]{$\scriptstyle\noexpand\textup{LC}$}}
- \def\SEQRC{\prftree[by]{$\scriptstyle\noexpand\textup{RC}$}}
- \def\SEQLAND{\prftree[by]{$\scriptstyle\noexpand\textup{L}%
+ \def\SEQAX{\prftree[by]{$\scriptstyle\textup{Ax}$}}
+ \def\SEQLF{\prftree[by]{$\scriptstyle\textup{L}\bot$}}
+ \def\SEQLW{\prftree[by]{$\scriptstyle\textup{LW}$}}
+ \def\SEQRW{\prftree[by]{$\scriptstyle\textup{RW}$}}
+ \def\SEQLC{\prftree[by]{$\scriptstyle\textup{LC}$}}
+ \def\SEQRC{\prftree[by]{$\scriptstyle\textup{RC}$}}
+ \def\SEQLAND{\prftree[by]{$\scriptstyle\textup{L}%
\mathord{\wedge}$}}
- \def\SEQRAND{\prftree[by]{$\scriptstyle\noexpand\textup{R}%
+ \def\SEQRAND{\prftree[by]{$\scriptstyle\textup{R}%
\mathord{\wedge}$}}
- \def\SEQLOR{\prftree[by]{$\scriptstyle\noexpand\textup{L}%
+ \def\SEQLOR{\prftree[by]{$\scriptstyle\textup{L}%
\mathord{\vee}$}}
- \def\SEQROR{\prftree[by]{$\scriptstyle\noexpand\textup{R}%
+ \def\SEQROR{\prftree[by]{$\scriptstyle\textup{R}%
\mathord{\vee}$}}
\ifprfIMPOption
- \def\SEQLIMP{\prftree[by]{$\scriptstyle\noexpand\textup{L}%
+ \def\SEQLIMP{\prftree[by]{$\scriptstyle\textup{L}%
\mathord{\supset}$}}
- \def\SEQRIMP{\prftree[by]{$\scriptstyle\noexpand\textup{R}%
+ \def\SEQRIMP{\prftree[by]{$\scriptstyle\textup{R}%
\mathord{\supset}$}}
\else
- \def\SEQLIMP{\prftree[by]{$\scriptstyle\noexpand\textup{L}%
+ \def\SEQLIMP{\prftree[by]{$\scriptstyle\textup{L}%
\mathord{\rightarrow}$}}
- \def\SEQRIMP{\prftree[by]{$\scriptstyle\noexpand\textup{R}%
+ \def\SEQRIMP{\prftree[by]{$\scriptstyle\textup{R}%
\mathord{\rightarrow}$}}
\fi
- \def\SEQLALL{\prftree[by]{$\scriptstyle\noexpand\textup{L}%
+ \def\SEQLALL{\prftree[by]{$\scriptstyle\textup{L}%
\mathord{\forall}$}}
- \def\SEQRALL{\prftree[by]{$\scriptstyle\noexpand\textup{R}%
+ \def\SEQRALL{\prftree[by]{$\scriptstyle\textup{R}%
\mathord{\forall}$}}
- \def\SEQLEX{\prftree[by]{$\scriptstyle\noexpand\textup{L}%
+ \def\SEQLEX{\prftree[by]{$\scriptstyle\textup{L}%
\mathord{\exists}$}}
- \def\SEQREX{\prftree[by]{$\scriptstyle\noexpand\textup{R}%
+ \def\SEQREX{\prftree[by]{$\scriptstyle\textup{R}%
\mathord{\exists}$}}
- \def\SEQCUT{\prftree[by]{$\scriptstyle\noexpand\textup{Cut}$}}
+ \def\SEQCUT{\prftree[by]{$\scriptstyle\textup{Cut}$}}
\fi
% -------------------------------------------------------------------