Mercurial > hg > Papers > 2017 > atton-master

comparison paper/bussproofs.sty @ 34:9800586284e1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Writing expression ...
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Sat, 28 Jan 2017 09:46:02 +0900
parents
children
comparison
equal deleted inserted replaced
33:74a29a48575a 34:9800586284e1
1 %
2 \def\BPmessage{Proof Tree (bussproofs) style macros. Version 1.1.}
3 % bussproofs.sty. Version 1.1
4 % (c) 1994,1995,1996,2004,2005,2006, 2011.
5 % Copyright retained by Samuel R. Buss.
6 %
7 % ==== Legal statement: ====
8 % This work may be distributed and/or modified under the
9 % conditions of the LaTeX Project Public License, either version 1.3
10 % of this license or (at your option) any later version.
11 % The latest version of this license is in
12 % http://www.latex-project.org/lppl.txt.
13 % and version 1.3 or later is part of all distributions of LaTeX
14 % version 2005/12/1 or later.
15 %
16 % This work has the LPPL maintenance status 'maintained'.
17 %
18 % The Current Maintainer of the work is Sam Buss.
19 %
20 % This work consists of bussproofs.sty.
21 % =====
22 % Informal summary of legal situation:
23 % This software may be used and distributed freely, except that
24 % if you make changes, you must change the file name to be different
25 % than bussproofs.sty to avoid compatibility problems.
26 % The terms of the LaTeX Public License are the legally controlling terms
27 % and override any contradictory terms of the "informal situation".
28 %
29 % Please report comments and bugs to sbuss@ucsd.edu.
30 %
31 % Thanks to Felix Joachimski for making changes to let these macros
32 % work in plain TeX in addition to LaTeX. Nothing has been done
33 % to see if they work in AMSTeX. The comments below mostly
34 % are written for LaTeX, however.
35 % July 2004, version 0.7
36 % - bug fix, right labels with descenders inserted too much space.
37 % Thanks to Peter Smith for finding this bug,
38 % see http://www.phil.cam.ac.uk/teaching_staff/Smith/LaTeX/
39 % March 2005, version 0.8.
40 % Added a default definition for \fCenter at Denis Kosygin's
41 % suggestion.
42 % September 2005, version 0.9.
43 % Fixed some subtle spacing problems, by adding %'s to the end of
44 % few lines where they were inadvertantly omitted. Thanks to
45 % Arnold Beckmann for finding and fixing this problem.
46 % April 2006, version 0.9.1. Updated comments and testbp2.tex file.
47 % No change to the actual macros.
48 % June 2006, version 1.0. The first integer numbered release.
49 % New feature: root of proof may now be at the bottom instead of
50 % at just the top. Thanks to Alex Hertel for the suggestion to implement
51 % this.
52 % June 2011, version 1.1.
53 % New feature: 4-ary and 5-ary inferences. Thanks to Thomas Strathmann
54 % for taking the initiative to implement these.
55 % Four new commands: QuaternaryInf(C) and QuinaryInf(C).
56 % Bug fix: \insertBetweenHyps now works for proofs with root at top and
57 % three or more hypotheses..
58
59 % A good exposition of how to use bussproofs.sty (version 0.9) has been written
60 % by Peter Smith and is available on the internet.
61 % The comments below also describe the features of bussproofs.sty,
62 % including user-modifiable parameters.
63
64 % bussproofs.sty allows the construction of proof trees in the
65 % style of the sequent calculus and many other proof systems
66 % One novel feature of these macros is they support the horizontal
67 % alignment according to some center point specified with the
68 % command \fCenter. This is the style often used in sequent
69 % calculus proofs.
70 % Proofs are specified in left-to-right traversal order.
71 % For example a proof
72 % A B
73 % -----
74 % D C
75 % ---------
76 % E
77 %
78 % if given in the order D,A,B,C,E. Each line in the proof is
79 % specified according to the arity of the inference which generates
80 % it. Thus, E would be specified with a \BinaryInf or \BinaryInfC
81 % command.
82 %
83 % The above proof tree could be displayed with the commands:
84 %
85 % \AxiomC{D}
86 % \AxiomC{A}
87 % \AxiomC{B}
88 % \BinaryInfC{C}
89 % \BinaryInfC{E}
90 % \DisplayProof
91 %
92 % Inferences in a proof may be nullary (axioms), unary, binary, or
93 % trinary.
94 %
95 % IMPORTANT: You must give the \DisplayProof command to make the proof
96 % be printed. To display a centered proof on a line by itself,
97 % put the proof inside \begin{center} ... \end{center}.
98 %
99 % There are two styles for specifying horizontal centering of
100 % lines (formulas or sequents) in a proof. One format \AxiomC{...}
101 % just centers the formula {...} in the usual way. The other
102 % format is \Axiom$...\fCenter...$. Here, the \fCenter specifies
103 % the center of the formula. (It is permissable for \fCenter to
104 % generate typeset material; in fact, I usually define it to generate
105 % the sequent arrow.) In unary inferences, the \fCenter
106 % positions will be vertically aligned in the upper and lower lines of
107 % the inference. Unary, Binary, Trinary inferences are specified
108 % with the same format as Axioms. The two styles of centering
109 % lines may be combined in a single proof.
110 %
111 % By using the optional \EnableBpAbbreviations command, various
112 % abbreviated two or three letter commands are enabled. This allows,
113 % in particular:
114 % \AX and \AXC for \Axiom and \AxiomC, (resp.),
115 % \DP for \DisplayProof,
116 % \BI and \BIC for \BinaryInf and \BinaryInfC,
117 % \UI and \UIC for \UnaryInf and \UnaryInfC,
118 % \TI and \TIC for \TrinaryInf and \TrinaryInfC,
119 % \LL and \RL for \LeftLabel and \RightLabel.
120 % See the source code below for additional abbreviations.
121 % The enabling of these short abbreviations is OPTIONAL, since
122 % there is the possibility of conflicting with names from other
123 % macro packages.
124 %
125 % By default, the inferences have single horizontal lines (scores)
126 % This can be overridden using the \doubleLine, \noLine commands.
127 % These two commands affect only the next inference. You can make
128 % make a permanent override that applies to the rest of the current
129 % proof using \alwaysDoubleLine and \alwaysNoLine. \singleLine
130 % and \alwaysSingleLine work in the analogous way.
131 %
132 % The macros do their best to give good placements of for the
133 % parts of the proof. Several macros allow you to override the
134 % defaults. These are \insertBetweenHyps{...} which overrides
135 % the default spacing between hypotheses of Binary and Trinary
136 % inferences with {...}. And \kernHyps{...} specifies a distance
137 % to shift the whole block of hypotheses to the right (modifying
138 % the default center position.
139 % Other macros set the vertical placement of the whole proof.
140 % The default is to try to do a good job of placement for inferences
141 % included in text. Two other useful macros are: \bottomAlignProof
142 % which aligns the hbox output by \DisplayProof according to the base
143 % of the bottom line of the proof, and \centerAlignProof which
144 % does a precise center vertical alignment.
145 %
146 % Often, one wishes to place a label next to an inference, usually
147 % to specify the type of inference. These labels can be placed
148 % by using the commands \LeftLabel{...} and \RightLabel{...}
149 % immediately before the command which specifies the inference.
150 % For example, to generate
151 %
152 % A B
153 % --------- X
154 % C
155 %
156 % use the commands
157 % \AxiomC{A}
158 % \AxiomC{B}
159 % \RightLabel{X}
160 % \BinaryInfC{C}
161 % \DisplayProof
162 %
163 % The \DisplayProof command just displays the proof as a text
164 % item. This allows you to put proofs anywhere normal text
165 % might appear; for example, in a paragraph, in a table, in
166 % a tabbing environment, etc. When displaying a proof as inline text,
167 % you should write \DisplayProof{} (with curly brackets) so that
168 % LaTeX will not "eat" the white space following the \DisplayProof
169 % command.
170 % For displaying proofs in a centered display: Do not use the \[...\]
171 % construction (nor $$...$$). Instead use
172 % \begin{center} ... \DisplayProof\end{center}.
173 % Actually there is a better construction to use instead of the
174 % \begin{center}...\DisplayProof\end{center}. This is to
175 % write
176 % \begin{prooftree} ... \end{prooftree}.
177 % Note there is no \DisplayProof used for this: the
178 % \end{prooftree} automatically supplies the \DisplayProof
179 % command.
180 %
181 % Warning: Any commands that set line types or set vertical or
182 % horizontal alignment that are given AFTER the \DisplayProof
183 % command will affect the next proof, no matter how distant.
184
185
186
187
188 % Usages:
189 % =======
190 %
191 % \Axiom$<antecedent>\fCenter<succedent>$
192 %
193 % \AxiomC{<whole sequent or formula}
194 %
195 % Note that the use of surrounding {}'s is mandatory in \AxiomC and
196 % is prohibited in $\Axiom. On the other hand, the $'s are optional
197 % in \AxiomC and are mandatory in \Axiom. To typeset the argument
198 % to \AxiomC in math mode, you must use $'s (or \(...\) ).
199 % The same comments apply to the inference commands below.
200 %
201 % \UnaryInf$<antecendent>\fCenter<succedent>$
202 %
203 % \UnaryInfC{<whole sequent or formula>}
204 %
205 % \BinaryInf$<antecendent>\fCenter<succedent>$
206 %
207 % \BinaryInfC{<whole sequent or formula>}
208 %
209 % \TrinaryInf$<antecendent>\fCenter<succedent>$
210 %
211 % \TrinaryInfC{<whole sequent or formula>}
212 %
213 % \QuaternaryInf$<antecendent>\fCenter<succedent>$
214 %
215 % \QuaternaryInfC{<whole sequent or formula>}
216 %
217 % \QuinaryInf$<antecendent>\fCenter<succedent>$
218 %
219 % \QuinaryInfC{<whole sequent or formula>}
220 %
221 % \LeftLabel{<text>} - Puts <text> as a label to the left
222 % of the next inference line. (Works even if
223 % \noLine is used too.)
224 %
225 % \RightLabel{<text>} - Puts <text> as a label to the right of the
226 % next inference line. (Also works with \noLine.)
227 %
228 % \DisplayProof - outputs the whole proof tree (and finishes it).
229 % The proof tree is output as an hbox.
230 %
231 %
232 % \kernHyps{<dimen>} - Slides the upper hypotheses right distance <dimen>
233 % (This is similar to shifting conclusion left)
234 % - kernHyps works with Unary, Binary and Trinary
235 % inferences and with centered or uncentered sequents.
236 % - Negative values for <dimen> are permitted.
237 %
238 % \insertBetweenHyps{...} - {...} will be inserted between the upper
239 % hypotheses of a Binary or Trinary Inferences.
240 % It is possible to use negative horizontal space
241 % to push them closer together (and even overlap).
242 % This command affects only the next inference.
243 %
244 % \doubleLine - Makes the current (ie, next) horizontal line doubled
245 %
246 % \alwaysDoubleLine - Makes lines doubled for rest of proof
247 %
248 % \singleLine - Makes the current (ie, next) line single
249 %
250 % \alwaysSingleLine - Undoes \alwaysDoubleLine or \alwaysNoLine.
251 %
252 % \noLine - Make no line at all at current (ie next) inference.
253 %
254 % \alwaysNoLine - Makes no lines for rest of proof. (Untested)
255 %
256 % \solidLine - Does solid horizontal line for current inference
257 %
258 % \dottedLine - Does dotted horizontal line for current inference
259 %
260 % \dashedLine - Does dashed horizontal line for current inference
261 %
262 % \alwaysSolidLine - Makes the indicated change in line type, permanently
263 % \alwaysDashedLine until end of proof or until overridden.
264 % \alwaysDottedLine
265 %
266 % \bottomAlignProof - Vertically align proof according to its bottom line.
267 % \centerAlignProof - Vertically align proof proof precisely in its center.
268 % \normalAlignProof - Overrides earlier bottom/center AlignProof commands.
269 % The default alignment will look good in most cases,
270 % whether the proof is displayed or is
271 % in-line. Other alignments may be more
272 % appropriate when putting proofs in tables or
273 % pictures, etc. For custom alignments, use
274 % TeX's raise commands.
275 %
276 % \rootAtTop - specifies that proofs have their root a the top. That it,
277 % proofs will be "upside down".
278 % \rootAtBottom - (default) Specifies that proofs have root at the bottom
279 % The \rootAtTop and \rootAtBottom commands apply *only* to the
280 % current proof. If you want to make them persistent, use one of
281 % the next two commands:
282 % \alwaysRootAtTop
283 % \alwaysRootAtBottom (default)
284 %
285
286 % Optional short abbreviations for commands:
287 \def\EnableBpAbbreviations{%
288 \let\AX\Axiom
289 \let\AXC\AxiomC
290 \let\UI\UnaryInf
291 \let\UIC\UnaryInfC
292 \let\BI\BinaryInf
293 \let\BIC\BinaryInfC
294 \let\TI\TrinaryInf
295 \let\TIC\TrinaryInfC
296 \let\QI\QuaternaryInf
297 \let\QIC\QuaternaryInfC
298 \let\QuI\QuinaryInf
299 \let\QuIC\QuinaryInfC
300 \let\LL\LeftLabel
301 \let\RL\RightLabel
302 \let\DP\DisplayProof
303 }
304
305 % Parameters which control the style of the proof trees.
306 % The user may wish to override these parameters locally or globally.
307 % BUT DON'T CHANGE THE PARAMETERS BY CHANGING THIS FILE (to avoid
308 % future incompatibilities). Instead, you should change them in your
309 % TeX document right after including this style file in the
310 % header material of your LaTeX document.
311
312 \def\ScoreOverhang{4pt} % How much underlines extend out
313 \def\ScoreOverhangLeft{\ScoreOverhang}
314 \def\ScoreOverhangRight{\ScoreOverhang}
315
316 \def\extraVskip{2pt} % Extra space above and below lines
317 \def\ruleScoreFiller{\hrule} % Horizontal rule filler.
318 \def\dottedScoreFiller{\hbox to4pt{\hss.\hss}}
319 \def\dashedScoreFiller{\hbox to2.8mm{\hss\vrule width1.4mm height0.4pt depth0.0pt\hss}}
320 \def\defaultScoreFiller{\ruleScoreFiller} % Default horizontal filler.
321 \def\defaultBuildScore{\buildSingleScore} % In \singleLine mode at start.
322
323 \def\defaultHypSeparation{\hskip.2in} % Used if \insertBetweenHyps isn't given
324
325 \def\labelSpacing{3pt} % Horizontal space separating labels and lines
326
327 \def\proofSkipAmount{\vskip.8ex plus.8ex minus.4ex}
328 % Space above and below a prooftree display.
329
330 \def\defaultRootPosition{\buildRootBottom} % Default: Proofs root at bottom
331 %\def\defaultRootPosition{\buildRootTop} % Makes all proofs upside down
332
333 \ifx\fCenter\undefined
334 \def\fCenter{\relax}
335 \fi
336
337 %
338 % End of user-modifiable parameters.
339 % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
340
341 % Here are some internal paramenters and defaults. Not really intended
342 % to be user-modifiable.
343
344 \def\theHypSeparation{\defaultHypSeparation}
345 \def\alwaysScoreFiller{\defaultScoreFiller} % Horizontal filler.
346 \def\alwaysBuildScore{\defaultBuildScore}
347 \def\theScoreFiller{\alwaysScoreFiller} % Horizontal filler.
348 \def\buildScore{\alwaysBuildScore} %This command builds the score.
349 \def\hypKernAmt{0pt} % Initial setting for kerning the hypotheses.
350
351 \def\defaultLeftLabel{}
352 \def\defaultRightLabel{}
353
354 \def\myTrue{Y}
355 \def\bottomAlignFlag{N}
356 \def\centerAlignFlag{N}
357 \def\defaultRootAtBottomFlag{Y}
358 \def\rootAtBottomFlag{Y}
359
360 % End of internal parameters and defaults.
361
362 \expandafter\ifx\csname newenvironment\endcsname\relax%
363 % If in TeX:
364 \message{\BPmessage}
365 \def\makeatletter{\catcode`\@=11\relax}
366 \def\makeatother{\catcode`\@=12\relax}
367 \makeatletter
368 \def\newcount{\alloc@0\count\countdef\insc@unt}
369 \def\newdimen{\alloc@1\dimen\dimendef\insc@unt}
370 \def\newskip{\alloc@2\skip\skipdef\insc@unt}
371 \def\newbox{\alloc@4\box\chardef\insc@unt}
372 \makeatother
373 \else
374 % If in LaTeX
375 \typeout{\BPmessage}
376 \newenvironment{prooftree}%
377 {\begin{center}\proofSkipAmount \leavevmode}%
378 {\DisplayProof \proofSkipAmount \end{center} }
379 \fi
380
381 \def\thecur#1{\csname#1\number\theLevel\endcsname}
382
383 \newcount\theLevel % This counter is the height of the stack.
384 \global\theLevel=0 % Initialized to zero
385 \newcount\myMaxLevel
386 \global\myMaxLevel=0
387 \newbox\myBoxA % Temporary storage boxes
388 \newbox\myBoxB
389 \newbox\myBoxC
390 \newbox\myBoxD
391 \newbox\myBoxLL % Boxes for the left label and the right label.
392 \newbox\myBoxRL
393 \newdimen\thisAboveSkip %Internal use: amount to skip above line
394 \newdimen\thisBelowSkip %Internal use: amount to skip below line
395 \newdimen\newScoreStart % More temporary storage.
396 \newdimen\newScoreEnd
397 \newdimen\newCenter
398 \newdimen\displace
399 \newdimen\leftLowerAmt% Amount to lower left label
400 \newdimen\rightLowerAmt% Amount to lower right label
401 \newdimen\scoreHeight% Score height
402 \newdimen\scoreDepth% Score Depth
403 \newdimen\htLbox%
404 \newdimen\htRbox%
405 \newdimen\htRRbox%
406 \newdimen\htRRRbox%
407 \newdimen\htAbox%
408 \newdimen\htCbox%
409
410 \setbox\myBoxLL=\hbox{\defaultLeftLabel}%
411 \setbox\myBoxRL=\hbox{\defaultRightLabel}%
412
413 \def\allocatemore{%
414 \ifnum\theLevel>\myMaxLevel%
415 \expandafter\newbox\curBox%
416 \expandafter\newdimen\curScoreStart%
417 \expandafter\newdimen\curCenter%
418 \expandafter\newdimen\curScoreEnd%
419 \global\advance\myMaxLevel by1%
420 \fi%
421 }
422
423 \def\prepAxiom{%
424 \advance\theLevel by1%
425 \edef\curBox{\thecur{myBox}}%
426 \edef\curScoreStart{\thecur{myScoreStart}}%
427 \edef\curCenter{\thecur{myCenter}}%
428 \edef\curScoreEnd{\thecur{myScoreEnd}}%
429 \allocatemore%
430 }
431
432 \def\Axiom$#1\fCenter#2${%
433 % Get level and correct names set.
434 \prepAxiom%
435 % Define the boxes
436 \setbox\myBoxA=\hbox{$\mathord{#1}\fCenter\mathord{\relax}$}%
437 \setbox\myBoxB=\hbox{$#2$}%
438 \global\setbox\curBox=%
439 \hbox{\hskip\ScoreOverhangLeft\relax%
440 \unhcopy\myBoxA\unhcopy\myBoxB\hskip\ScoreOverhangRight\relax}%
441 % Set the relevant dimensions for the boxes
442 \global\curScoreStart=0pt \relax
443 \global\curScoreEnd=\wd\curBox \relax
444 \global\curCenter=\wd\myBoxA \relax
445 \global\advance \curCenter by \ScoreOverhangLeft%
446 \ignorespaces
447 }
448
449 \def\AxiomC#1{ % Note argument not in math mode
450 % Get level and correct names set.
451 \prepAxiom%
452 % Define the box.
453 \setbox\myBoxA=\hbox{#1}%
454 \global\setbox\curBox =%
455 \hbox{\hskip\ScoreOverhangLeft\relax%
456 \unhcopy\myBoxA\hskip\ScoreOverhangRight\relax}%
457 % Set the relevant dimensions for the boxes
458 \global\curScoreStart=0pt \relax
459 \global\curScoreEnd=\wd\curBox \relax
460 \global\curCenter=.5\wd\curBox \relax
461 \global\advance \curCenter by \ScoreOverhangLeft%
462 \ignorespaces
463 }
464
465 \def\prepUnary{%
466 \ifnum \theLevel<1
467 \errmessage{Hypotheses missing!}
468 \fi%
469 \edef\curBox{\thecur{myBox}}%
470 \edef\curScoreStart{\thecur{myScoreStart}}%
471 \edef\curCenter{\thecur{myCenter}}%
472 \edef\curScoreEnd{\thecur{myScoreEnd}}%
473 }
474
475 \def\UnaryInf$#1\fCenter#2${%
476 \prepUnary%
477 \buildConclusion{#1}{#2}%
478 \joinUnary%
479 \resetInferenceDefaults%
480 \ignorespaces%
481 }
482
483 \def\UnaryInfC#1{
484 \prepUnary%
485 \buildConclusionC{#1}%
486 %Align and join the curBox and the new box into one vbox.
487 \joinUnary%
488 \resetInferenceDefaults%
489 \ignorespaces%
490 }
491
492 \def\prepBinary{%
493 \ifnum\theLevel<2
494 \errmessage{Hypotheses missing!}
495 \fi%
496 \edef\rcurBox{\thecur{myBox}}% Set up names of right hypothesis
497 \edef\rcurScoreStart{\thecur{myScoreStart}}%
498 \edef\rcurCenter{\thecur{myCenter}}%
499 \edef\rcurScoreEnd{\thecur{myScoreEnd}}%
500 \advance\theLevel by-1%
501 \edef\lcurBox{\thecur{myBox}}% Set up names of left hypothesis
502 \edef\lcurScoreStart{\thecur{myScoreStart}}%
503 \edef\lcurCenter{\thecur{myCenter}}%
504 \edef\lcurScoreEnd{\thecur{myScoreEnd}}%
505 }
506
507 \def\BinaryInf$#1\fCenter#2${%
508 \prepBinary%
509 \buildConclusion{#1}{#2}%
510 \joinBinary%
511 \resetInferenceDefaults%
512 \ignorespaces%
513 }
514
515 \def\BinaryInfC#1{%
516 \prepBinary%
517 \buildConclusionC{#1}%
518 \joinBinary%
519 \resetInferenceDefaults%
520 \ignorespaces%
521 }
522
523 \def\prepTrinary{%
524 \ifnum\theLevel<3
525 \errmessage{Hypotheses missing!}
526 \fi%
527 \edef\rcurBox{\thecur{myBox}}% Set up names of right hypothesis
528 \edef\rcurScoreStart{\thecur{myScoreStart}}%
529 \edef\rcurCenter{\thecur{myCenter}}%
530 \edef\rcurScoreEnd{\thecur{myScoreEnd}}%
531 \advance\theLevel by-1%
532 \edef\ccurBox{\thecur{myBox}}% Set up names of center hypothesis
533 \edef\ccurScoreStart{\thecur{myScoreStart}}%
534 \edef\ccurCenter{\thecur{myCenter}}%
535 \edef\ccurScoreEnd{\thecur{myScoreEnd}}%
536 \advance\theLevel by-1%
537 \edef\lcurBox{\thecur{myBox}}% Set up names of left hypothesis
538 \edef\lcurScoreStart{\thecur{myScoreStart}}%
539 \edef\lcurCenter{\thecur{myCenter}}%
540 \edef\lcurScoreEnd{\thecur{myScoreEnd}}%
541 }
542
543 \def\TrinaryInf$#1\fCenter#2${%
544 \prepTrinary%
545 \buildConclusion{#1}{#2}%
546 \joinTrinary%
547 \resetInferenceDefaults%
548 \ignorespaces%
549 }
550
551 \def\TrinaryInfC#1{%
552 \prepTrinary%
553 \buildConclusionC{#1}%
554 \joinTrinary%
555 \resetInferenceDefaults%
556 \ignorespaces%
557 }
558
559 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
560 \def\prepQuaternary{%
561 \ifnum\theLevel<4
562 \errmessage{Hypotheses missing!}
563 \fi%
564 \edef\rrcurBox{\thecur{myBox}}% Set up names of very right hypothesis
565 \edef\rrcurScoreStart{\thecur{myScoreStart}}%
566 \edef\rrcurCenter{\thecur{myCenter}}%
567 \edef\rrcurScoreEnd{\thecur{myScoreEnd}}%
568 \advance\theLevel by-1%
569 \edef\rcurBox{\thecur{myBox}}% Set up names of right hypothesis
570 \edef\rcurScoreStart{\thecur{myScoreStart}}%
571 \edef\rcurCenter{\thecur{myCenter}}%
572 \edef\rcurScoreEnd{\thecur{myScoreEnd}}%
573 \advance\theLevel by-1%
574 \edef\ccurBox{\thecur{myBox}}% Set up names of center hypothesis
575 \edef\ccurScoreStart{\thecur{myScoreStart}}%
576 \edef\ccurCenter{\thecur{myCenter}}%
577 \edef\ccurScoreEnd{\thecur{myScoreEnd}}%
578 \advance\theLevel by-1%
579 \edef\lcurBox{\thecur{myBox}}% Set up names of left hypothesis
580 \edef\lcurScoreStart{\thecur{myScoreStart}}%
581 \edef\lcurCenter{\thecur{myCenter}}%
582 \edef\lcurScoreEnd{\thecur{myScoreEnd}}%
583 }
584
585 \def\QuaternaryInf$#1\fCenter#2${%
586 \prepQuaternary%
587 \buildConclusion{#1}{#2}%
588 \joinQuaternary%
589 \resetInferenceDefaults%
590 \ignorespaces%
591 }
592
593 \def\QuaternaryInfC#1{%
594 \prepQuaternary%
595 \buildConclusionC{#1}%
596 \joinQuaternary%
597 \resetInferenceDefaults%
598 \ignorespaces%
599 }
600
601 \def\joinQuaternary{% Construct the quarterary inference into a vbox.
602 % Join the four hypotheses's boxes into one hbox.
603 \setbox\myBoxA=\hbox{\theHypSeparation}%
604 \lcurScoreEnd=\rrcurScoreEnd%
605 \advance\lcurScoreEnd by\wd\rcurBox%
606 \advance\lcurScoreEnd by\wd\lcurBox%
607 \advance\lcurScoreEnd by\wd\ccurBox%
608 \advance\lcurScoreEnd by3\wd\myBoxA%
609 \displace=\lcurScoreEnd%
610 \advance\displace by -\lcurScoreStart%
611 \lcurCenter=.5\displace%
612 \advance\lcurCenter by\lcurScoreStart%
613 \ifx\rootAtBottomFlag\myTrue%
614 \setbox\lcurBox=%
615 \hbox{\box\lcurBox\unhcopy\myBoxA\box\ccurBox%
616 \unhcopy\myBoxA\box\rcurBox
617 \unhcopy\myBoxA\box\rrcurBox}%
618 \else%
619 \htLbox = \ht\lcurBox%
620 \htAbox = \ht\myBoxA%
621 \htCbox = \ht\ccurBox%
622 \htRbox = \ht\rcurBox%
623 \htRRbox = \ht\rrcurBox%
624 \setbox\lcurBox=%
625 \hbox{\lower\htLbox\box\lcurBox%
626 \lower\htAbox\copy\myBoxA\lower\htCbox\box\ccurBox%
627 \lower\htAbox\copy\myBoxA\lower\htRbox\box\rcurBox%
628 \lower\htAbox\copy\myBoxA\lower\htRRbox\box\rrcurBox}%
629 \fi%
630 % Adjust center of upper hypotheses according to how much
631 % the lower sequent is off-center.
632 \displace=\newCenter%
633 \advance\displace by -.5\newScoreStart%
634 \advance\displace by -.5\newScoreEnd%
635 \advance\lcurCenter by \displace%
636 %Align and join the curBox and the two hypotheses's box into one vbox.
637 \edef\curBox{\lcurBox}%
638 \edef\curScoreStart{\lcurScoreStart}%
639 \edef\curScoreEnd{\lcurScoreEnd}%
640 \edef\curCenter{\lcurCenter}%
641 \joinUnary%
642 }
643
644 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
645 \def\prepQuinary{%
646 \ifnum\theLevel<5
647 \errmessage{Hypotheses missing!}
648 \fi%
649 \edef\rrrcurBox{\thecur{myBox}}% Set up names of very very right hypothesis
650 \edef\rrrcurScoreStart{\thecur{myScoreStart}}%
651 \edef\rrrcurCenter{\thecur{myCenter}}%
652 \edef\rrrcurScoreEnd{\thecur{myScoreEnd}}%
653 \advance\theLevel by-1%
654 \edef\rrcurBox{\thecur{myBox}}% Set up names of very right hypothesis
655 \edef\rrcurScoreStart{\thecur{myScoreStart}}%
656 \edef\rrcurCenter{\thecur{myCenter}}%
657 \edef\rrcurScoreEnd{\thecur{myScoreEnd}}%
658 \advance\theLevel by-1%
659 \edef\rcurBox{\thecur{myBox}}% Set up names of right hypothesis
660 \edef\rcurScoreStart{\thecur{myScoreStart}}%
661 \edef\rcurCenter{\thecur{myCenter}}%
662 \edef\rcurScoreEnd{\thecur{myScoreEnd}}%
663 \advance\theLevel by-1%
664 \edef\ccurBox{\thecur{myBox}}% Set up names of center hypothesis
665 \edef\ccurScoreStart{\thecur{myScoreStart}}%
666 \edef\ccurCenter{\thecur{myCenter}}%
667 \edef\ccurScoreEnd{\thecur{myScoreEnd}}%
668 \advance\theLevel by-1%
669 \edef\lcurBox{\thecur{myBox}}% Set up names of left hypothesis
670 \edef\lcurScoreStart{\thecur{myScoreStart}}%
671 \edef\lcurCenter{\thecur{myCenter}}%
672 \edef\lcurScoreEnd{\thecur{myScoreEnd}}%
673 }
674
675 \def\QuinaryInf$#1\fCenter#2${%
676 \prepQuinary%
677 \buildConclusion{#1}{#2}%
678 \joinQuinary%
679 \resetInferenceDefaults%
680 \ignorespaces%
681 }
682
683 \def\QuinaryInfC#1{%
684 \prepQuinary%
685 \buildConclusionC{#1}%
686 \joinQuinary%
687 \resetInferenceDefaults%
688 \ignorespaces%
689 }
690
691 \def\joinQuinary{% Construct the quinary inference into a vbox.
692 % Join the five hypotheses's boxes into one hbox.
693 \setbox\myBoxA=\hbox{\theHypSeparation}%
694 \lcurScoreEnd=\rrrcurScoreEnd%
695 \advance\lcurScoreEnd by\wd\rrcurBox%
696 \advance\lcurScoreEnd by\wd\rcurBox%
697 \advance\lcurScoreEnd by\wd\lcurBox%
698 \advance\lcurScoreEnd by\wd\ccurBox%
699 \advance\lcurScoreEnd by4\wd\myBoxA%
700 \displace=\lcurScoreEnd%
701 \advance\displace by -\lcurScoreStart%
702 \lcurCenter=.5\displace%
703 \advance\lcurCenter by\lcurScoreStart%
704 \ifx\rootAtBottomFlag\myTrue%
705 \setbox\lcurBox=%
706 \hbox{\box\lcurBox\unhcopy\myBoxA\box\ccurBox%
707 \unhcopy\myBoxA\box\rcurBox
708 \unhcopy\myBoxA\box\rrcurBox
709 \unhcopy\myBoxA\box\rrrcurBox}%
710 \else%
711 \htLbox = \ht\lcurBox%
712 \htAbox = \ht\myBoxA%
713 \htCbox = \ht\ccurBox%
714 \htRbox = \ht\rcurBox%
715 \htRRbox = \ht\rrcurBox%
716 \htRRRbox = \ht\rrrcurBox%
717 \setbox\lcurBox=%
718 \hbox{\lower\htLbox\box\lcurBox%
719 \lower\htAbox\copy\myBoxA\lower\htCbox\box\ccurBox%
720 \lower\htAbox\copy\myBoxA\lower\htRbox\box\rcurBox%
721 \lower\htAbox\copy\myBoxA\lower\htRRbox\box\rrcurBox%
722 \lower\htAbox\copy\myBoxA\lower\htRRRbox\box\rrrcurBox}%
723 \fi%
724 % Adjust center of upper hypotheses according to how much
725 % the lower sequent is off-center.
726 \displace=\newCenter%
727 \advance\displace by -.5\newScoreStart%
728 \advance\displace by -.5\newScoreEnd%
729 \advance\lcurCenter by \displace%
730 %Align and join the curBox and the two hypotheses's box into one vbox.
731 \edef\curBox{\lcurBox}%
732 \edef\curScoreStart{\lcurScoreStart}%
733 \edef\curScoreEnd{\lcurScoreEnd}%
734 \edef\curCenter{\lcurCenter}%
735 \joinUnary%
736 }
737
738 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
739
740 \def\buildConclusion#1#2{% Build lower sequent w/ center at \fCenter position.
741 % Define the boxes
742 \setbox\myBoxA=\hbox{$\mathord{#1}\fCenter\mathord{\relax}$}%
743 \setbox\myBoxB=\hbox{$#2$}%
744 % Put them together in \myBoxC
745 \setbox\myBoxC =%
746 \hbox{\hskip\ScoreOverhangLeft\relax%
747 \unhcopy\myBoxA\unhcopy\myBoxB\hskip\ScoreOverhangRight\relax}%
748 % Calculate the center of the \myBoxC string.
749 \newScoreStart=0pt \relax%
750 \newCenter=\wd\myBoxA \relax%
751 \advance \newCenter by \ScoreOverhangLeft%
752 \newScoreEnd=\wd\myBoxC%
753 }
754
755 \def\buildConclusionC#1{% Build lower sequent w/o \fCenter present.
756 % Define the box.
757 \setbox\myBoxA=\hbox{#1}%
758 \setbox\myBoxC =%
759 \hbox{\hbox{\hskip\ScoreOverhangLeft\relax%
760 \unhcopy\myBoxA\hskip\ScoreOverhangRight\relax}}%
761 % Calculate kerning to line up centers
762 \newScoreStart=0pt \relax%
763 \newCenter=.5\wd\myBoxC \relax%
764 \newScoreEnd=\wd\myBoxC%
765 \advance \newCenter by \ScoreOverhangLeft%
766 }
767
768 \def\joinUnary{%Align and join \curBox and \myBoxC into a single vbox
769 \global\advance\curCenter by -\hypKernAmt%
770 \ifnum\curCenter<\newCenter%
771 \displace=\newCenter%
772 \advance \displace by -\curCenter%
773 \kernUpperBox%
774 \else%
775 \displace=\curCenter%
776 \advance \displace by -\newCenter%
777 \kernLowerBox%
778 \fi%
779 \ifnum \newScoreStart < \curScoreStart %
780 \global \curScoreStart = \newScoreStart \fi%
781 \ifnum \curScoreEnd < \newScoreEnd %
782 \global \curScoreEnd = \newScoreEnd \fi%
783 % Leave room for the left label.
784 \ifnum \curScoreStart<\wd\myBoxLL%
785 \global\displace = \wd\myBoxLL%
786 \global\advance\displace by -\curScoreStart%
787 \kernUpperBox%
788 \kernLowerBox%
789 \fi%
790 % Draw the score
791 \buildScore%
792 % Form the score and labels into a box.
793 \buildScoreLabels%
794 % Form the new box and its dimensions
795 \ifx\rootAtBottomFlag\myTrue%
796 \buildRootBottom%
797 \else%
798 \buildRootTop%
799 \fi%
800 \global \curScoreStart=\newScoreStart%
801 \global \curScoreEnd=\newScoreEnd%
802 \global \curCenter=\newCenter%
803 }
804
805 \def\buildRootBottom{%
806 \global \setbox \curBox =%
807 \vbox{\box\curBox%
808 \vskip\thisAboveSkip \relax%
809 \nointerlineskip\box\myBoxD%
810 \vskip\thisBelowSkip \relax%
811 \nointerlineskip\box\myBoxC}%
812 }
813
814 \def\buildRootTop{%
815 \global \setbox \curBox =%
816 \vbox{\box\myBoxC%
817 \vskip\thisAboveSkip \relax%
818 \nointerlineskip\box\myBoxD%
819 \vskip\thisBelowSkip \relax%
820 \nointerlineskip\box\curBox}%
821 }
822
823 \def\kernUpperBox{%
824 \global\setbox\curBox =%
825 \hbox{\hskip\displace\box\curBox}%
826 \global\advance \curScoreStart by \displace%
827 \global\advance \curScoreEnd by \displace%
828 \global\advance\curCenter by \displace%
829 }
830
831 \def\kernLowerBox{%
832 \global\setbox\myBoxC =%
833 \hbox{\hskip\displace\unhbox\myBoxC}%
834 \global\advance \newScoreStart by \displace%
835 \global\advance \newScoreEnd by \displace%
836 \global\advance\newCenter by \displace%
837 }
838
839 \def\joinBinary{% Construct the binary inference into a vbox.
840 % Join the two hypotheses's boxes into one hbox.
841 \setbox\myBoxA=\hbox{\theHypSeparation}%
842 \lcurScoreEnd=\rcurScoreEnd%
843 \advance\lcurScoreEnd by\wd\lcurBox%
844 \advance\lcurScoreEnd by\wd\myBoxA%
845 \displace=\lcurScoreEnd%
846 \advance\displace by -\lcurScoreStart%
847 \lcurCenter=.5\displace%
848 \advance\lcurCenter by\lcurScoreStart%
849 \ifx\rootAtBottomFlag\myTrue%
850 \setbox\lcurBox=%
851 \hbox{\box\lcurBox\unhcopy\myBoxA\box\rcurBox}%
852 \else%
853 \htLbox = \ht\lcurBox%
854 \htAbox = \ht\myBoxA%
855 \htRbox = \ht\rcurBox%
856 \setbox\lcurBox=%
857 \hbox{\lower\htLbox\box\lcurBox%
858 \lower\htAbox\box\myBoxA\lower\htRbox\box\rcurBox}%
859 \fi%
860 % Adjust center of upper hypotheses according to how much
861 % the lower sequent is off-center.
862 \displace=\newCenter%
863 \advance\displace by -.5\newScoreStart%
864 \advance\displace by -.5\newScoreEnd%
865 \advance\lcurCenter by \displace%
866 %Align and join the curBox and the two hypotheses's box into one vbox.
867 \edef\curBox{\lcurBox}%
868 \edef\curScoreStart{\lcurScoreStart}%
869 \edef\curScoreEnd{\lcurScoreEnd}%
870 \edef\curCenter{\lcurCenter}%
871 \joinUnary%
872 }
873
874 \def\joinTrinary{% Construct the trinary inference into a vbox.
875 % Join the three hypotheses's boxes into one hbox.
876 \setbox\myBoxA=\hbox{\theHypSeparation}%
877 \lcurScoreEnd=\rcurScoreEnd%
878 \advance\lcurScoreEnd by\wd\lcurBox%
879 \advance\lcurScoreEnd by\wd\ccurBox%
880 \advance\lcurScoreEnd by2\wd\myBoxA%
881 \displace=\lcurScoreEnd%
882 \advance\displace by -\lcurScoreStart%
883 \lcurCenter=.5\displace%
884 \advance\lcurCenter by\lcurScoreStart%
885 \ifx\rootAtBottomFlag\myTrue%
886 \setbox\lcurBox=%
887 \hbox{\box\lcurBox\unhcopy\myBoxA\box\ccurBox%
888 \unhcopy\myBoxA\box\rcurBox}%
889 \else%
890 \htLbox = \ht\lcurBox%
891 \htAbox = \ht\myBoxA%
892 \htCbox = \ht\ccurBox%
893 \htRbox = \ht\rcurBox%
894 \setbox\lcurBox=%
895 \hbox{\lower\htLbox\box\lcurBox%
896 \lower\htAbox\copy\myBoxA\lower\htCbox\box\ccurBox%
897 \lower\htAbox\copy\myBoxA\lower\htRbox\box\rcurBox}%
898 \fi%
899 % Adjust center of upper hypotheses according to how much
900 % the lower sequent is off-center.
901 \displace=\newCenter%
902 \advance\displace by -.5\newScoreStart%
903 \advance\displace by -.5\newScoreEnd%
904 \advance\lcurCenter by \displace%
905 %Align and join the curBox and the two hypotheses's box into one vbox.
906 \edef\curBox{\lcurBox}%
907 \edef\curScoreStart{\lcurScoreStart}%
908 \edef\curScoreEnd{\lcurScoreEnd}%
909 \edef\curCenter{\lcurCenter}%
910 \joinUnary%
911 }
912
913 \def\DisplayProof{%
914 % Display (and purge) the proof tree.
915 % Choose the appropriate vertical alignment.
916 \ifnum \theLevel=1 \relax \else%x
917 \errmessage{Proof tree badly specified.}%
918 \fi%
919 \edef\curBox{\thecur{myBox}}%
920 \ifx\bottomAlignFlag\myTrue%
921 \displace=0pt%
922 \else%
923 \displace=.5\ht\curBox%
924 \ifx\centerAlignFlag\myTrue\relax
925 \else%
926 \advance\displace by -3pt%
927 \fi%
928 \fi%
929 \leavevmode%
930 \lower\displace\hbox{\copy\curBox}%
931 \global\theLevel=0%
932 \global\def\alwaysBuildScore{\defaultBuildScore}% Restore "always"
933 \global\def\alwaysScoreFiller{\defaultScoreFiller}% Restore "always"
934 \global\def\bottomAlignFlag{N}%
935 \global\def\centerAlignFlag{N}%
936 \resetRootPosition
937 \resetInferenceDefaults%
938 \ignorespaces
939 }
940
941 \def\buildSingleScore{% Make an hbox with a single score.
942 \displace=\curScoreEnd%
943 \advance \displace by -\curScoreStart%
944 \global\setbox \myBoxD =%
945 \hbox to \displace{\expandafter\xleaders\theScoreFiller\hfill}%
946 %\global\setbox \myBoxD =%
947 %\hbox{\hskip\curScoreStart\relax \box\myBoxD}%
948 }
949
950 \def\buildDoubleScore{% Make an hbox with a double score.
951 \buildSingleScore%
952 \global\setbox\myBoxD=%
953 \hbox{\hbox to0pt{\copy\myBoxD\hss}\raise2pt\copy\myBoxD}%
954 }
955
956 \def\buildNoScore{% Make an hbox with no score (raise a little anyway)
957 \global\setbox\myBoxD=\hbox{\vbox{\vskip1pt}}%
958 }
959
960 \def\doubleLine{%
961 \gdef\buildScore{\buildDoubleScore}% Set next score to this type
962 \ignorespaces
963 }
964 \def\alwaysDoubleLine{%
965 \gdef\alwaysBuildScore{\buildDoubleScore}% Do double for rest of proof.
966 \gdef\buildScore{\buildDoubleScore}% Set next score to be double
967 \ignorespaces
968 }
969 \def\singleLine{%
970 \gdef\buildScore{\buildSingleScore}% Set next score to be single
971 \ignorespaces
972 }
973 \def\alwaysSingleLine{%
974 \gdef\alwaysBuildScore{\buildSingleScore}% Do single for rest of proof.
975 \gdef\buildScore{\buildSingleScore}% Set next score to be single
976 \ignorespaces
977 }
978 \def\noLine{%
979 \gdef\buildScore{\buildNoScore}% Set next score to this type
980 \ignorespaces
981 }
982 \def\alwaysNoLine{%
983 \gdef\alwaysBuildScore{\buildNoScore}%Do nolines for rest of proof.
984 \gdef\buildScore{\buildNoScore}% Set next score to be blank
985 \ignorespaces
986 }
987 \def\solidLine{%
988 \gdef\theScoreFiller{\ruleScoreFiller}% Use solid horizontal line.
989 \ignorespaces
990 }
991 \def\alwaysSolidLine{%
992 \gdef\alwaysScoreFiller{\ruleScoreFiller}% Do solid for rest of proof
993 \gdef\theScoreFiller{\ruleScoreFiller}% Use solid horizontal line.
994 \ignorespaces
995 }
996 \def\dottedLine{%
997 \gdef\theScoreFiller{\dottedScoreFiller}% Use dotted horizontal line.
998 \ignorespaces
999 }
1000 \def\alwaysDottedLine{%
1001 \gdef\alwaysScoreFiller{\dottedScoreFiller}% Do dotted for rest of proof
1002 \gdef\theScoreFiller{\dottedScoreFiller}% Use dotted horizontal line.
1003 \ignorespaces
1004 }
1005 \def\dashedLine{%
1006 \gdef\theScoreFiller{\dashedScoreFiller}% Use dashed horizontal line.
1007 \ignorespaces
1008 }
1009 \def\alwaysDashedLine{%
1010 \gdef\alwaysScoreFiller{\dashedScoreFiller}% Do dashed for rest of proof
1011 \gdef\theScoreFiller{\dashedScoreFiller}% Use dashed horizontal line.
1012 \ignorespaces
1013 }
1014 \def\kernHyps#1{%
1015 \gdef\hypKernAmt{#1}%
1016 \ignorespaces
1017 }
1018 \def\insertBetweenHyps#1{%
1019 \gdef\theHypSeparation{#1}%
1020 \ignorespaces
1021 }
1022
1023 \def\centerAlignProof{%
1024 \def\centerAlignFlag{Y}%
1025 \def\bottomAlignFlag{N}%
1026 \ignorespaces
1027 }
1028 \def\bottomAlignProof{%
1029 \def\centerAlignFlag{N}%
1030 \def\bottomAlignFlag{Y}%
1031 \ignorespaces
1032 }
1033 \def\normalAlignProof{%
1034 \def\centerAlignFlag{N}%
1035 \def\bottomAlignFlag{N}%
1036 \ignorespaces
1037 }
1038
1039 \def\LeftLabel#1{%
1040 \global\setbox\myBoxLL=\hbox{{#1}\hskip\labelSpacing}%
1041 \ignorespaces
1042 }
1043 \def\RightLabel#1{%
1044 \global\setbox\myBoxRL=\hbox{\hskip\labelSpacing #1}%
1045 \ignorespaces
1046 }
1047
1048 \def\buildScoreLabels{%
1049 \scoreHeight = \ht\myBoxD%
1050 \scoreDepth = \dp\myBoxD%
1051 \leftLowerAmt=\ht\myBoxLL%
1052 \advance \leftLowerAmt by -\dp\myBoxLL%
1053 \advance \leftLowerAmt by -\scoreHeight%
1054 \advance \leftLowerAmt by \scoreDepth%
1055 \leftLowerAmt=.5\leftLowerAmt%
1056 \rightLowerAmt=\ht\myBoxRL%
1057 \advance \rightLowerAmt by -\dp\myBoxRL%
1058 \advance \rightLowerAmt by -\scoreHeight%
1059 \advance \rightLowerAmt by \scoreDepth%
1060 \rightLowerAmt=.5\rightLowerAmt%
1061 \displace = \curScoreStart%
1062 \advance\displace by -\wd\myBoxLL%
1063 \global\setbox\myBoxD =%
1064 \hbox{\hskip\displace%
1065 \lower\leftLowerAmt\copy\myBoxLL%
1066 \box\myBoxD%
1067 \lower\rightLowerAmt\copy\myBoxRL}%
1068 \global\thisAboveSkip = \ht\myBoxLL%
1069 \global\advance \thisAboveSkip by -\leftLowerAmt%
1070 \global\advance \thisAboveSkip by -\scoreHeight%
1071 \ifnum \thisAboveSkip<0 %
1072 \global\thisAboveSkip=0pt%
1073 \fi%
1074 \displace = \ht\myBoxRL%
1075 \advance \displace by -\rightLowerAmt%
1076 \advance \displace by -\scoreHeight%
1077 \ifnum \displace<0 %
1078 \displace=0pt%
1079 \fi%
1080 \ifnum \displace>\thisAboveSkip %
1081 \global\thisAboveSkip=\displace%
1082 \fi%
1083 \global\thisBelowSkip = \dp\myBoxLL%
1084 \global\advance\thisBelowSkip by \leftLowerAmt%
1085 \global\advance\thisBelowSkip by -\scoreDepth%
1086 \ifnum\thisBelowSkip<0 %
1087 \global\thisBelowSkip = 0pt%
1088 \fi%
1089 \displace = \dp\myBoxRL%
1090 \advance\displace by \rightLowerAmt%
1091 \advance\displace by -\scoreDepth%
1092 \ifnum\displace<0 %
1093 \displace = 0pt%
1094 \fi%
1095 \ifnum\displace>\thisBelowSkip%
1096 \global\thisBelowSkip = \displace%
1097 \fi%
1098 \global\thisAboveSkip = -\thisAboveSkip%
1099 \global\thisBelowSkip = -\thisBelowSkip%
1100 \global\advance\thisAboveSkip by\extraVskip% Extra space above line
1101 \global\advance\thisBelowSkip by\extraVskip% Extra space below line
1102 }
1103
1104 \def\resetInferenceDefaults{%
1105 \global\def\theHypSeparation{\defaultHypSeparation}%
1106 \global\setbox\myBoxLL=\hbox{\defaultLeftLabel}%
1107 \global\setbox\myBoxRL=\hbox{\defaultRightLabel}%
1108 \global\def\buildScore{\alwaysBuildScore}%
1109 \global\def\theScoreFiller{\alwaysScoreFiller}%
1110 \gdef\hypKernAmt{0pt}% Restore to zero kerning.
1111 }
1112
1113
1114 \def\rootAtBottom{%
1115 \global\def\rootAtBottomFlag{Y}%
1116 }
1117
1118 \def\rootAtTop{%
1119 \global\def\rootAtBottomFlag{N}%
1120 }
1121
1122 \def\resetRootPosition{%
1123 \global\edef\rootAtBottomFlag{\defaultRootAtBottomFlag}
1124 }
1125
1126 \def\alwaysRootAtBottom{%
1127 \global\def\defaultRootAtBottomFlag{Y}
1128 \rootAtBottom
1129 }
1130
1131 \def\alwaysRootAtTop{%
1132 \global\def\defaultRootAtBottomFlag{N}
1133 \rootAtTop
1134 }
1135
1136