update lkproof

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

1 files changed, 168 insertions, 187 deletions

diff --git a/Master/texmf-dist/tex/latex/lkproof/proof.sty b/Master/texmf-dist/tex/latex/lkproof/proof.sty
index e32030018a1..c272a8103f1 100644
--- a/Master/texmf-dist/tex/latex/lkproof/proof.sty
+++ b/Master/texmf-dist/tex/latex/lkproof/proof.sty
@@ -1,8 +1,8 @@
-%       proof.sty       (Proof Figure Macros)
+%	proof.sty	(Proof Figure Macros)
 %
-%       version 3.0 (for both LaTeX 2.09 and LaTeX 2e)
-%       Mar 6, 1997
-%       Copyright (C) 1990 -- 1997, Makoto Tatsuta (tatsuta@kusm.kyoto-u.ac.jp)
+% 	version 3.1 (for both LaTeX 2.09 and LaTeX 2e)
+%	Nov 24, 2005
+% 	Copyright (C) 1990 -- 2005, Makoto Tatsuta (tatsuta@nii.ac.jp)
 % 
 % This program is free software; you can redistribute it or modify
 % it under the terms of the GNU General Public License as published by
@@ -14,71 +14,71 @@
 % MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 % GNU General Public License for more details.
 %
-%       Usage:
-%               In \documentstyle, specify an optional style `proof', say,
-%                       \documentstyle[proof]{article}.
+%	Usage:
+%		In \documentstyle, specify an optional style `proof', say,
+%			\documentstyle[proof]{article}.
 %
-%       The following macros are available:
+%	The following macros are available:
 %
-%       In all the following macros, all the arguments such as
-%       <Lowers> and <Uppers> are processed in math mode.
+%	In all the following macros, all the arguments such as
+%	<Lowers> and <Uppers> are processed in math mode.
 %
-%       \infer<Lower><Uppers>
-%               draws an inference.
+%	\infer<Lower><Uppers>
+%		draws an inference.
 %
-%               Use & in <Uppers> to delimit upper formulae.
-%               <Uppers> consists more than 0 formulae.
+%		Use & in <Uppers> to delimit upper formulae.
+%		<Uppers> consists more than 0 formulae.
 %
-%               \infer returns \hbox{ ... } or \vbox{ ... } and
-%               sets \@LeftOffset and \@RightOffset globally.
+%		\infer returns \hbox{ ... } or \vbox{ ... } and
+%		sets \@LeftOffset and \@RightOffset globally.
 %
-%       \infer[<Label>]<Lower><Uppers>
-%               draws an inference labeled with <Label>.
+%	\infer[<Label>]<Lower><Uppers>
+%		draws an inference labeled with <Label>.
 %
-%       \infer*<Lower><Uppers>
-%               draws a many step deduction.
+%	\infer*<Lower><Uppers>
+%		draws a many step deduction.
 %
-%       \infer*[<Label>]<Lower><Uppers>
-%               draws a many step deduction labeled with <Label>.
+%	\infer*[<Label>]<Lower><Uppers>
+%		draws a many step deduction labeled with <Label>.
 %
-%       \infer=<Lower><Uppers>
-%               draws a double-ruled deduction.
+%	\infer=<Lower><Uppers>
+%		draws a double-ruled deduction.
 %
-%       \infer=[<Label>]<Lower><Uppers>
-%               draws a double-ruled deduction labeled with <Label>.
+%	\infer=[<Label>]<Lower><Uppers>
+%		draws a double-ruled deduction labeled with <Label>.
 %
-%       \deduce<Lower><Uppers>
-%               draws an inference without a rule.
+%	\deduce<Lower><Uppers>
+%		draws an inference without a rule.
 %
-%       \deduce[<Proof>]<Lower><Uppers>
-%               draws a many step deduction with a proof name.
+%	\deduce[<Proof>]<Lower><Uppers>
+%		draws a many step deduction with a proof name.
 %
-%       Example:
-%               If you want to write
-%                           B C
-%                          -----
-%                      A     D
-%                     ----------
-%                         E
-%       use
-%               \infer{E}{
-%                       A
-%                       &
-%                       \infer{D}{B & C}
-%               }
+%	Example:
+%		If you want to write
+%       	       	    B C
+%		 	   -----
+%		       A     D
+%		      ----------
+%			  E
+%	use
+%		\infer{E}{
+%			A
+%			&
+%			\infer{D}{B & C}
+%		}
 %
 
-%       Style Parameters
+%	Style Parameters
 
-\newdimen\inferLineSkip         \inferLineSkip=2pt
-\newdimen\inferLabelSkip        \inferLabelSkip=5pt
+\newdimen\inferLineSkip		\inferLineSkip=2pt
+\newdimen\inferLabelSkip	\inferLabelSkip=5pt
 \def\inferTabSkip{\quad}
 
-%       Variables
+%	Variables
 
-\newdimen\@LeftOffset   % global
-\newdimen\@RightOffset  % global
-\newdimen\@SavedLeftOffset      % safe from users
+\newdimen\@LeftOffset	% global
+\newdimen\@RightOffset	% global
+\newdimen\@SavedLeftOffset	% safe from users
 
 \newdimen\UpperWidth
 \newdimen\LowerWidth
@@ -100,32 +100,18 @@
 \newbox\@LabelPart
 \newbox\ResultBox
 
-%       Flags
+%	Flags
 
-\newif\if@inferRule     % whether \@infer draws a rule.
-\newif\if@DoubleRule    % whether \@infer draws doulbe rules.
-\newif\if@ReturnLeftOffset      % whether \@infer returns \@LeftOffset.
-\newif\if@MathSaved     % whether inner math mode where \infer or
-                       % \deduce appears.
+\newif\if@inferRule	% whether \@infer draws a rule.
+\newif\if@DoubleRule	% whether \@infer draws doulbe rules.
+\newif\if@ReturnLeftOffset	% whether \@infer returns \@LeftOffset.
 
-%       Special Fonts
+%	Special Fonts
 
 \def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@
     \vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}
 
-%       Math Save Macros
-%
-%       \@SaveMath is called in the very begining of toplevel macros
-%       which are \infer and \deduce.
-%       \@RestoreMath is called in the very last before toplevel macros end.
-%       Remark \infer and \deduce ends calling \@infer.
-
-\def\@SaveMath{\@MathSavedfalse \ifmmode \ifinner
-       \relax $\relax \@MathSavedtrue \fi\fi }
-
-\def\@RestoreMath{\if@MathSaved \relax $\relax\fi }
-
-%       Macros
+%	Macros
 
 % Renaming @ifnextchar and @ifnch of LaTeX2e to @IFnextchar and @IFnch.
 
@@ -138,141 +124,136 @@
       \fi \reserved@d}
 
 \def\@ifEmpty#1#2#3{\def\@tempa{\@empty}\def\@tempb{#1}\relax
-       \ifx \@tempa \@tempb #2\else #3\fi }
+	\ifx \@tempa \@tempb #2\else #3\fi }
 
-\def\infer{\@SaveMath \@IFnextchar *{\@inferSteps}{\relax
-       \@IFnextchar ={\@inferDoubleRule}{\@inferOneStep}}}
+\def\infer{\@IFnextchar *{\@inferSteps}{\relax
+	\@IFnextchar ={\@inferDoubleRule}{\@inferOneStep}}}
 
 \def\@inferOneStep{\@inferRuletrue \@DoubleRulefalse
-       \@IFnextchar [{\@infer}{\@infer[\@empty]}}
+	\@IFnextchar [{\@infer}{\@infer[\@empty]}}
 
 \def\@inferDoubleRule={\@inferRuletrue \@DoubleRuletrue
-       \@IFnextchar [{\@infer}{\@infer[\@empty]}}
+	\@IFnextchar [{\@infer}{\@infer[\@empty]}}
 
 \def\@inferSteps*{\@IFnextchar [{\@@inferSteps}{\@@inferSteps[\@empty]}}
 
 \def\@@inferSteps[#1]{\@deduce{#1}[\DeduceSym]}
 
-\def\deduce{\@SaveMath \@IFnextchar [{\@deduce{\@empty}}
-       {\@inferRulefalse \@infer[\@empty]}}
+\def\deduce{\@IFnextchar [{\@deduce{\@empty}}
+	{\@inferRulefalse \@infer[\@empty]}}
 
-%       \@deduce<Proof Label>[<Proof>]<Lower><Uppers>
+%	\@deduce<Proof Label>[<Proof>]<Lower><Uppers>
 
 \def\@deduce#1[#2]#3#4{\@inferRulefalse
-       \@infer[\@empty]{#3}{\@SaveMath \@infer[{#1}]{#2}{#4}}}
+	\@infer[\@empty]{#3}{\@infer[{#1}]{#2}{#4}}}
 
-%       \@infer[<Label>]<Lower><Uppers>
-%               If \@inferRuletrue, it draws a rule and <Label> is right to
-%               a rule. In this case, if \@DoubleRuletrue, it draws
-%               double rules.
+%	\@infer[<Label>]<Lower><Uppers>
+%		If \@inferRuletrue, it draws a rule and <Label> is right to
+%		a rule. In this case, if \@DoubleRuletrue, it draws
+%		double rules.
 %
-%               Otherwise, draws no rule and <Label> is right to <Lower>.
+%		Otherwise, draws no rule and <Label> is right to <Lower>.
 
 \def\@infer[#1]#2#3{\relax
 % Get parameters
-       \if@ReturnLeftOffset \else \@SavedLeftOffset=\@LeftOffset \fi
-       \setbox\@LabelPart=\hbox{$#1$}\relax
-       \setbox\@LowerPart=\hbox{$#2$}\relax
-%
-       \global\@LeftOffset=0pt
-       \setbox\@UpperPart=\vbox{\tabskip=0pt \halign{\relax
-               \global\@RightOffset=0pt \@ReturnLeftOffsettrue $##$&&
-               \inferTabSkip
-               \global\@RightOffset=0pt \@ReturnLeftOffsetfalse $##$\cr
-               #3\cr}}\relax
-%                       Here is a little trick.
-%                       \@ReturnLeftOffsettrue(false) influences on \infer or
-%                       \deduce placed in ## locally
-%                       because of \@SaveMath and \@RestoreMath.
-       \UpperLeftOffset=\@LeftOffset
-       \UpperRightOffset=\@RightOffset
+	\if@ReturnLeftOffset \else \@SavedLeftOffset=\@LeftOffset \fi
+	\setbox\@LabelPart=\hbox{$#1$}\relax
+	\setbox\@LowerPart=\hbox{$#2$}\relax
+%
+	\global\@LeftOffset=0pt
+	\setbox\@UpperPart=\vbox{\tabskip=0pt \halign{\relax
+		\global\@RightOffset=0pt \@ReturnLeftOffsettrue $##$&&
+		\inferTabSkip
+		\global\@RightOffset=0pt \@ReturnLeftOffsetfalse $##$\cr
+		#3\cr}}\relax
+	\UpperLeftOffset=\@LeftOffset
+	\UpperRightOffset=\@RightOffset
 % Calculate Adjustments
-       \LowerWidth=\wd\@LowerPart
-       \LowerHeight=\ht\@LowerPart
-       \LowerCenter=0.5\LowerWidth
-%
-       \UpperWidth=\wd\@UpperPart \advance\UpperWidth by -\UpperLeftOffset
-       \advance\UpperWidth by -\UpperRightOffset
-       \UpperCenter=\UpperLeftOffset
-       \advance\UpperCenter by 0.5\UpperWidth
-%
-       \ifdim \UpperWidth > \LowerWidth
-               % \UpperCenter > \LowerCenter
-       \UpperAdjust=0pt
-       \RuleAdjust=\UpperLeftOffset
-       \LowerAdjust=\UpperCenter \advance\LowerAdjust by -\LowerCenter
-       \RuleWidth=\UpperWidth
-       \global\@LeftOffset=\LowerAdjust
-%
-       \else   % \UpperWidth <= \LowerWidth
-       \ifdim \UpperCenter > \LowerCenter
-%
-       \UpperAdjust=0pt
-       \RuleAdjust=\UpperCenter \advance\RuleAdjust by -\LowerCenter
-       \LowerAdjust=\RuleAdjust
-       \RuleWidth=\LowerWidth
-       \global\@LeftOffset=\LowerAdjust
-%
-       \else   % \UpperWidth <= \LowerWidth
-               % \UpperCenter <= \LowerCenter
-%
-       \UpperAdjust=\LowerCenter \advance\UpperAdjust by -\UpperCenter
-       \RuleAdjust=0pt
-       \LowerAdjust=0pt
-       \RuleWidth=\LowerWidth
-       \global\@LeftOffset=0pt
-%
-       \fi\fi
+	\LowerWidth=\wd\@LowerPart
+	\LowerHeight=\ht\@LowerPart
+	\LowerCenter=0.5\LowerWidth
+%
+	\UpperWidth=\wd\@UpperPart \advance\UpperWidth by -\UpperLeftOffset
+	\advance\UpperWidth by -\UpperRightOffset
+	\UpperCenter=\UpperLeftOffset
+	\advance\UpperCenter by 0.5\UpperWidth
+%
+	\ifdim \UpperWidth > \LowerWidth
+		% \UpperCenter > \LowerCenter
+	\UpperAdjust=0pt
+	\RuleAdjust=\UpperLeftOffset
+	\LowerAdjust=\UpperCenter \advance\LowerAdjust by -\LowerCenter
+	\RuleWidth=\UpperWidth
+	\global\@LeftOffset=\LowerAdjust
+%
+	\else	% \UpperWidth <= \LowerWidth
+	\ifdim \UpperCenter > \LowerCenter
+%
+	\UpperAdjust=0pt
+	\RuleAdjust=\UpperCenter \advance\RuleAdjust by -\LowerCenter
+	\LowerAdjust=\RuleAdjust
+	\RuleWidth=\LowerWidth
+	\global\@LeftOffset=\LowerAdjust
+%
+	\else	% \UpperWidth <= \LowerWidth
+		% \UpperCenter <= \LowerCenter
+%
+	\UpperAdjust=\LowerCenter \advance\UpperAdjust by -\UpperCenter
+	\RuleAdjust=0pt
+	\LowerAdjust=0pt
+	\RuleWidth=\LowerWidth
+	\global\@LeftOffset=0pt
+%
+	\fi\fi
 % Make a box
-       \if@inferRule
-%
-       \setbox\ResultBox=\vbox{
-               \moveright \UpperAdjust \box\@UpperPart
-               \nointerlineskip \kern\inferLineSkip
-               \if@DoubleRule
-               \moveright \RuleAdjust \vbox{\hrule width\RuleWidth
-                       \kern 1pt\hrule width\RuleWidth}\relax
-               \else
-               \moveright \RuleAdjust \vbox{\hrule width\RuleWidth}\relax
-               \fi
-               \nointerlineskip \kern\inferLineSkip
-               \moveright \LowerAdjust \box\@LowerPart }\relax
-%
-       \@ifEmpty{#1}{}{\relax
-%
-       \HLabelAdjust=\wd\ResultBox     \advance\HLabelAdjust by -\RuleAdjust
-       \advance\HLabelAdjust by -\RuleWidth
-       \WidthAdjust=\HLabelAdjust
-       \advance\WidthAdjust by -\inferLabelSkip
-       \advance\WidthAdjust by -\wd\@LabelPart
-       \ifdim \WidthAdjust < 0pt \WidthAdjust=0pt \fi
-%
-       \VLabelAdjust=\dp\@LabelPart
-       \advance\VLabelAdjust by -\ht\@LabelPart
-       \VLabelAdjust=0.5\VLabelAdjust  \advance\VLabelAdjust by \LowerHeight
-       \advance\VLabelAdjust by \inferLineSkip
-%
-       \setbox\ResultBox=\hbox{\box\ResultBox
-               \kern -\HLabelAdjust \kern\inferLabelSkip
-               \raise\VLabelAdjust \box\@LabelPart \kern\WidthAdjust}\relax
-%
-       }\relax % end @ifEmpty
-%
-       \else % \@inferRulefalse
-%
-       \setbox\ResultBox=\vbox{
-               \moveright \UpperAdjust \box\@UpperPart
-               \nointerlineskip \kern\inferLineSkip
-               \moveright \LowerAdjust \hbox{\unhbox\@LowerPart
-                       \@ifEmpty{#1}{}{\relax
-                       \kern\inferLabelSkip \unhbox\@LabelPart}}}\relax
-       \fi
-%
-       \global\@RightOffset=\wd\ResultBox
-       \global\advance\@RightOffset by -\@LeftOffset
-       \global\advance\@RightOffset by -\LowerWidth
-       \if@ReturnLeftOffset \else \global\@LeftOffset=\@SavedLeftOffset \fi
-%
-       \box\ResultBox
-       \@RestoreMath
+	\if@inferRule
+%
+	\setbox\ResultBox=\vbox{
+		\moveright \UpperAdjust \box\@UpperPart
+		\nointerlineskip \kern\inferLineSkip
+		\if@DoubleRule
+		\moveright \RuleAdjust \vbox{\hrule width\RuleWidth
+			\kern 1pt\hrule width\RuleWidth}\relax
+		\else
+		\moveright \RuleAdjust \vbox{\hrule width\RuleWidth}\relax
+		\fi
+		\nointerlineskip \kern\inferLineSkip
+		\moveright \LowerAdjust \box\@LowerPart }\relax
+%
+	\@ifEmpty{#1}{}{\relax
+%
+	\HLabelAdjust=\wd\ResultBox	\advance\HLabelAdjust by -\RuleAdjust
+	\advance\HLabelAdjust by -\RuleWidth
+	\WidthAdjust=\HLabelAdjust
+	\advance\WidthAdjust by -\inferLabelSkip
+	\advance\WidthAdjust by -\wd\@LabelPart
+	\ifdim \WidthAdjust < 0pt \WidthAdjust=0pt \fi
+%
+	\VLabelAdjust=\dp\@LabelPart
+	\advance\VLabelAdjust by -\ht\@LabelPart
+	\VLabelAdjust=0.5\VLabelAdjust	\advance\VLabelAdjust by \LowerHeight
+	\advance\VLabelAdjust by \inferLineSkip
+%
+	\setbox\ResultBox=\hbox{\box\ResultBox
+		\kern -\HLabelAdjust \kern\inferLabelSkip
+		\raise\VLabelAdjust \box\@LabelPart \kern\WidthAdjust}\relax
+%
+	}\relax % end @ifEmpty
+%
+	\else % \@inferRulefalse
+%
+	\setbox\ResultBox=\vbox{
+		\moveright \UpperAdjust \box\@UpperPart
+		\nointerlineskip \kern\inferLineSkip
+		\moveright \LowerAdjust \hbox{\unhbox\@LowerPart
+			\@ifEmpty{#1}{}{\relax
+			\kern\inferLabelSkip \unhbox\@LabelPart}}}\relax
+	\fi
+%
+	\global\@RightOffset=\wd\ResultBox
+	\global\advance\@RightOffset by -\@LeftOffset
+	\global\advance\@RightOffset by -\LowerWidth
+	\if@ReturnLeftOffset \else \global\@LeftOffset=\@SavedLeftOffset \fi
+%
+	\box\ResultBox
 }