src/Tools/isac/Doc/railsetup.sty
changeset 60188 422186a35be8
parent 60187 751b8a13c271
child 60189 6b021e8cb8da
     1.1 --- a/src/Tools/isac/Doc/railsetup.sty	Thu Apr 08 13:09:44 2021 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,1202 +0,0 @@
     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}}