|
0
|
1 |
% Mathpartir --- Math Paragraph for Typesetting Inference Rules
|
|
|
2 |
%
|
|
|
3 |
% Copyright (C) 2001, 2002, 2003, 2004, 2005 Didier Rémy
|
|
|
4 |
%
|
|
|
5 |
% Author : Didier Remy
|
|
|
6 |
% Version : 1.2.0
|
|
|
7 |
% Bug Reports : to author
|
|
|
8 |
% Web Site : http://pauillac.inria.fr/~remy/latex/
|
|
|
9 |
%
|
|
|
10 |
% Mathpartir is free software; you can redistribute it and/or modify
|
|
|
11 |
% it under the terms of the GNU General Public License as published by
|
|
|
12 |
% the Free Software Foundation; either version 2, or (at your option)
|
|
|
13 |
% any later version.
|
|
|
14 |
%
|
|
|
15 |
% Mathpartir is distributed in the hope that it will be useful,
|
|
|
16 |
% but WITHOUT ANY WARRANTY; without even the implied warranty of
|
|
|
17 |
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
|
|
18 |
% GNU General Public License for more details
|
|
|
19 |
% (http://pauillac.inria.fr/~remy/license/GPL).
|
|
|
20 |
%
|
|
|
21 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
22 |
% File mathpartir.sty (LaTeX macros)
|
|
|
23 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
24 |
|
|
|
25 |
\NeedsTeXFormat{LaTeX2e}
|
|
|
26 |
\ProvidesPackage{mathpartir}
|
|
|
27 |
[2005/12/20 version 1.2.0 Math Paragraph for Typesetting Inference Rules]
|
|
|
28 |
|
|
|
29 |
%%
|
|
|
30 |
|
|
|
31 |
%% Identification
|
|
|
32 |
%% Preliminary declarations
|
|
|
33 |
|
|
|
34 |
\RequirePackage {keyval}
|
|
|
35 |
|
|
|
36 |
%% Options
|
|
|
37 |
%% More declarations
|
|
|
38 |
|
|
|
39 |
%% PART I: Typesetting maths in paragraphe mode
|
|
|
40 |
|
|
|
41 |
%% \newdimen \mpr@tmpdim
|
|
|
42 |
%% Dimens are a precious ressource. Uses seems to be local.
|
|
|
43 |
\let \mpr@tmpdim \@tempdima
|
|
|
44 |
|
|
|
45 |
% To ensure hevea \hva compatibility, \hva should expands to nothing
|
|
|
46 |
% in mathpar or in inferrule
|
|
|
47 |
\let \mpr@hva \empty
|
|
|
48 |
|
|
|
49 |
%% normal paragraph parametters, should rather be taken dynamically
|
|
|
50 |
\def \mpr@savepar {%
|
|
|
51 |
\edef \MathparNormalpar
|
|
|
52 |
{\noexpand \lineskiplimit \the\lineskiplimit
|
|
|
53 |
\noexpand \lineskip \the\lineskip}%
|
|
|
54 |
}
|
|
|
55 |
|
|
|
56 |
\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em}
|
|
|
57 |
\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}
|
|
|
58 |
\def \mpr@lineskip {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
|
|
|
59 |
\let \MathparLineskip \mpr@lineskip
|
|
|
60 |
\def \mpr@paroptions {\MathparLineskip}
|
|
|
61 |
\let \mpr@prebindings \relax
|
|
|
62 |
|
|
|
63 |
\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em
|
|
|
64 |
|
|
|
65 |
\def \mpr@goodbreakand
|
|
|
66 |
{\hskip -\mpr@andskip \penalty -1000\hskip \mpr@andskip}
|
|
|
67 |
\def \mpr@and {\hskip \mpr@andskip}
|
|
|
68 |
\def \mpr@andcr {\penalty 50\mpr@and}
|
|
|
69 |
\def \mpr@cr {\penalty -10000\mpr@and}
|
|
|
70 |
\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10}
|
|
|
71 |
|
|
|
72 |
\def \mpr@bindings {%
|
|
|
73 |
\let \and \mpr@andcr
|
|
|
74 |
\let \par \mpr@andcr
|
|
|
75 |
\let \\\mpr@cr
|
|
|
76 |
\let \eqno \mpr@eqno
|
|
|
77 |
\let \hva \mpr@hva
|
|
|
78 |
}
|
|
|
79 |
\let \MathparBindings \mpr@bindings
|
|
|
80 |
|
|
|
81 |
% \@ifundefined {ignorespacesafterend}
|
|
|
82 |
% {\def \ignorespacesafterend {\aftergroup \ignorespaces}
|
|
|
83 |
|
|
|
84 |
\newenvironment{mathpar}[1][]
|
|
|
85 |
{$$\mpr@savepar \parskip 0em \hsize \linewidth \centering
|
|
|
86 |
\vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else
|
|
|
87 |
\noindent $\displaystyle\fi
|
|
|
88 |
\MathparBindings}
|
|
|
89 |
{\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend}
|
|
|
90 |
|
|
|
91 |
\newenvironment{mathparpagebreakable}[1][]
|
|
|
92 |
{\begingroup
|
|
|
93 |
\par
|
|
|
94 |
\mpr@savepar \parskip 0em \hsize \linewidth \centering
|
|
|
95 |
\mpr@prebindings \mpr@paroptions #1%
|
|
|
96 |
\vskip \abovedisplayskip \vskip -\lineskip%
|
|
|
97 |
\ifmmode \else $\displaystyle\fi
|
|
|
98 |
\MathparBindings
|
|
|
99 |
}
|
|
|
100 |
{\unskip
|
|
|
101 |
\ifmmode $\fi \par\endgroup
|
|
|
102 |
\vskip \belowdisplayskip
|
|
|
103 |
\noindent
|
|
|
104 |
\ignorespacesafterend}
|
|
|
105 |
|
|
|
106 |
% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum
|
|
|
107 |
% \wd0 < \hsize $$\box0$$\else \bmathpar #1\emathpar \fi}
|
|
|
108 |
|
|
|
109 |
%%% HOV BOXES
|
|
|
110 |
|
|
|
111 |
\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip
|
|
|
112 |
\vbox \bgroup \tabskip 0em \let \\ \cr
|
|
|
113 |
\halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup
|
|
|
114 |
\egroup}
|
|
|
115 |
|
|
|
116 |
\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize
|
|
|
117 |
\box0\else \mathvbox {#1}\fi}
|
|
|
118 |
|
|
|
119 |
|
|
|
120 |
%% Part II -- operations on lists
|
|
|
121 |
|
|
|
122 |
\newtoks \mpr@lista
|
|
|
123 |
\newtoks \mpr@listb
|
|
|
124 |
|
|
|
125 |
\long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
|
|
|
126 |
{#2}\edef #2{\the \mpr@lista \the \mpr@listb}}
|
|
|
127 |
|
|
|
128 |
\long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
|
|
|
129 |
{#2}\edef #2{\the \mpr@listb\the\mpr@lista}}
|
|
|
130 |
|
|
|
131 |
\long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb
|
|
|
132 |
\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}
|
|
|
133 |
|
|
|
134 |
\def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}
|
|
|
135 |
\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}
|
|
|
136 |
|
|
|
137 |
\def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}
|
|
|
138 |
\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}}
|
|
|
139 |
|
|
|
140 |
\def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}%
|
|
|
141 |
\mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the
|
|
|
142 |
\mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty
|
|
|
143 |
\def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop
|
|
|
144 |
\mpr@flatten \mpr@all \mpr@to \mpr@one
|
|
|
145 |
\expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof
|
|
|
146 |
\mpr@all \mpr@stripend
|
|
|
147 |
\ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi
|
|
|
148 |
\ifx 1\mpr@isempty
|
|
|
149 |
\repeat
|
|
|
150 |
}
|
|
|
151 |
|
|
|
152 |
\def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty
|
|
|
153 |
\def \\##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp}
|
|
|
154 |
|
|
|
155 |
%% Part III -- Type inference rules
|
|
|
156 |
|
|
|
157 |
\newif \if@premisse
|
|
|
158 |
\newbox \mpr@hlist
|
|
|
159 |
\newbox \mpr@vlist
|
|
|
160 |
\newif \ifmpr@center \mpr@centertrue
|
|
|
161 |
\def \mpr@htovlist {%
|
|
|
162 |
\setbox \mpr@hlist
|
|
|
163 |
\hbox {\strut
|
|
|
164 |
\ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
|
|
|
165 |
\unhbox \mpr@hlist}%
|
|
|
166 |
\setbox \mpr@vlist
|
|
|
167 |
\vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
|
|
|
168 |
\else \unvbox \mpr@vlist \box \mpr@hlist
|
|
|
169 |
\fi}%
|
|
|
170 |
}
|
|
|
171 |
% OLD version
|
|
|
172 |
% \def \mpr@htovlist {%
|
|
|
173 |
% \setbox \mpr@hlist
|
|
|
174 |
% \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}%
|
|
|
175 |
% \setbox \mpr@vlist
|
|
|
176 |
% \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
|
|
|
177 |
% \else \unvbox \mpr@vlist \box \mpr@hlist
|
|
|
178 |
% \fi}%
|
|
|
179 |
% }
|
|
|
180 |
|
|
|
181 |
\def \mpr@item #1{$\displaystyle #1$}
|
|
|
182 |
\def \mpr@sep{2em}
|
|
|
183 |
\def \mpr@blank { }
|
|
|
184 |
\def \mpr@hovbox #1#2{\hbox
|
|
|
185 |
\bgroup
|
|
|
186 |
\ifx #1T\@premissetrue
|
|
|
187 |
\else \ifx #1B\@premissefalse
|
|
|
188 |
\else
|
|
|
189 |
\PackageError{mathpartir}
|
|
|
190 |
{Premisse orientation should either be T or B}
|
|
|
191 |
{Fatal error in Package}%
|
|
|
192 |
\fi \fi
|
|
|
193 |
\def \@test {#2}\ifx \@test \mpr@blank\else
|
|
|
194 |
\setbox \mpr@hlist \hbox {}%
|
|
|
195 |
\setbox \mpr@vlist \vbox {}%
|
|
|
196 |
\if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi
|
|
|
197 |
\let \@hvlist \empty \let \@rev \empty
|
|
|
198 |
\mpr@tmpdim 0em
|
|
|
199 |
\expandafter \mpr@makelist #2\mpr@to \mpr@flat
|
|
|
200 |
\if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi
|
|
|
201 |
\def \\##1{%
|
|
|
202 |
\def \@test {##1}\ifx \@test \empty
|
|
|
203 |
\mpr@htovlist
|
|
|
204 |
\mpr@tmpdim 0em %%% last bug fix not extensively checked
|
|
|
205 |
\else
|
|
|
206 |
\setbox0 \hbox{\mpr@item {##1}}\relax
|
|
|
207 |
\advance \mpr@tmpdim by \wd0
|
|
|
208 |
%\mpr@tmpdim 1.02\mpr@tmpdim
|
|
|
209 |
\ifnum \mpr@tmpdim < \hsize
|
|
|
210 |
\ifnum \wd\mpr@hlist > 0
|
|
|
211 |
\if@premisse
|
|
|
212 |
\setbox \mpr@hlist
|
|
|
213 |
\hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}%
|
|
|
214 |
\else
|
|
|
215 |
\setbox \mpr@hlist
|
|
|
216 |
\hbox {\unhbox \mpr@hlist \hskip \mpr@sep \unhbox0}%
|
|
|
217 |
\fi
|
|
|
218 |
\else
|
|
|
219 |
\setbox \mpr@hlist \hbox {\unhbox0}%
|
|
|
220 |
\fi
|
|
|
221 |
\else
|
|
|
222 |
\ifnum \wd \mpr@hlist > 0
|
|
|
223 |
\mpr@htovlist
|
|
|
224 |
\mpr@tmpdim \wd0
|
|
|
225 |
\fi
|
|
|
226 |
\setbox \mpr@hlist \hbox {\unhbox0}%
|
|
|
227 |
\fi
|
|
|
228 |
\advance \mpr@tmpdim by \mpr@sep
|
|
|
229 |
\fi
|
|
|
230 |
}%
|
|
|
231 |
\@rev
|
|
|
232 |
\mpr@htovlist
|
|
|
233 |
\ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
|
|
|
234 |
\fi
|
|
|
235 |
\egroup
|
|
|
236 |
}
|
|
|
237 |
|
|
|
238 |
%%% INFERENCE RULES
|
|
|
239 |
|
|
|
240 |
\@ifundefined{@@over}{%
|
|
|
241 |
\let\@@over\over % fallback if amsmath is not loaded
|
|
|
242 |
\let\@@overwithdelims\overwithdelims
|
|
|
243 |
\let\@@atop\atop \let\@@atopwithdelims\atopwithdelims
|
|
|
244 |
\let\@@above\above \let\@@abovewithdelims\abovewithdelims
|
|
|
245 |
}{}
|
|
|
246 |
|
|
|
247 |
%% The default
|
|
|
248 |
|
|
|
249 |
\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
|
|
|
250 |
$\displaystyle {#1\mpr@over #2}$}}
|
|
|
251 |
\def \mpr@@nofraction #1#2{\hbox {\advance \hsize by -0.5em
|
|
|
252 |
$\displaystyle {#1\@@atop #2}$}}
|
|
|
253 |
|
|
|
254 |
\let \mpr@fraction \mpr@@fraction
|
|
|
255 |
|
|
|
256 |
%% A generic solution to arrow
|
|
|
257 |
|
|
|
258 |
\def \mpr@make@fraction #1#2#3#4#5{\hbox {%
|
|
|
259 |
\def \mpr@tail{#1}%
|
|
|
260 |
\def \mpr@body{#2}%
|
|
|
261 |
\def \mpr@head{#3}%
|
|
|
262 |
\setbox1=\hbox{$#4$}\setbox2=\hbox{$#5$}%
|
|
|
263 |
\setbox3=\hbox{$\mkern -3mu\mpr@body\mkern -3mu$}%
|
|
|
264 |
\setbox3=\hbox{$\mkern -3mu \mpr@body\mkern -3mu$}%
|
|
|
265 |
\dimen0=\dp1\advance\dimen0 by \ht3\relax\dp1\dimen0\relax
|
|
|
266 |
\dimen0=\ht2\advance\dimen0 by \dp3\relax\ht2\dimen0\relax
|
|
|
267 |
\setbox0=\hbox {$\box1 \@@atop \box2$}%
|
|
|
268 |
\dimen0=\wd0\box0
|
|
|
269 |
\box0 \hskip -\dimen0\relax
|
|
|
270 |
\hbox to \dimen0 {$%
|
|
|
271 |
\mathrel{\mpr@tail}\joinrel
|
|
|
272 |
\xleaders\hbox{\copy3}\hfil\joinrel\mathrel{\mpr@head}%
|
|
|
273 |
$}}}
|
|
|
274 |
|
|
|
275 |
%% Old stuff should be removed in next version
|
|
|
276 |
\def \mpr@@nothing #1#2
|
|
|
277 |
{$\lower 0.01pt \mpr@@nofraction {#1}{#2}$}
|
|
|
278 |
\def \mpr@@reduce #1#2{\hbox
|
|
|
279 |
{$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}}
|
|
|
280 |
\def \mpr@@rewrite #1#2#3{\hbox
|
|
|
281 |
{$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}}
|
|
|
282 |
\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}}
|
|
|
283 |
|
|
|
284 |
\def \mpr@empty {}
|
|
|
285 |
\def \mpr@inferrule
|
|
|
286 |
{\bgroup
|
|
|
287 |
\ifnum \linewidth<\hsize \hsize \linewidth\fi
|
|
|
288 |
\mpr@rulelineskip
|
|
|
289 |
\let \and \qquad
|
|
|
290 |
\let \hva \mpr@hva
|
|
|
291 |
\let \@rulename \mpr@empty
|
|
|
292 |
\let \@rule@options \mpr@empty
|
|
|
293 |
\let \mpr@over \@@over
|
|
|
294 |
\mpr@inferrule@}
|
|
|
295 |
\newcommand {\mpr@inferrule@}[3][]
|
|
|
296 |
{\everymath={\displaystyle}%
|
|
|
297 |
\def \@test {#2}\ifx \empty \@test
|
|
|
298 |
\setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%
|
|
|
299 |
\else
|
|
|
300 |
\def \@test {#3}\ifx \empty \@test
|
|
|
301 |
\setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}%
|
|
|
302 |
\else
|
|
|
303 |
\setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}%
|
|
|
304 |
\fi \fi
|
|
|
305 |
\def \@test {#1}\ifx \@test\empty \box0
|
|
|
306 |
\else \vbox
|
|
|
307 |
%%% Suggestion de Francois pour les etiquettes longues
|
|
|
308 |
%%% {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi
|
|
|
309 |
{\hbox {\RefTirName {#1}}\box0}\fi
|
|
|
310 |
\egroup}
|
|
|
311 |
|
|
|
312 |
\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}
|
|
|
313 |
|
|
|
314 |
% They are two forms
|
|
|
315 |
% \inferrule [label]{[premisses}{conclusions}
|
|
|
316 |
% or
|
|
|
317 |
% \inferrule* [options]{[premisses}{conclusions}
|
|
|
318 |
%
|
|
|
319 |
% Premisses and conclusions are lists of elements separated by \\
|
|
|
320 |
% Each \\ produces a break, attempting horizontal breaks if possible,
|
|
|
321 |
% and vertical breaks if needed.
|
|
|
322 |
%
|
|
|
323 |
% An empty element obtained by \\\\ produces a vertical break in all cases.
|
|
|
324 |
%
|
|
|
325 |
% The former rule is aligned on the fraction bar.
|
|
|
326 |
% The optional label appears on top of the rule
|
|
|
327 |
% The second form to be used in a derivation tree is aligned on the last
|
|
|
328 |
% line of its conclusion
|
|
|
329 |
%
|
|
|
330 |
% The second form can be parameterized, using the key=val interface. The
|
|
|
331 |
% folloiwng keys are recognized:
|
|
|
332 |
%
|
|
|
333 |
% width set the width of the rule to val
|
|
|
334 |
% narrower set the width of the rule to val\hsize
|
|
|
335 |
% before execute val at the beginning/left
|
|
|
336 |
% lab put a label [Val] on top of the rule
|
|
|
337 |
% lskip add negative skip on the right
|
|
|
338 |
% left put a left label [Val]
|
|
|
339 |
% Left put a left label [Val], ignoring its width
|
|
|
340 |
% right put a right label [Val]
|
|
|
341 |
% Right put a right label [Val], ignoring its width
|
|
|
342 |
% leftskip skip negative space on the left-hand side
|
|
|
343 |
% rightskip skip negative space on the right-hand side
|
|
|
344 |
% vdots lift the rule by val and fill vertical space with dots
|
|
|
345 |
% after execute val at the end/right
|
|
|
346 |
%
|
|
|
347 |
% Note that most options must come in this order to avoid strange
|
|
|
348 |
% typesetting (in particular leftskip must preceed left and Left and
|
|
|
349 |
% rightskip must follow Right or right; vdots must come last
|
|
|
350 |
% or be only followed by rightskip.
|
|
|
351 |
%
|
|
|
352 |
|
|
|
353 |
%% Keys that make sence in all kinds of rules
|
|
|
354 |
\def \mprset #1{\setkeys{mprset}{#1}}
|
|
|
355 |
\define@key {mprset}{andskip}[]{\mpr@andskip=#1}
|
|
|
356 |
\define@key {mprset}{lineskip}[]{\lineskip=#1}
|
|
|
357 |
\define@key {mprset}{flushleft}[]{\mpr@centerfalse}
|
|
|
358 |
\define@key {mprset}{center}[]{\mpr@centertrue}
|
|
|
359 |
\define@key {mprset}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
|
|
|
360 |
\define@key {mprset}{atop}[]{\let \mpr@fraction \mpr@@nofraction}
|
|
|
361 |
\define@key {mprset}{myfraction}[]{\let \mpr@fraction #1}
|
|
|
362 |
\define@key {mprset}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
|
|
|
363 |
\define@key {mprset}{sep}{\def\mpr@sep{#1}}
|
|
|
364 |
|
|
|
365 |
\newbox \mpr@right
|
|
|
366 |
\define@key {mpr}{flushleft}[]{\mpr@centerfalse}
|
|
|
367 |
\define@key {mpr}{center}[]{\mpr@centertrue}
|
|
|
368 |
\define@key {mpr}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
|
|
|
369 |
\define@key {mpr}{myfraction}[]{\let \mpr@fraction #1}
|
|
|
370 |
\define@key {mpr}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
|
|
|
371 |
\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
|
|
|
372 |
\advance \hsize by -\wd0\box0}
|
|
|
373 |
\define@key {mpr}{width}{\hsize #1}
|
|
|
374 |
\define@key {mpr}{sep}{\def\mpr@sep{#1}}
|
|
|
375 |
\define@key {mpr}{before}{#1}
|
|
|
376 |
\define@key {mpr}{lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
|
|
|
377 |
\define@key {mpr}{Lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
|
|
|
378 |
\define@key {mpr}{narrower}{\hsize #1\hsize}
|
|
|
379 |
\define@key {mpr}{leftskip}{\hskip -#1}
|
|
|
380 |
\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}
|
|
|
381 |
\define@key {mpr}{rightskip}
|
|
|
382 |
{\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}}
|
|
|
383 |
\define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax
|
|
|
384 |
\advance \hsize by -\wd0\box0}
|
|
|
385 |
\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
|
|
|
386 |
\advance \hsize by -\wd0\box0}
|
|
|
387 |
\define@key {mpr}{Left}{\llap{$\TirName {#1}\;$}}
|
|
|
388 |
\define@key {mpr}{right}
|
|
|
389 |
{\setbox0 \hbox {$\;\TirName {#1}$}\relax \advance \hsize by -\wd0
|
|
|
390 |
\setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
|
|
|
391 |
\define@key {mpr}{RIGHT}
|
|
|
392 |
{\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0
|
|
|
393 |
\setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
|
|
|
394 |
\define@key {mpr}{Right}
|
|
|
395 |
{\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\TirName {#1}$}}}
|
|
|
396 |
\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}
|
|
|
397 |
\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}
|
|
|
398 |
|
|
|
399 |
\newcommand \mpr@inferstar@ [3][]{\setbox0
|
|
|
400 |
\hbox {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax
|
|
|
401 |
\setbox \mpr@right \hbox{}%
|
|
|
402 |
$\setkeys{mpr}{#1}%
|
|
|
403 |
\ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else
|
|
|
404 |
\mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi
|
|
|
405 |
\box \mpr@right \mpr@vdots$}
|
|
|
406 |
\setbox1 \hbox {\strut}
|
|
|
407 |
\@tempdima \dp0 \advance \@tempdima by -\dp1
|
|
|
408 |
\raise \@tempdima \box0}
|
|
|
409 |
|
|
|
410 |
\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}
|
|
|
411 |
\newcommand \mpr@err@skipargs[3][]{}
|
|
|
412 |
\def \mpr@inferstar*{\ifmmode
|
|
|
413 |
\let \@do \mpr@inferstar@
|
|
|
414 |
\else
|
|
|
415 |
\let \@do \mpr@err@skipargs
|
|
|
416 |
\PackageError {mathpartir}
|
|
|
417 |
{\string\inferrule* can only be used in math mode}{}%
|
|
|
418 |
\fi \@do}
|
|
|
419 |
|
|
|
420 |
|
|
|
421 |
%%% Exports
|
|
|
422 |
|
|
|
423 |
% Envirnonment mathpar
|
|
|
424 |
|
|
|
425 |
\let \inferrule \mpr@infer
|
|
|
426 |
|
|
|
427 |
% make a short name \infer is not already defined
|
|
|
428 |
\@ifundefined {infer}{\let \infer \mpr@infer}{}
|
|
|
429 |
|
|
|
430 |
\def \TirNameStyle #1{\small \textsc{#1}}
|
|
|
431 |
\def \tir@name #1{\hbox {\small \TirNameStyle{#1}}}
|
|
|
432 |
\let \TirName \tir@name
|
|
|
433 |
\let \DefTirName \TirName
|
|
|
434 |
\let \RefTirName \TirName
|
|
|
435 |
|
|
|
436 |
%%% Other Exports
|
|
|
437 |
|
|
|
438 |
% \let \listcons \mpr@cons
|
|
|
439 |
% \let \listsnoc \mpr@snoc
|
|
|
440 |
% \let \listhead \mpr@head
|
|
|
441 |
% \let \listmake \mpr@makelist
|
|
|
442 |
|
|
|
443 |
|
|
|
444 |
|
|
|
445 |
|
|
|
446 |
\endinput
|