diff options
author | Karl Berry <karl@freefriends.org> | 2006-01-13 00:03:31 +0000 |
---|---|---|
committer | Karl Berry <karl@freefriends.org> | 2006-01-13 00:03:31 +0000 |
commit | dba09c751a6f9d8fd641a41c73fc590634c4eb19 (patch) | |
tree | d37e91304341af3657b00977c274c6bf2b549c5a /Master/texmf-dist/tex | |
parent | ef0a1845d1d9d71acc3172564f4423057a077ca4 (diff) |
proof
git-svn-id: svn://tug.org/texlive/trunk@1222 c570f23f-e606-0410-a88d-b1316a301751
Diffstat (limited to 'Master/texmf-dist/tex')
-rw-r--r-- | Master/texmf-dist/tex/latex/proof/proof.sty | 278 |
1 files changed, 278 insertions, 0 deletions
diff --git a/Master/texmf-dist/tex/latex/proof/proof.sty b/Master/texmf-dist/tex/latex/proof/proof.sty new file mode 100644 index 00000000000..e32030018a1 --- /dev/null +++ b/Master/texmf-dist/tex/latex/proof/proof.sty @@ -0,0 +1,278 @@ +% 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 +} |