helm/ocaml/tactics/doc/infernce.sty

   1 %%
   2 %% This is file `infernce.sty',
   3 %% generated with the docstrip utility.
   4 %%
   5 %% The original source files were:
   6 %%
   7 %% semantic.dtx  (with options: `allOptions,inference')
   8 %%
   9 %% IMPORTANT NOTICE:
  10 %%
  11 %% For the copyright see the source file.
  12 %%
  13 %% Any modified versions of this file must be renamed
  14 %% with new filenames distinct from infernce.sty.
  15 %%
  16 %% For distribution of the original source see the terms
  17 %% for copying and modification in the file semantic.dtx.
  18 %%
  19 %% This generated file may be distributed as long as the
  20 %% original source files, as listed above, are part of the
  21 %% same distribution. (The sources need not necessarily be
  22 %% in the same archive or directory.)
  23 %%
  24 %% semantic.dtx  (c)1995--2002 Peter M^^f8ller Neergaard and
  25 %%                             Arne John Glenstrup
  26 %%
  27 \expandafter\ifx\csname sem@nticsLoader\endcsname\relax
  28   \PackageError{semantic}{%
  29     This file should not be loaded directly}
  30     {%
  31       This file is an option of the semantic package.  It should not be
  32         loaded directly\MessageBreak
  33       but by using \protect\usepackage{semantic} in your document
  34         preamble.\MessageBreak
  35       No commands are defined.\MessageBreak
  36      Type <return> to proceed.
  37     }%
  38 \else
  39 \TestForConflict{\@@tempa,\@@tempb,\@adjustPremises,\@inference}
  40 \TestForConflict{\@inferenceBack,\@inferenceFront,\@inferenceOrPremis}
  41 \TestForConflict{\@premises,\@processInference,\@processPremiseLine}
  42 \TestForConflict{\@setLengths,\inference,\predicate,\predicatebegin}
  43 \TestForConflict{\predicateend,\setnamespace,\setpremisesend}
  44 \TestForConflict{\setpremisesspace,\@makeLength,\@@space}
  45 \TestForConflict{\@@aLineBox,\if@@shortDivider}
  46 \newtoks\@@tempa
  47 \newtoks\@@tempb
  48 \newcommand{\@makeLength}[4]{
  49   \@@tempa=\expandafter{\csname @@#2\endcsname}
  50   \@@tempb=\expandafter{\csname @set#2\endcsname} %
  51   \expandafter \newlength \the\@@tempa
  52   \expandafter \newcommand \the\@@tempb {}
  53   \expandafter \newcommand \csname set#1\endcsname[1]{}
  54   \expandafter \xdef \csname set#1\endcsname##1%
  55     {{\dimen0=##1}%
  56       \noexpand\renewcommand{\the\@@tempb}{%
  57         \noexpand\setlength{\the \@@tempa}{##1 #4}}%
  58     }%
  59   \csname set#1\endcsname{#3}
  60   \@@tempa=\expandafter{\@setLengths} %
  61   \edef\@setLengths{\the\@@tempa \the\@@tempb} %
  62   }
  63
  64 \newcommand{\@setLengths}{%
  65   \setlength{\baselineskip}{1.166em}%
  66   \setlength{\lineskip}{1pt}%
  67   \setlength{\lineskiplimit}{1pt}}
  68 \@makeLength{premisesspace}{pSpace}{1.5em}{plus 1fil}
  69 \@makeLength{premisesend}{pEnd}{.75em}{plus 0.5fil}
  70 \@makeLength{namespace}{nSpace}{.5em}{}
  71 \newbox\@@aLineBox
  72 \newif\if@@shortDivider
  73 \newcommand{\@@space}{ }
  74 \newcommand{\predicate}[1]{\predicatebegin #1\predicateend}
  75 \newcommand{\predicatebegin}{$}
  76 \newcommand{\predicateend}{$}
  77 \def\inference{%
  78   \@@shortDividerfalse
  79   \expandafter\hbox\bgroup
  80   \@ifstar{\@@shortDividertrue\@inferenceFront}%
  81           \@inferenceFront
  82 }
  83 \def\@inferenceFront{%
  84   \@ifnextchar[%
  85      {\@inferenceFrontName}%
  86      {\@inferenceMiddle}%
  87 }
  88 \def\@inferenceFrontName[#1]{%
  89   \setbox3=\hbox{\footnotesize #1}%
  90   \ifdim \wd3 > \z@
  91     \unhbox3%
  92     \hskip\@@nSpace
  93   \fi
  94   \@inferenceMiddle
  95 }
  96 \long\def\@inferenceMiddle#1{%
  97   \@setLengths%
  98   \setbox\@@pBox=
  99     \vbox{%
 100       \@premises{#1}%
 101       \unvbox\@@pBox
 102     }%
 103   \@inferenceBack
 104 }
 105 \long\def\@inferenceBack#1{%
 106   \setbox\@@cBox=%
 107    \hbox{\hskip\@@pEnd \predicate{\ignorespaces#1}\unskip\hskip\@@pEnd}%
 108   \setbox1=\hbox{$ $}%
 109   \setbox\@@pBox=\vtop{\unvbox\@@pBox
 110                  \vskip 4\fontdimen8\textfont3}%
 111   \setbox\@@cBox=\vbox{\vskip 4\fontdimen8\textfont3%
 112                  \box\@@cBox}%
 113   \if@@shortDivider
 114     \ifdim\wd\@@pBox >\wd\@@cBox%
 115       \dimen1=\wd\@@pBox%
 116     \else%
 117       \dimen1=\wd\@@cBox%
 118     \fi%
 119     \dimen0=\wd\@@cBox%
 120     \hbox to \dimen1{%
 121       \hss
 122       $\frac{\hbox to \dimen0{\hss\box\@@pBox\hss}}%
 123         {\box\@@cBox}$%
 124       \hss
 125     }%
 126   \else
 127     $\frac{\box\@@pBox}%
 128           {\box\@@cBox}$%
 129   \fi
 130   \@ifnextchar[%
 131      {\@inferenceBackName}%{}%
 132      {\egroup}
 133 }
 134 \def\@inferenceBackName[#1]{%
 135   \setbox3=\hbox{\footnotesize #1}%
 136   \ifdim \wd3 > \z@
 137     \hskip\@@nSpace
 138     \unhbox3%
 139   \fi
 140   \egroup
 141 }
 142 \newcommand{\@premises}[1]{%
 143   \setbox\@@pBox=\vbox{}%
 144   \dimen\@@maxwidth=\wd\@@cBox%
 145   \@processPremises #1\\\end%
 146   \@adjustPremises%
 147 }
 148 \newcommand{\@adjustPremises}{%
 149   \setbox\@@pBox=\vbox{%
 150     \@@moreLinestrue %
 151     \loop %
 152       \setbox\@@pBox=\vbox{%
 153         \unvbox\@@pBox %
 154         \global\setbox\@@aLineBox=\lastbox %
 155       }%
 156       \ifvoid\@@aLineBox %
 157         \@@moreLinesfalse %
 158       \else %
 159         \hbox to \dimen\@@maxwidth{\unhbox\@@aLineBox}%
 160       \fi %
 161     \if@@moreLines\repeat%
 162   }%
 163 }
 164 \def\@processPremises#1\\#2\end{%
 165   \setbox\@@pLineBox=\hbox{}%
 166   \@processPremiseLine #1&\end%
 167   \setbox\@@pLineBox=\hbox{\unhbox\@@pLineBox \unskip}%
 168   \ifdim \wd\@@pLineBox > \z@ %
 169     \setbox\@@pLineBox=%
 170       \hbox{\hskip\@@pEnd \unhbox\@@pLineBox \hskip\@@pEnd}%
 171     \ifdim \wd\@@pLineBox > \dimen\@@maxwidth %
 172       \dimen\@@maxwidth=\wd\@@pLineBox %
 173     \fi %
 174     \setbox\@@pBox=\vbox{\box\@@pLineBox\unvbox\@@pBox}%
 175   \fi %
 176   \def\sem@tmp{#2}%
 177   \ifx \sem@tmp\empty \else %
 178     \@ReturnAfterFi{%
 179       \@processPremises #2\end %
 180     }%
 181   \fi%
 182 }
 183 \def\@processPremiseLine#1&#2\end{%
 184   \def\sem@tmp{#1}%
 185   \ifx \sem@tmp\empty \else%
 186     \ifx \sem@tmp\@@space \else%
 187     \setbox\@@pLineBox=%
 188       \hbox{\unhbox\@@pLineBox%
 189             \@inferenceOrPremis #1\inference\end%
 190             \hskip\@@pSpace}%
 191     \fi%
 192   \fi%
 193   \def\sem@tmp{#2}%
 194   \ifx \sem@tmp\empty \else%
 195     \@ReturnAfterFi{%
 196       \@processPremiseLine#2\end%
 197     }%
 198   \fi%
 199 }
 200 \def\@inferenceOrPremis#1\inference{%
 201   \@ifnext \end
 202     {\@dropnext{\predicate{\ignorespaces #1}\unskip}}%
 203     {\@processInference #1\inference}%
 204 }
 205 \def\@processInference#1\inference\end{%
 206   \ignorespaces #1%
 207   \setbox3=\lastbox
 208   \dimen3=\dp3
 209   \advance\dimen3 by -\fontdimen22\textfont2
 210   \advance\dimen3 by \fontdimen8\textfont3
 211   \expandafter\raise\dimen3\box3%
 212 }
 213 \long\def\@ReturnAfterFi#1\fi{\fi#1}
 214 \fi
 215 \endinput
 216 %%
 217 %% End of file `infernce.sty'.