src/Tools/isac/Doc/railsetup.sty
changeset 59827 168abe8dd1e3
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/isac/Doc/railsetup.sty	Wed Mar 11 15:25:52 2020 +0100
     1.3 @@ -0,0 +1,1202 @@
     1.4 +% rail.sty - style file to support railroad diagrams
     1.5 +%
     1.6 +% 09-Jul-90 L. Rooijakkers
     1.7 +% 08-Oct-90 L. Rooijakkers	fixed centering bug when \rail@tmpc<0.
     1.8 +% 07-Feb-91 L. Rooijakkers	added \railoptions command, indexing
     1.9 +% 08-Feb-91 L. Rooijakkers	minor fixes
    1.10 +% 28-Jun-94 K. Barthelmann	turned into LaTeX2e package
    1.11 +% 08-Dec-96 K. Barthelmann	replaced \@writefile
    1.12 +% 13-Dec-96 K. Barthelmann	cleanup
    1.13 +% 22-Feb-98 K. Barthelmann	fixed catcodes of special characters
    1.14 +% 18-Apr-98 K. Barthelmann	fixed \par handling
    1.15 +% 19-May-98 J. Olsson		Added new macros to support arrow heads.
    1.16 +% 26-Jul-98 K. Barthelmann	changed \par to output newlines
    1.17 +% 02-May-11 M. Wenzel           default setup for Isabelle
    1.18 +%
    1.19 +% This style file needs to be used in conjunction with the 'rail'
    1.20 +% program. Running LaTeX as 'latex file' produces file.rai, which should be
    1.21 +% processed by Rail with 'rail file'. This produces file.rao, which will
    1.22 +% be picked up by LaTeX on the next 'latex file' run.
    1.23 +%
    1.24 +% LaTeX will warn if there is no file.rao or it's out of date.
    1.25 +%
    1.26 +% The macros in this file thus consist of two parts: those that read and
    1.27 +% write the .rai and .rao files, and those that do the actual formatting
    1.28 +% of the railroad diagrams.
    1.29 +
    1.30 +\NeedsTeXFormat{LaTeX2e}
    1.31 +\ProvidesPackage{rail}[1998/05/19]
    1.32 +
    1.33 +% railroad diagram formatting parameters (user level)
    1.34 +% all of these are copied into their internal versions by \railinit
    1.35 +%
    1.36 +% \railunit : \unitlength within railroad diagrams
    1.37 +% \railextra : extra length at outside of diagram
    1.38 +% \railboxheight : height of ovals and frames
    1.39 +% \railboxskip : vertical space between lines
    1.40 +% \railboxleft : space to the left of a box
    1.41 +% \railboxright : space to the right of a box
    1.42 +% \railovalspace : extra space around contents of oval
    1.43 +% \railframespace : extra space around contents of frame
    1.44 +% \railtextleft : space to the left of text
    1.45 +% \railtextright : space to the right of text
    1.46 +% \railtextup : space to lift text up
    1.47 +% \railjoinsize : circle size of join/split arcs
    1.48 +% \railjoinadjust : space to adjust join
    1.49 +%
    1.50 +% \railnamesep : separator between name and rule body
    1.51 +
    1.52 +\newlength\railunit
    1.53 +\newlength\railextra
    1.54 +\newlength\railboxheight
    1.55 +\newlength\railboxskip
    1.56 +\newlength\railboxleft
    1.57 +\newlength\railboxright
    1.58 +\newlength\railovalspace
    1.59 +\newlength\railframespace
    1.60 +\newlength\railtextleft
    1.61 +\newlength\railtextright
    1.62 +\newlength\railtextup
    1.63 +\newlength\railjoinsize
    1.64 +\newlength\railjoinadjust
    1.65 +\newlength\railnamesep
    1.66 +
    1.67 +% initialize the parameters
    1.68 +
    1.69 +\setlength\railunit{1sp}
    1.70 +\setlength\railextra{4ex}
    1.71 +\setlength\railboxleft{1ex}
    1.72 +\setlength\railboxright{1ex}
    1.73 +\setlength\railovalspace{2ex}
    1.74 +\setlength\railframespace{2ex}
    1.75 +\setlength\railtextleft{1ex}
    1.76 +\setlength\railtextright{1ex}
    1.77 +\setlength\railjoinadjust{0pt}
    1.78 +\setlength\railnamesep{1ex}
    1.79 +
    1.80 +\DeclareOption{10pt}{
    1.81 +  \setlength\railboxheight{16pt}
    1.82 +  \setlength\railboxskip{24pt}
    1.83 +  \setlength\railtextup{5pt}
    1.84 +  \setlength\railjoinsize{16pt}
    1.85 +}
    1.86 +\DeclareOption{11pt}{
    1.87 +  \setlength\railboxheight{16pt}
    1.88 +  \setlength\railboxskip{24pt}
    1.89 +  \setlength\railtextup{5pt}
    1.90 +  \setlength\railjoinsize{16pt}
    1.91 +}
    1.92 +\DeclareOption{12pt}{
    1.93 +  \setlength\railboxheight{20pt}
    1.94 +  \setlength\railboxskip{28pt}
    1.95 +  \setlength\railtextup{6pt}
    1.96 +  \setlength\railjoinsize{20pt}
    1.97 +}
    1.98 +
    1.99 +\ExecuteOptions{10pt}
   1.100 +\ProcessOptions
   1.101 +
   1.102 +% internal versions of the formatting parameters
   1.103 +%
   1.104 +% \rail@extra   : \railextra
   1.105 +% \rail@boxht   : \railboxheight
   1.106 +% \rail@boxsp   : \railboxskip
   1.107 +% \rail@boxlf   : \railboxleft
   1.108 +% \rail@boxrt   : \railboxright
   1.109 +% \rail@boxhht  : \railboxheight / 2
   1.110 +% \rail@ovalsp  : \railovalspace
   1.111 +% \rail@framesp : \railframespace
   1.112 +% \rail@textlf  : \railtextleft
   1.113 +% \rail@textrt  : \railtextright
   1.114 +% \rail@textup  : \railtextup
   1.115 +% \rail@joinsz  : \railjoinsize
   1.116 +% \rail@joinhsz : \railjoinsize / 2
   1.117 +% \rail@joinadj : \railjoinadjust
   1.118 +%
   1.119 +% \railinit : internalize all of the parameters.
   1.120 +
   1.121 +\newcount\rail@extra
   1.122 +\newcount\rail@boxht
   1.123 +\newcount\rail@boxsp
   1.124 +\newcount\rail@boxlf
   1.125 +\newcount\rail@boxrt
   1.126 +\newcount\rail@boxhht
   1.127 +\newcount\rail@ovalsp
   1.128 +\newcount\rail@framesp
   1.129 +\newcount\rail@textlf
   1.130 +\newcount\rail@textrt
   1.131 +\newcount\rail@textup
   1.132 +\newcount\rail@joinsz
   1.133 +\newcount\rail@joinhsz
   1.134 +\newcount\rail@joinadj
   1.135 +
   1.136 +\newcommand\railinit{
   1.137 +\rail@extra=\railextra
   1.138 +\divide\rail@extra by \railunit
   1.139 +\rail@boxht=\railboxheight
   1.140 +\divide\rail@boxht by \railunit
   1.141 +\rail@boxsp=\railboxskip
   1.142 +\divide\rail@boxsp by \railunit
   1.143 +\rail@boxlf=\railboxleft
   1.144 +\divide\rail@boxlf by \railunit
   1.145 +\rail@boxrt=\railboxright
   1.146 +\divide\rail@boxrt by \railunit
   1.147 +\rail@boxhht=\railboxheight
   1.148 +\divide\rail@boxhht by \railunit
   1.149 +\divide\rail@boxhht by 2
   1.150 +\rail@ovalsp=\railovalspace
   1.151 +\divide\rail@ovalsp by \railunit
   1.152 +\rail@framesp=\railframespace
   1.153 +\divide\rail@framesp by \railunit
   1.154 +\rail@textlf=\railtextleft
   1.155 +\divide\rail@textlf by \railunit
   1.156 +\rail@textrt=\railtextright
   1.157 +\divide\rail@textrt by \railunit
   1.158 +\rail@textup=\railtextup
   1.159 +\divide\rail@textup by \railunit
   1.160 +\rail@joinsz=\railjoinsize
   1.161 +\divide\rail@joinsz by \railunit
   1.162 +\rail@joinhsz=\railjoinsize
   1.163 +\divide\rail@joinhsz by \railunit
   1.164 +\divide\rail@joinhsz by 2
   1.165 +\rail@joinadj=\railjoinadjust
   1.166 +\divide\rail@joinadj by \railunit
   1.167 +}
   1.168 +
   1.169 +\AtBeginDocument{\railinit}
   1.170 +
   1.171 +% \rail@param : declarations for list environment
   1.172 +%
   1.173 +% \railparam{TEXT} : sets \rail@param to TEXT
   1.174 +%
   1.175 +% \rail@reserved : characters reserved for grammar
   1.176 +
   1.177 +\newcommand\railparam[1]{
   1.178 +\def\rail@param{
   1.179 +  \setlength\leftmargin{0pt}\setlength\rightmargin{0pt}
   1.180 +  \setlength\labelwidth{0pt}\setlength\labelsep{0pt}
   1.181 +  \setlength\itemindent{0pt}\setlength\listparindent{0pt}
   1.182 +  #1
   1.183 +}
   1.184 +}
   1.185 +\railparam{}
   1.186 +
   1.187 +\newtoks\rail@reserved
   1.188 +\rail@reserved={:;|*+?[]()'"}
   1.189 +
   1.190 +% \rail@termfont : format setup for terminals
   1.191 +%
   1.192 +% \rail@nontfont : format setup for nonterminals
   1.193 +%
   1.194 +% \rail@annofont : format setup for annotations
   1.195 +%
   1.196 +% \rail@rulefont : format setup for rule names
   1.197 +%
   1.198 +% \rail@indexfont : format setup for index entry
   1.199 +%
   1.200 +% \railtermfont{TEXT} : set terminal format setup to TEXT
   1.201 +%
   1.202 +% \railnontermfont{TEXT} : set nonterminal format setup to TEXT
   1.203 +%
   1.204 +% \railannotatefont{TEXT} : set annotation format setup to TEXT
   1.205 +%
   1.206 +% \railnamefont{TEXT} : set rule name format setup to TEXT
   1.207 +%
   1.208 +% \railindexfont{TEXT} : set index entry format setup to TEXT
   1.209 +
   1.210 +\def\rail@termfont{\ttfamily\upshape}
   1.211 +\def\rail@nontfont{\rmfamily\upshape}
   1.212 +\def\rail@annofont{\rmfamily\itshape}
   1.213 +\def\rail@namefont{\rmfamily\itshape}
   1.214 +\def\rail@indexfont{\rmfamily\itshape}
   1.215 +
   1.216 +\newcommand\railtermfont[1]{
   1.217 +\def\rail@termfont{#1}
   1.218 +}
   1.219 +
   1.220 +\newcommand\railnontermfont[1]{
   1.221 +\def\rail@nontfont{#1}
   1.222 +}
   1.223 +
   1.224 +\newcommand\railannotatefont[1]{
   1.225 +\def\rail@annofont{#1}
   1.226 +}
   1.227 +
   1.228 +\newcommand\railnamefont[1]{
   1.229 +\def\rail@namefont{#1}
   1.230 +}
   1.231 +
   1.232 +\newcommand\railindexfont[1]{
   1.233 +\def\rail@indexfont{#1}
   1.234 +}
   1.235 +
   1.236 +% railroad read/write macros
   1.237 +%
   1.238 +% \begin{rail} TEXT \end{rail} : TEXT is written out to the .rai file,
   1.239 +%                                as \rail@i{NR}{TEXT}. Then the matching
   1.240 +%                                \rail@o{NR}{FMT} from the .rao file is
   1.241 +%                                executed (if defined).
   1.242 +%
   1.243 +% \railoptions{OPTIONS} : OPTIONS are written out to the .rai file,
   1.244 +%                         as \rail@p{OPTIONS}.
   1.245 +%
   1.246 +% \railterm{IDENT,IDENT,...} : format IDENT as terminals. writes out
   1.247 +%                              \rail@t{IDENT} to the .rai file
   1.248 +%
   1.249 +% \railalias{IDENT}{TEXT} : format IDENT as TEXT. defines \rail@t@IDENT as
   1.250 +%                           TEXT.
   1.251 +%
   1.252 +% \railtoken{IDENT}{TEXT} : abbreviates \railalias{IDENT}{TEXT}\railterm{IDENT}
   1.253 +%                           (for backward compatibility)
   1.254 +%
   1.255 +% \rail@setcodes : guards special characters
   1.256 +%
   1.257 +% \rail@makeother{CHARACTER} : sets \catcode of CHARACTER to "other"
   1.258 +%                              used inside a loop for \rail@setcodes
   1.259 +%
   1.260 +% \rail@nr : railroad diagram counter
   1.261 +%
   1.262 +% \ifrail@match : current \rail@i{NR}{TEXT} matches
   1.263 +%
   1.264 +% \rail@first : actions to be done first. read in .rao file,
   1.265 +%               open .rai file if \@filesw true, undefine \rail@first.
   1.266 +%               executed from \begin{rail}, \railoptions and \railterm.
   1.267 +%
   1.268 +% \rail@i{NR}{TEXT} : defines \rail@i@NR as TEXT. written to the .rai
   1.269 +%                     file by \rail, read from the .rao file by
   1.270 +%                     \rail@first
   1.271 +%
   1.272 +% \rail@t{IDENT} : tells Rail that IDENT is to be custom formatted,
   1.273 +%                  written to the .rai file by \railterm.
   1.274 +%
   1.275 +% \rail@o{NR}{TEXT} : defines \rail@o@NR as TEXT, read from the .rao
   1.276 +%                     file by \rail@first.
   1.277 +%
   1.278 +% \rail@p{OPTIONS} : pass options to rail, written to the .rai file by
   1.279 +%                    \railoptions
   1.280 +%
   1.281 +% \rail@write{TEXT} : write TEXT to the .rai file
   1.282 +%
   1.283 +% \rail@warn : warn user for mismatching diagrams
   1.284 +%
   1.285 +% \rail@endwarn : either \relax or \rail@warn
   1.286 +%
   1.287 +% \ifrail@all : checked at the end of the document
   1.288 +
   1.289 +\def\rail@makeother#1{
   1.290 +  \expandafter\catcode\expandafter`\csname\string #1\endcsname=12
   1.291 +}
   1.292 +
   1.293 +\def\rail@setcodes{
   1.294 +\let\par=\relax
   1.295 +\let\\=\relax
   1.296 +\expandafter\@tfor\expandafter\rail@symbol\expandafter:\expandafter=%
   1.297 +  \the\rail@reserved
   1.298 +\do{\expandafter\rail@makeother\rail@symbol}
   1.299 +}
   1.300 +
   1.301 +\newcount\rail@nr
   1.302 +
   1.303 +\newif\ifrail@all
   1.304 +\rail@alltrue
   1.305 +
   1.306 +\newif\ifrail@match
   1.307 +
   1.308 +\def\rail@first{
   1.309 +\begingroup
   1.310 +\makeatletter
   1.311 +\rail@setcodes
   1.312 +\InputIfFileExists{\jobname.rao}{}{\PackageInfo{rail}{No file \jobname.rao}}
   1.313 +\makeatother
   1.314 +\endgroup
   1.315 +\if@filesw
   1.316 +\newwrite\tf@rai
   1.317 +\immediate\openout\tf@rai=\jobname.rai
   1.318 +\fi
   1.319 +\global\let\rail@first=\relax
   1.320 +}
   1.321 +
   1.322 +\long\def\rail@body#1\end{
   1.323 +{
   1.324 +\newlinechar=`^^J
   1.325 +\def\par{\string\par^^J}
   1.326 +\rail@write{\string\rail@i{\number\rail@nr}{#1}}
   1.327 +}
   1.328 +\xdef\rail@i@{#1}
   1.329 +\end
   1.330 +}
   1.331 +
   1.332 +\newenvironment{rail}{
   1.333 +\global\advance\rail@nr by 1
   1.334 +\rail@first
   1.335 +\begingroup
   1.336 +\rail@setcodes
   1.337 +\rail@body
   1.338 +}{
   1.339 +\endgroup
   1.340 +\rail@matchtrue
   1.341 +\@ifundefined{rail@o@\number\rail@nr}{\rail@matchfalse}{}
   1.342 +\expandafter\ifx\csname rail@i@\number\rail@nr\endcsname\rail@i@
   1.343 +\else
   1.344 +\rail@matchfalse
   1.345 +\fi
   1.346 +\ifrail@match
   1.347 +\csname rail@o@\number\rail@nr\endcsname
   1.348 +\else
   1.349 +\PackageWarning{rail}{Railroad diagram {\number\rail@nr} doesn't match}
   1.350 +\global\let\rail@endwarn=\rail@warn
   1.351 +\begin{list}{}{\rail@param}
   1.352 +\rail@begin{1}{}
   1.353 +\rail@setbox{\bfseries ???}
   1.354 +\rail@oval
   1.355 +\rail@end
   1.356 +\end{list}
   1.357 +\fi
   1.358 +}
   1.359 +
   1.360 +\newcommand\railoptions[1]{
   1.361 +\rail@first
   1.362 +\rail@write{\string\rail@p{#1}}
   1.363 +}
   1.364 +
   1.365 +\newcommand\railterm[1]{
   1.366 +\rail@first
   1.367 +\@for\rail@@:=#1\do{
   1.368 +\rail@write{\string\rail@t{\rail@@}}
   1.369 +}
   1.370 +}
   1.371 +
   1.372 +\newcommand\railalias[2]{
   1.373 +\expandafter\def\csname rail@t@#1\endcsname{#2}
   1.374 +}
   1.375 +
   1.376 +\newcommand\railtoken[2]{\railalias{#1}{#2}\railterm{#1}}
   1.377 +
   1.378 +\long\def\rail@i#1#2{
   1.379 +\expandafter\gdef\csname rail@i@#1\endcsname{#2}
   1.380 +}
   1.381 +
   1.382 +\def\rail@o#1#2{
   1.383 +\expandafter\gdef\csname rail@o@#1\endcsname{
   1.384 +\begin{list}{}{\rail@param}
   1.385 +#2
   1.386 +\end{list}
   1.387 +}
   1.388 +}
   1.389 +
   1.390 +\def\rail@t#1{}
   1.391 +
   1.392 +\def\rail@p#1{}
   1.393 +
   1.394 +\long\def\rail@write#1{\@ifundefined{tf@rai}{}{\immediate\write\tf@rai{#1}}}
   1.395 +
   1.396 +\def\rail@warn{
   1.397 +\PackageWarningNoLine{rail}{Railroad diagram(s) may have changed.
   1.398 +                            Use 'rail' and rerun}
   1.399 +}
   1.400 +
   1.401 +\let\rail@endwarn=\relax
   1.402 +
   1.403 +\AtEndDocument{\rail@endwarn}
   1.404 +
   1.405 +% index entry macro
   1.406 +%
   1.407 +% \rail@index{IDENT} : add index entry for IDENT
   1.408 +
   1.409 +\def\rail@index#1{
   1.410 +\index{\rail@indexfont#1}
   1.411 +}
   1.412 +
   1.413 +% railroad formatting primitives
   1.414 +%
   1.415 +% \rail@x : current x
   1.416 +% \rail@y : current y
   1.417 +% \rail@ex : current end x
   1.418 +% \rail@sx : starting x for \rail@cr
   1.419 +% \rail@rx : rightmost previous x for \rail@cr
   1.420 +%
   1.421 +% \rail@tmpa : temporary count
   1.422 +% \rail@tmpb : temporary count
   1.423 +% \rail@tmpc : temporary count
   1.424 +%
   1.425 +% \rail@put : put at (\rail@x,\rail@y)
   1.426 +% \rail@vput : put vector at (\rail@x,\rail@y)
   1.427 +%
   1.428 +% \rail@eline : end line by drawing from \rail@ex to \rail@x
   1.429 +%
   1.430 +% \rail@vreline : end line by drawing a vector from \rail@x to \rail@ex
   1.431 +%
   1.432 +% \rail@vleline : end line by drawing a vector from \rail@ex to \rail@x
   1.433 +%
   1.434 +% \rail@sety{LEVEL} : set \rail@y to level LEVEL
   1.435 +
   1.436 +\newcount\rail@x
   1.437 +\newcount\rail@y
   1.438 +\newcount\rail@ex
   1.439 +\newcount\rail@sx
   1.440 +\newcount\rail@rx
   1.441 +
   1.442 +\newcount\rail@tmpa
   1.443 +\newcount\rail@tmpb
   1.444 +\newcount\rail@tmpc
   1.445 +
   1.446 +\def\rail@put{\put(\number\rail@x,\number\rail@y)}
   1.447 +
   1.448 +\def\rail@vput{\put(\number\rail@ex,\number\rail@y)}
   1.449 +
   1.450 +\def\rail@eline{
   1.451 +\rail@tmpb=\rail@x
   1.452 +\advance\rail@tmpb by -\rail@ex
   1.453 +\rail@put{\line(-1,0){\number\rail@tmpb}}
   1.454 +}
   1.455 +
   1.456 +\def\rail@vreline{
   1.457 +\rail@tmpb=\rail@x
   1.458 +\advance\rail@tmpb by -\rail@ex
   1.459 +\rail@vput{\vector(1,0){\number\rail@tmpb}}
   1.460 +}
   1.461 +
   1.462 +\def\rail@vleline{
   1.463 +\rail@tmpb=\rail@x
   1.464 +\advance\rail@tmpb by -\rail@ex
   1.465 +\rail@put{\vector(-1,0){\number\rail@tmpb}}
   1.466 +}
   1.467 +
   1.468 +\def\rail@sety#1{
   1.469 +\rail@y=#1
   1.470 +\multiply\rail@y by -\rail@boxsp
   1.471 +\advance\rail@y by -\rail@boxht
   1.472 +}
   1.473 +
   1.474 +% \rail@begin{HEIGHT}{NAME} : begin a railroad diagram of height HEIGHT
   1.475 +%
   1.476 +% \rail@end : end a railroad diagram
   1.477 +%
   1.478 +% \rail@expand{IDENT} : expand IDENT
   1.479 +
   1.480 +\def\rail@begin#1#2{
   1.481 +\item
   1.482 +\begin{minipage}[t]{\linewidth}
   1.483 +\ifx\@empty#2\else
   1.484 +{\rail@namefont \rail@expand{#2}}\\*[\railnamesep]
   1.485 +\fi
   1.486 +\unitlength=\railunit
   1.487 +\rail@tmpa=#1
   1.488 +\multiply\rail@tmpa by \rail@boxsp
   1.489 +\begin{picture}(0,\number\rail@tmpa)(0,-\number\rail@tmpa)
   1.490 +\rail@ex=0
   1.491 +\rail@rx=0
   1.492 +\rail@x=\rail@extra
   1.493 +\rail@sx=\rail@x
   1.494 +\rail@sety{0}
   1.495 +}
   1.496 +
   1.497 +\def\rail@end{
   1.498 +\advance\rail@x by \rail@extra
   1.499 +\rail@eline
   1.500 +\end{picture}
   1.501 +\end{minipage}
   1.502 +}
   1.503 +
   1.504 +\def\rail@vend{
   1.505 +\advance\rail@x by \rail@extra
   1.506 +\rail@vreline
   1.507 +\end{picture}
   1.508 +\end{minipage}
   1.509 +}
   1.510 +
   1.511 +\def\rail@expand#1{\@ifundefined{rail@t@#1}{#1}{\csname rail@t@#1\endcsname}}
   1.512 +
   1.513 +% \rail@token{TEXT}[ANNOT] : format token TEXT with annotation
   1.514 +% \rail@ltoken{TEXT}[ANNOT] : format token TEXT with annotation, arrow left
   1.515 +% \rail@rtoken{TEXT}[ANNOT] : format token TEXT with annotation, arrow right
   1.516 +%
   1.517 +% \rail@ctoken{TEXT}[ANNOT] : format token TEXT centered with annotation
   1.518 +% \rail@lctoken{TEXT}[ANNOT] : format token TEXT centered with annotation, arrow left
   1.519 +% \rail@rctoken{TEXT}[ANNOT] : format token TEXT centered with annotation, arrow right
   1.520 +%
   1.521 +% \rail@nont{TEXT}[ANNOT] : format nonterminal TEXT with annotation
   1.522 +% \rail@lnont{TEXT}[ANNOT] : format nonterminal TEXT with annotation, arrow left
   1.523 +% \rail@rnont{TEXT}[ANNOT] : format nonterminal TEXT with annotation. arrow right
   1.524 +%
   1.525 +% \rail@cnont{TEXT}[ANNOT] : format nonterminal TEXT centered with annotation
   1.526 +% \rail@lcnont{TEXT}[ANNOT] : format nonterminal TEXT centered with annotation,
   1.527 +%                             arrow left
   1.528 +% \rail@rcnont{TEXT}[ANNOT] : format nonterminal TEXT centered with annotation,
   1.529 +%                             arrow right
   1.530 +%
   1.531 +% \rail@term{TEXT}[ANNOT] : format terminal TEXT with annotation
   1.532 +% \rail@lterm{TEXT}[ANNOT] : format terminal TEXT with annotation, arrow left
   1.533 +% \rail@rterm{TEXT}[ANNOT] : format terminal TEXT with annotation, arrow right
   1.534 +%
   1.535 +% \rail@cterm{TEXT}[ANNOT] : format terminal TEXT centered with annotation
   1.536 +% \rail@lcterm{TEXT}[ANNOT] : format terminal TEXT centered with annotation, arrow left
   1.537 +% \rail@rcterm{TEXT}[ANNOT] : format terminal TEXT centered with annotation,
   1.538 +%                             arrow right
   1.539 +%
   1.540 +% \rail@annote[TEXT] : format TEXT as annotation
   1.541 +
   1.542 +\def\rail@token#1[#2]{
   1.543 +\rail@setbox{%
   1.544 +{\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
   1.545 +}
   1.546 +\rail@oval
   1.547 +}
   1.548 +
   1.549 +\def\rail@ltoken#1[#2]{
   1.550 +\rail@setbox{%
   1.551 +{\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
   1.552 +}
   1.553 +\rail@vloval
   1.554 +}
   1.555 +
   1.556 +\def\rail@rtoken#1[#2]{
   1.557 +\rail@setbox{%
   1.558 +{\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
   1.559 +}
   1.560 +\rail@vroval
   1.561 +}
   1.562 +
   1.563 +\def\rail@ctoken#1[#2]{
   1.564 +\rail@setbox{%
   1.565 +{\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
   1.566 +}
   1.567 +\rail@coval
   1.568 +}
   1.569 +
   1.570 +\def\rail@lctoken#1[#2]{
   1.571 +\rail@setbox{%
   1.572 +{\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
   1.573 +}
   1.574 +\rail@vlcoval
   1.575 +}
   1.576 +
   1.577 +\def\rail@rctoken#1[#2]{
   1.578 +\rail@setbox{%
   1.579 +{\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
   1.580 +}
   1.581 +\rail@vrcoval
   1.582 +}
   1.583 +
   1.584 +\def\rail@nont#1[#2]{
   1.585 +\rail@setbox{%
   1.586 +{\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
   1.587 +}
   1.588 +\rail@frame
   1.589 +}
   1.590 +
   1.591 +\def\rail@lnont#1[#2]{
   1.592 +\rail@setbox{%
   1.593 +{\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
   1.594 +}
   1.595 +\rail@vlframe
   1.596 +}
   1.597 +
   1.598 +\def\rail@rnont#1[#2]{
   1.599 +\rail@setbox{%
   1.600 +{\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
   1.601 +}
   1.602 +\rail@vrframe
   1.603 +}
   1.604 +
   1.605 +\def\rail@cnont#1[#2]{
   1.606 +\rail@setbox{%
   1.607 +{\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
   1.608 +}
   1.609 +\rail@cframe
   1.610 +}
   1.611 +
   1.612 +\def\rail@lcnont#1[#2]{
   1.613 +\rail@setbox{%
   1.614 +{\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
   1.615 +}
   1.616 +\rail@vlcframe
   1.617 +}
   1.618 +
   1.619 +\def\rail@rcnont#1[#2]{
   1.620 +\rail@setbox{%
   1.621 +{\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
   1.622 +}
   1.623 +\rail@vrcframe
   1.624 +}
   1.625 +
   1.626 +\def\rail@term#1[#2]{
   1.627 +\rail@setbox{%
   1.628 +{\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
   1.629 +}
   1.630 +\rail@oval
   1.631 +}
   1.632 +
   1.633 +\def\rail@lterm#1[#2]{
   1.634 +\rail@setbox{%
   1.635 +{\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
   1.636 +}
   1.637 +\rail@vloval
   1.638 +}
   1.639 +
   1.640 +\def\rail@rterm#1[#2]{
   1.641 +\rail@setbox{%
   1.642 +{\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
   1.643 +}
   1.644 +\rail@vroval
   1.645 +}
   1.646 +
   1.647 +\def\rail@cterm#1[#2]{
   1.648 +\rail@setbox{%
   1.649 +{\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
   1.650 +}
   1.651 +\rail@coval
   1.652 +}
   1.653 +
   1.654 +\def\rail@lcterm#1[#2]{
   1.655 +\rail@setbox{%
   1.656 +{\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
   1.657 +}
   1.658 +\rail@vlcoval
   1.659 +}
   1.660 +
   1.661 +\def\rail@rcterm#1[#2]{
   1.662 +\rail@setbox{%
   1.663 +{\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
   1.664 +}
   1.665 +\rail@vrcoval
   1.666 +}
   1.667 +
   1.668 +\def\rail@annote[#1]{
   1.669 +\rail@setbox{\rail@annofont #1}
   1.670 +\rail@text
   1.671 +}
   1.672 +
   1.673 +% \rail@box : temporary box for \rail@oval and \rail@frame
   1.674 +%
   1.675 +% \rail@setbox{TEXT} : set \rail@box to TEXT, set \rail@tmpa to width
   1.676 +%
   1.677 +% \rail@oval : format \rail@box of width \rail@tmpa inside an oval
   1.678 +% \rail@vloval : format \rail@box of width \rail@tmpa inside an oval, vector left
   1.679 +% \rail@vroval : format \rail@box of width \rail@tmpa inside an oval, vector right
   1.680 +%
   1.681 +% \rail@coval : same as \rail@oval, but centered between \rail@x and
   1.682 +%               \rail@mx
   1.683 +% \rail@vlcoval : same as \rail@oval, but centered between \rail@x and
   1.684 +%                 \rail@mx, vector left
   1.685 +% \rail@vrcoval : same as \rail@oval, but centered between \rail@x and
   1.686 +%                 \rail@mx, vector right
   1.687 +%
   1.688 +% \rail@frame : format \rail@box of width \rail@tmpa inside a frame
   1.689 +% \rail@vlframe : format \rail@box of width \rail@tmpa inside a frame, vector left
   1.690 +% \rail@vrframe : format \rail@box of width \rail@tmpa inside a frame, vector right
   1.691 +%
   1.692 +% \rail@cframe : same as \rail@frame, but centered between \rail@x and
   1.693 +%                \rail@mx
   1.694 +% \rail@vlcframe : same as \rail@frame, but centered between \rail@x and
   1.695 +%                  \rail@mx, vector left
   1.696 +% \rail@vrcframe : same as \rail@frame, but centered between \rail@x and
   1.697 +%                  \rail@mx, vector right
   1.698 +%
   1.699 +% \rail@text : format \rail@box of width \rail@tmpa above the line
   1.700 +
   1.701 +\newbox\rail@box
   1.702 +
   1.703 +\def\rail@setbox#1{
   1.704 +\setbox\rail@box\hbox{\strut#1}
   1.705 +\rail@tmpa=\wd\rail@box
   1.706 +\divide\rail@tmpa by \railunit
   1.707 +}
   1.708 +
   1.709 +\def\rail@oval{
   1.710 +\advance\rail@x by \rail@boxlf
   1.711 +\rail@eline
   1.712 +\advance\rail@tmpa by \rail@ovalsp
   1.713 +\ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi
   1.714 +\rail@tmpb=\rail@tmpa
   1.715 +\divide\rail@tmpb by 2
   1.716 +\advance\rail@y by -\rail@boxhht
   1.717 +\rail@put{\makebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}}
   1.718 +\advance\rail@y by \rail@boxhht
   1.719 +\advance\rail@x by \rail@tmpb
   1.720 +\rail@put{\oval(\number\rail@tmpa,\number\rail@boxht)}
   1.721 +\advance\rail@x by \rail@tmpb
   1.722 +\rail@ex=\rail@x
   1.723 +\advance\rail@x by \rail@boxrt
   1.724 +}
   1.725 +
   1.726 +\def\rail@vloval{
   1.727 +\advance\rail@x by \rail@boxlf
   1.728 +\rail@eline
   1.729 +\advance\rail@tmpa by \rail@ovalsp
   1.730 +\ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi
   1.731 +\rail@tmpb=\rail@tmpa
   1.732 +\divide\rail@tmpb by 2
   1.733 +\advance\rail@y by -\rail@boxhht
   1.734 +\rail@put{\makebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}}
   1.735 +\advance\rail@y by \rail@boxhht
   1.736 +\advance\rail@x by \rail@tmpb
   1.737 +\rail@put{\oval(\number\rail@tmpa,\number\rail@boxht)}
   1.738 +\advance\rail@x by \rail@tmpb
   1.739 +\rail@ex=\rail@x
   1.740 +\advance\rail@x by \rail@boxrt
   1.741 +\rail@vleline
   1.742 +}
   1.743 +
   1.744 +\def\rail@vroval{
   1.745 +\advance\rail@x by \rail@boxlf
   1.746 +\rail@vreline
   1.747 +\advance\rail@tmpa by \rail@ovalsp
   1.748 +\ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi
   1.749 +\rail@tmpb=\rail@tmpa
   1.750 +\divide\rail@tmpb by 2
   1.751 +\advance\rail@y by -\rail@boxhht
   1.752 +\rail@put{\makebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}}
   1.753 +\advance\rail@y by \rail@boxhht
   1.754 +\advance\rail@x by \rail@tmpb
   1.755 +\rail@put{\oval(\number\rail@tmpa,\number\rail@boxht)}
   1.756 +\advance\rail@x by \rail@tmpb
   1.757 +\rail@ex=\rail@x
   1.758 +\advance\rail@x by \rail@boxrt
   1.759 +}
   1.760 +
   1.761 +\def\rail@coval{
   1.762 +\rail@tmpb=\rail@tmpa
   1.763 +\advance\rail@tmpb by \rail@ovalsp
   1.764 +\ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi
   1.765 +\advance\rail@tmpb by \rail@boxlf
   1.766 +\advance\rail@tmpb by \rail@boxrt
   1.767 +\rail@tmpc=\rail@mx
   1.768 +\advance\rail@tmpc by -\rail@x
   1.769 +\advance\rail@tmpc by -\rail@tmpb
   1.770 +\divide\rail@tmpc by 2
   1.771 +\ifnum\rail@tmpc>0
   1.772 +\advance\rail@x by \rail@tmpc
   1.773 +\fi
   1.774 +\rail@oval
   1.775 +}
   1.776 +
   1.777 +\def\rail@vlcoval{
   1.778 +\rail@tmpb=\rail@tmpa
   1.779 +\advance\rail@tmpb by \rail@ovalsp
   1.780 +\ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi
   1.781 +\advance\rail@tmpb by \rail@boxlf
   1.782 +\advance\rail@tmpb by \rail@boxrt
   1.783 +\rail@tmpc=\rail@mx
   1.784 +\advance\rail@tmpc by -\rail@x
   1.785 +\advance\rail@tmpc by -\rail@tmpb
   1.786 +\divide\rail@tmpc by 2
   1.787 +\ifnum\rail@tmpc>0
   1.788 +\advance\rail@x by \rail@tmpc
   1.789 +\fi
   1.790 +\rail@vloval
   1.791 +}
   1.792 +
   1.793 +\def\rail@vrcoval{
   1.794 +\rail@tmpb=\rail@tmpa
   1.795 +\advance\rail@tmpb by \rail@ovalsp
   1.796 +\ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi
   1.797 +\advance\rail@tmpb by \rail@boxlf
   1.798 +\advance\rail@tmpb by \rail@boxrt
   1.799 +\rail@tmpc=\rail@mx
   1.800 +\advance\rail@tmpc by -\rail@x
   1.801 +\advance\rail@tmpc by -\rail@tmpb
   1.802 +\divide\rail@tmpc by 2
   1.803 +\ifnum\rail@tmpc>0
   1.804 +\advance\rail@x by \rail@tmpc
   1.805 +\fi
   1.806 +\rail@vroval
   1.807 +}
   1.808 +
   1.809 +\def\rail@frame{
   1.810 +\advance\rail@x by \rail@boxlf
   1.811 +\rail@eline
   1.812 +\advance\rail@tmpa by \rail@framesp
   1.813 +\ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi
   1.814 +\advance\rail@y by -\rail@boxhht
   1.815 +\rail@put{\framebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}}
   1.816 +\advance\rail@y by \rail@boxhht
   1.817 +\advance\rail@x by \rail@tmpa
   1.818 +\rail@ex=\rail@x
   1.819 +\advance\rail@x by \rail@boxrt
   1.820 +}
   1.821 +
   1.822 +\def\rail@vlframe{
   1.823 +\advance\rail@x by \rail@boxlf
   1.824 +\rail@eline
   1.825 +\advance\rail@tmpa by \rail@framesp
   1.826 +\ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi
   1.827 +\advance\rail@y by -\rail@boxhht
   1.828 +\rail@put{\framebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}}
   1.829 +\advance\rail@y by \rail@boxhht
   1.830 +\advance\rail@x by \rail@tmpa
   1.831 +\rail@ex=\rail@x
   1.832 +\advance\rail@x by \rail@boxrt
   1.833 +\rail@vleline
   1.834 +}
   1.835 +
   1.836 +\def\rail@vrframe{
   1.837 +\advance\rail@x by \rail@boxlf
   1.838 +\rail@vreline
   1.839 +\advance\rail@tmpa by \rail@framesp
   1.840 +\ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi
   1.841 +\advance\rail@y by -\rail@boxhht
   1.842 +\rail@put{\framebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}}
   1.843 +\advance\rail@y by \rail@boxhht
   1.844 +\advance\rail@x by \rail@tmpa
   1.845 +\rail@ex=\rail@x
   1.846 +\advance\rail@x by \rail@boxrt
   1.847 +}
   1.848 +
   1.849 +\def\rail@cframe{
   1.850 +\rail@tmpb=\rail@tmpa
   1.851 +\advance\rail@tmpb by \rail@framesp
   1.852 +\ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi
   1.853 +\advance\rail@tmpb by \rail@boxlf
   1.854 +\advance\rail@tmpb by \rail@boxrt
   1.855 +\rail@tmpc=\rail@mx
   1.856 +\advance\rail@tmpc by -\rail@x
   1.857 +\advance\rail@tmpc by -\rail@tmpb
   1.858 +\divide\rail@tmpc by 2
   1.859 +\ifnum\rail@tmpc>0
   1.860 +\advance\rail@x by \rail@tmpc
   1.861 +\fi
   1.862 +\rail@frame
   1.863 +}
   1.864 +
   1.865 +\def\rail@vlcframe{
   1.866 +\rail@tmpb=\rail@tmpa
   1.867 +\advance\rail@tmpb by \rail@framesp
   1.868 +\ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi
   1.869 +\advance\rail@tmpb by \rail@boxlf
   1.870 +\advance\rail@tmpb by \rail@boxrt
   1.871 +\rail@tmpc=\rail@mx
   1.872 +\advance\rail@tmpc by -\rail@x
   1.873 +\advance\rail@tmpc by -\rail@tmpb
   1.874 +\divide\rail@tmpc by 2
   1.875 +\ifnum\rail@tmpc>0
   1.876 +\advance\rail@x by \rail@tmpc
   1.877 +\fi
   1.878 +\rail@vlframe
   1.879 +}
   1.880 +
   1.881 +\def\rail@vrcframe{
   1.882 +\rail@tmpb=\rail@tmpa
   1.883 +\advance\rail@tmpb by \rail@framesp
   1.884 +\ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi
   1.885 +\advance\rail@tmpb by \rail@boxlf
   1.886 +\advance\rail@tmpb by \rail@boxrt
   1.887 +\rail@tmpc=\rail@mx
   1.888 +\advance\rail@tmpc by -\rail@x
   1.889 +\advance\rail@tmpc by -\rail@tmpb
   1.890 +\divide\rail@tmpc by 2
   1.891 +\ifnum\rail@tmpc>0
   1.892 +\advance\rail@x by \rail@tmpc
   1.893 +\fi
   1.894 +\rail@vrframe
   1.895 +}
   1.896 +
   1.897 +\def\rail@text{
   1.898 +\advance\rail@x by \rail@textlf
   1.899 +\advance\rail@y by \rail@textup
   1.900 +\rail@put{\box\rail@box}
   1.901 +\advance\rail@y by -\rail@textup
   1.902 +\advance\rail@x by \rail@tmpa
   1.903 +\advance\rail@x by \rail@textrt
   1.904 +}
   1.905 +
   1.906 +% alternatives
   1.907 +%
   1.908 +% \rail@jx \rail@jy : current join point
   1.909 +%
   1.910 +% \rail@gx \rail@gy \rail@gex \rail@grx : global versions of \rail@x etc,
   1.911 +%                                         to pass values over group closings
   1.912 +%
   1.913 +% \rail@mx : maximum x so far
   1.914 +%
   1.915 +% \rail@sy : starting \rail@y for alternatives
   1.916 +%
   1.917 +% \rail@jput : put at (\rail@jx,\rail@jy)
   1.918 +%
   1.919 +% \rail@joval[PART] : put \oval[PART] with adjust
   1.920 +
   1.921 +\newcount\rail@jx
   1.922 +\newcount\rail@jy
   1.923 +
   1.924 +\newcount\rail@gx
   1.925 +\newcount\rail@gy
   1.926 +\newcount\rail@gex
   1.927 +\newcount\rail@grx
   1.928 +
   1.929 +\newcount\rail@sy
   1.930 +\newcount\rail@mx
   1.931 +
   1.932 +\def\rail@jput{
   1.933 +\put(\number\rail@jx,\number\rail@jy)
   1.934 +}
   1.935 +
   1.936 +\def\rail@joval[#1]{
   1.937 +\advance\rail@jx by \rail@joinadj
   1.938 +\rail@jput{\oval(\number\rail@joinsz,\number\rail@joinsz)[#1]}
   1.939 +\advance\rail@jx by -\rail@joinadj
   1.940 +}
   1.941 +
   1.942 +% \rail@barsplit : incoming split for '|'
   1.943 +%
   1.944 +% \rail@plussplit : incoming split for '+'
   1.945 +%
   1.946 +
   1.947 +\def\rail@barsplit{
   1.948 +\advance\rail@jy by -\rail@joinhsz
   1.949 +\rail@joval[tr]
   1.950 +\advance\rail@jx by \rail@joinhsz
   1.951 +}
   1.952 +
   1.953 +\def\rail@plussplit{
   1.954 +\advance\rail@jy by -\rail@joinhsz
   1.955 +\advance\rail@jx by \rail@joinsz
   1.956 +\rail@joval[tl]
   1.957 +\advance\rail@jx by -\rail@joinhsz
   1.958 +}
   1.959 +
   1.960 +% \rail@alt{SPLIT} : start alternatives with incoming split SPLIT
   1.961 +%
   1.962 +
   1.963 +\def\rail@alt#1{
   1.964 +\rail@sy=\rail@y
   1.965 +\rail@jx=\rail@x
   1.966 +\rail@jy=\rail@y
   1.967 +\advance\rail@x by \rail@joinsz
   1.968 +\rail@mx=0
   1.969 +\let\rail@list=\@empty
   1.970 +\let\rail@comma=\@empty
   1.971 +\let\rail@split=#1
   1.972 +\begingroup
   1.973 +\rail@sx=\rail@x
   1.974 +\rail@rx=0
   1.975 +}
   1.976 +
   1.977 +% \rail@nextalt{FIX}{Y} : start next alternative at vertical position Y
   1.978 +%                         and fix-up FIX
   1.979 +%
   1.980 +
   1.981 +\def\rail@nextalt#1#2{
   1.982 +\global\rail@gx=\rail@x
   1.983 +\global\rail@gy=\rail@y
   1.984 +\global\rail@gex=\rail@ex
   1.985 +\global\rail@grx=\rail@rx
   1.986 +\endgroup
   1.987 +#1
   1.988 +\ifnum\rail@gx>\rail@mx\rail@mx=\rail@gx\fi
   1.989 +\ifnum\rail@grx>\rail@mx\rail@mx=\rail@grx\fi
   1.990 +\edef\rail@list{\rail@list\rail@comma\number\rail@gex:\number\rail@gy}
   1.991 +\def\rail@comma{,}
   1.992 +\rail@split
   1.993 +\let\rail@split=\@empty
   1.994 +\rail@sety{#2}
   1.995 +\rail@tmpa=\rail@jy
   1.996 +\advance\rail@tmpa by -\rail@y
   1.997 +\advance\rail@tmpa by -\rail@joinhsz
   1.998 +\rail@jput{\line(0,-1){\number\rail@tmpa}}
   1.999 +\rail@jy=\rail@y
  1.1000 +\advance\rail@jy by \rail@joinhsz
  1.1001 +\advance\rail@jx by \rail@joinhsz
  1.1002 +\rail@joval[bl]
  1.1003 +\advance\rail@jx by -\rail@joinhsz
  1.1004 +\rail@ex=\rail@x
  1.1005 +\begingroup
  1.1006 +\rail@sx=\rail@x
  1.1007 +\rail@rx=0
  1.1008 +}
  1.1009 +
  1.1010 +% \rail@barjoin : outgoing join for first '|' alternative
  1.1011 +%
  1.1012 +% \rail@plusjoin : outgoing join for first '+' alternative
  1.1013 +%
  1.1014 +% \rail@altjoin : join for subsequent alternative
  1.1015 +%
  1.1016 +
  1.1017 +\def\rail@barjoin{
  1.1018 +\ifnum\rail@y<\rail@sy
  1.1019 +\global\rail@gex=\rail@jx
  1.1020 +\else
  1.1021 +\global\rail@gex=\rail@ex
  1.1022 +\fi
  1.1023 +\advance\rail@jy by -\rail@joinhsz
  1.1024 +\rail@joval[tl]
  1.1025 +\advance\rail@jx by -\rail@joinhsz
  1.1026 +\ifnum\rail@y<\rail@sy
  1.1027 +\rail@altjoin
  1.1028 +\fi
  1.1029 +}
  1.1030 +
  1.1031 +\def\rail@plusjoin{
  1.1032 +\global\rail@gex=\rail@ex
  1.1033 +\advance\rail@jy by -\rail@joinhsz
  1.1034 +\advance\rail@jx by -\rail@joinsz
  1.1035 +\rail@joval[tr]
  1.1036 +\advance\rail@jx by \rail@joinhsz
  1.1037 +}
  1.1038 +
  1.1039 +\def\rail@altjoin{
  1.1040 +\rail@eline
  1.1041 +\rail@tmpa=\rail@jy
  1.1042 +\advance\rail@tmpa by -\rail@y
  1.1043 +\advance\rail@tmpa by -\rail@joinhsz
  1.1044 +\rail@jput{\line(0,-1){\number\rail@tmpa}}
  1.1045 +\rail@jy=\rail@y
  1.1046 +\advance\rail@jy by \rail@joinhsz
  1.1047 +\advance\rail@jx by -\rail@joinhsz
  1.1048 +\rail@joval[br]
  1.1049 +\advance\rail@jx by \rail@joinhsz
  1.1050 +}
  1.1051 +
  1.1052 +% \rail@eltsplit EX:Y; : split EX:Y into \rail@ex \rail@y
  1.1053 +%
  1.1054 +% \rail@endalt{JOIN} : end alternatives with outgoing join JOIN
  1.1055 +
  1.1056 +\def\rail@eltsplit#1:#2;{\rail@ex=#1\rail@y=#2}
  1.1057 +
  1.1058 +\def\rail@endalt#1{
  1.1059 +\global\rail@gx=\rail@x
  1.1060 +\global\rail@gy=\rail@y
  1.1061 +\global\rail@gex=\rail@ex
  1.1062 +\global\rail@grx=\rail@rx
  1.1063 +\endgroup
  1.1064 +\ifnum\rail@gx>\rail@mx\rail@mx=\rail@gx\fi
  1.1065 +\ifnum\rail@grx>\rail@mx\rail@mx=\rail@grx\fi
  1.1066 +\edef\rail@list{\rail@list\rail@comma\number\rail@gex:\number\rail@gy}
  1.1067 +\rail@x=\rail@mx
  1.1068 +\rail@jx=\rail@x
  1.1069 +\rail@jy=\rail@sy
  1.1070 +\advance\rail@jx by \rail@joinsz
  1.1071 +\let\rail@join=#1
  1.1072 +\@for\rail@elt:=\rail@list\do{
  1.1073 +\expandafter\rail@eltsplit\rail@elt;
  1.1074 +\rail@join
  1.1075 +\let\rail@join=\rail@altjoin
  1.1076 +}
  1.1077 +\rail@x=\rail@mx
  1.1078 +\rail@y=\rail@sy
  1.1079 +\rail@ex=\rail@gex
  1.1080 +\advance\rail@x by \rail@joinsz
  1.1081 +}
  1.1082 +
  1.1083 +% \rail@bar : start '|' alternatives
  1.1084 +%
  1.1085 +% \rail@nextbar : next '|' alternative
  1.1086 +%
  1.1087 +% \rail@endbar : end '|' alternatives
  1.1088 +%
  1.1089 +
  1.1090 +\def\rail@bar{
  1.1091 +\rail@alt\rail@barsplit
  1.1092 +}
  1.1093 +
  1.1094 +\def\rail@nextbar{
  1.1095 +\rail@nextalt\relax
  1.1096 +}
  1.1097 +
  1.1098 +\def\rail@endbar{
  1.1099 +\rail@endalt\rail@barjoin
  1.1100 +}
  1.1101 +
  1.1102 +% \rail@plus : start '+' alternatives
  1.1103 +%
  1.1104 +% \rail@nextplus: next '+' alternative
  1.1105 +%
  1.1106 +% \rail@endplus : end '+' alternatives
  1.1107 +%
  1.1108 +
  1.1109 +\def\rail@plus{
  1.1110 +\rail@alt\rail@plussplit
  1.1111 +}
  1.1112 +
  1.1113 +\def\rail@nextplus{
  1.1114 +\rail@nextalt\rail@fixplus
  1.1115 +}
  1.1116 +
  1.1117 +\def\rail@fixplus{
  1.1118 +\ifnum\rail@gy<\rail@sy
  1.1119 +\begingroup
  1.1120 +\rail@x=\rail@gx
  1.1121 +\rail@y=\rail@gy
  1.1122 +\rail@ex=\rail@gex
  1.1123 +\rail@rx=\rail@grx
  1.1124 +\ifnum\rail@x<\rail@rx
  1.1125 +\rail@x=\rail@rx
  1.1126 +\fi
  1.1127 +\rail@eline
  1.1128 +\rail@jx=\rail@x
  1.1129 +\rail@jy=\rail@y
  1.1130 +\advance\rail@jy by \rail@joinhsz
  1.1131 +\rail@joval[br]
  1.1132 +\advance\rail@jx by \rail@joinhsz
  1.1133 +\rail@tmpa=\rail@sy
  1.1134 +\advance\rail@tmpa by -\rail@joinhsz
  1.1135 +\advance\rail@tmpa by -\rail@jy
  1.1136 +\rail@jput{\line(0,1){\number\rail@tmpa}}
  1.1137 +\rail@jy=\rail@sy
  1.1138 +\advance\rail@jy by -\rail@joinhsz
  1.1139 +\advance\rail@jx by \rail@joinhsz
  1.1140 +\rail@joval[tl]
  1.1141 +\advance\rail@jy by \rail@joinhsz
  1.1142 +\global\rail@gx=\rail@jx
  1.1143 +\global\rail@gy=\rail@jy
  1.1144 +\global\rail@gex=\rail@gx
  1.1145 +\global\rail@grx=\rail@rx
  1.1146 +\endgroup
  1.1147 +\fi
  1.1148 +}
  1.1149 +
  1.1150 +\def\rail@endplus{
  1.1151 +\rail@endalt\rail@plusjoin
  1.1152 +}
  1.1153 +
  1.1154 +% \rail@cr{Y} : carriage return to vertical position Y
  1.1155 +
  1.1156 +\def\rail@cr#1{
  1.1157 +\rail@tmpa=\rail@sx
  1.1158 +\advance\rail@tmpa by \rail@joinsz
  1.1159 +\ifnum\rail@x<\rail@tmpa\rail@x=\rail@tmpa\fi
  1.1160 +\rail@eline
  1.1161 +\rail@jx=\rail@x
  1.1162 +\rail@jy=\rail@y
  1.1163 +\advance\rail@x by \rail@joinsz
  1.1164 +\ifnum\rail@x>\rail@rx\rail@rx=\rail@x\fi
  1.1165 +\advance\rail@jy by -\rail@joinhsz
  1.1166 +\rail@joval[tr]
  1.1167 +\advance\rail@jx by \rail@joinhsz
  1.1168 +\rail@sety{#1}
  1.1169 +\rail@tmpa=\rail@jy
  1.1170 +\advance\rail@tmpa by -\rail@y
  1.1171 +\advance\rail@tmpa by -\rail@boxsp
  1.1172 +\advance\rail@tmpa by -\rail@joinhsz
  1.1173 +\rail@jput{\line(0,-1){\number\rail@tmpa}}
  1.1174 +\rail@jy=\rail@y
  1.1175 +\advance\rail@jy by \rail@boxsp
  1.1176 +\advance\rail@jy by \rail@joinhsz
  1.1177 +\advance\rail@jx by -\rail@joinhsz
  1.1178 +\rail@joval[br]
  1.1179 +\advance\rail@jy by -\rail@joinhsz
  1.1180 +\rail@tmpa=\rail@jx
  1.1181 +\advance\rail@tmpa by -\rail@sx
  1.1182 +\advance\rail@tmpa by -\rail@joinhsz
  1.1183 +\rail@jput{\line(-1,0){\number\rail@tmpa}}
  1.1184 +\rail@jx=\rail@sx
  1.1185 +\advance\rail@jx by \rail@joinhsz
  1.1186 +\advance\rail@jy by -\rail@joinhsz
  1.1187 +\rail@joval[tl]
  1.1188 +\advance\rail@jx by -\rail@joinhsz
  1.1189 +\rail@tmpa=\rail@boxsp
  1.1190 +\advance\rail@tmpa by -\rail@joinsz
  1.1191 +\rail@jput{\line(0,-1){\number\rail@tmpa}}
  1.1192 +\advance\rail@jy by -\rail@tmpa
  1.1193 +\advance\rail@jx by \rail@joinhsz
  1.1194 +\rail@joval[bl]
  1.1195 +\rail@x=\rail@jx
  1.1196 +\rail@ex=\rail@x
  1.1197 +}
  1.1198 +
  1.1199 +% default setup for Isabelle
  1.1200 +\newenvironment{railoutput}%
  1.1201 +{\begin{list}{}{\rail@param}\def\rail@expand{\relax}\makeatletter}{\makeatother\end{list}}
  1.1202 +
  1.1203 +\def\rail@termfont{\isabellestyle{tt}}
  1.1204 +\def\rail@nontfont{\isabellestyle{it}}
  1.1205 +\def\rail@namefont{\isabellestyle{it}}