Repaired output of marginal comments in ML antiquotation.
% 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)% % This program is free software; you can redistribute it or modify% it under the terms of the GNU General Public License as published by% the Free Software Foundation; either versions 1, or (at your option)% any later version.% % This program is distributed in the hope that it will be useful% but WITHOUT ANY WARRANTY; without even the implied warranty of% 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}.%% The following macros are available:%% In all the following macros, all the arguments such as% <Lowers> and <Uppers> are processed in math mode.%% \infer<Lower><Uppers>% draws an inference.%% 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[<Label>]<Lower><Uppers>% draws an inference labeled with <Label>.%% \infer*<Lower><Uppers>% draws a many step deduction.%% \infer*[<Label>]<Lower><Uppers>% draws a many step deduction labeled with <Label>.%% \infer=<Lower><Uppers>% draws a double-ruled deduction.%% \infer=[<Label>]<Lower><Uppers>% draws a double-ruled deduction labeled with <Label>.%% \deduce<Lower><Uppers>% draws an inference without a rule.%% \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}% }%% Style Parameters\newdimen\inferLineSkip \inferLineSkip=2pt\newdimen\inferLabelSkip \inferLabelSkip=5pt\def\inferTabSkip{\quad}% Variables\newdimen\@LeftOffset % global\newdimen\@RightOffset % global\newdimen\@SavedLeftOffset % safe from users\newdimen\UpperWidth\newdimen\LowerWidth\newdimen\LowerHeight\newdimen\UpperLeftOffset\newdimen\UpperRightOffset\newdimen\UpperCenter\newdimen\LowerCenter\newdimen\UpperAdjust\newdimen\RuleAdjust\newdimen\LowerAdjust\newdimen\RuleWidth\newdimen\HLabelAdjust\newdimen\VLabelAdjust\newdimen\WidthAdjust\newbox\@UpperPart\newbox\@LowerPart\newbox\@LabelPart\newbox\ResultBox% 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.% 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% Renaming @ifnextchar and @ifnch of LaTeX2e to @IFnextchar and @IFnch.\def\@IFnextchar#1#2#3{% \let\reserved@e=#1\def\reserved@a{#2}\def\reserved@b{#3}\futurelet \reserved@c\@IFnch}\def\@IFnch{\ifx \reserved@c \@sptoken \let\reserved@d\@xifnch \else \ifx \reserved@c \reserved@e\let\reserved@d\reserved@a\else \let\reserved@d\reserved@b\fi \fi \reserved@d}\def\@ifEmpty#1#2#3{\def\@tempa{\@empty}\def\@tempb{#1}\relax \ifx \@tempa \@tempb #2\else #3\fi }\def\infer{\@SaveMath \@IFnextchar *{\@inferSteps}{\relax \@IFnextchar ={\@inferDoubleRule}{\@inferOneStep}}}\def\@inferOneStep{\@inferRuletrue \@DoubleRulefalse \@IFnextchar [{\@infer}{\@infer[\@empty]}}\def\@inferDoubleRule={\@inferRuletrue \@DoubleRuletrue \@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]}}% \@deduce<Proof Label>[<Proof>]<Lower><Uppers>\def\@deduce#1[#2]#3#4{\@inferRulefalse \@infer[\@empty]{#3}{\@SaveMath \@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.%% 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% 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% 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}