src/Tools/isac/Doc/railsetup.sty
changeset 60188 422186a35be8
parent 59827 168abe8dd1e3
equal deleted inserted replaced
60187:751b8a13c271 60188:422186a35be8
     1 % rail.sty - style file to support railroad diagrams
       
     2 %
       
     3 % 09-Jul-90 L. Rooijakkers
       
     4 % 08-Oct-90 L. Rooijakkers	fixed centering bug when \rail@tmpc<0.
       
     5 % 07-Feb-91 L. Rooijakkers	added \railoptions command, indexing
       
     6 % 08-Feb-91 L. Rooijakkers	minor fixes
       
     7 % 28-Jun-94 K. Barthelmann	turned into LaTeX2e package
       
     8 % 08-Dec-96 K. Barthelmann	replaced \@writefile
       
     9 % 13-Dec-96 K. Barthelmann	cleanup
       
    10 % 22-Feb-98 K. Barthelmann	fixed catcodes of special characters
       
    11 % 18-Apr-98 K. Barthelmann	fixed \par handling
       
    12 % 19-May-98 J. Olsson		Added new macros to support arrow heads.
       
    13 % 26-Jul-98 K. Barthelmann	changed \par to output newlines
       
    14 % 02-May-11 M. Wenzel           default setup for Isabelle
       
    15 %
       
    16 % This style file needs to be used in conjunction with the 'rail'
       
    17 % program. Running LaTeX as 'latex file' produces file.rai, which should be
       
    18 % processed by Rail with 'rail file'. This produces file.rao, which will
       
    19 % be picked up by LaTeX on the next 'latex file' run.
       
    20 %
       
    21 % LaTeX will warn if there is no file.rao or it's out of date.
       
    22 %
       
    23 % The macros in this file thus consist of two parts: those that read and
       
    24 % write the .rai and .rao files, and those that do the actual formatting
       
    25 % of the railroad diagrams.
       
    26 
       
    27 \NeedsTeXFormat{LaTeX2e}
       
    28 \ProvidesPackage{rail}[1998/05/19]
       
    29 
       
    30 % railroad diagram formatting parameters (user level)
       
    31 % all of these are copied into their internal versions by \railinit
       
    32 %
       
    33 % \railunit : \unitlength within railroad diagrams
       
    34 % \railextra : extra length at outside of diagram
       
    35 % \railboxheight : height of ovals and frames
       
    36 % \railboxskip : vertical space between lines
       
    37 % \railboxleft : space to the left of a box
       
    38 % \railboxright : space to the right of a box
       
    39 % \railovalspace : extra space around contents of oval
       
    40 % \railframespace : extra space around contents of frame
       
    41 % \railtextleft : space to the left of text
       
    42 % \railtextright : space to the right of text
       
    43 % \railtextup : space to lift text up
       
    44 % \railjoinsize : circle size of join/split arcs
       
    45 % \railjoinadjust : space to adjust join
       
    46 %
       
    47 % \railnamesep : separator between name and rule body
       
    48 
       
    49 \newlength\railunit
       
    50 \newlength\railextra
       
    51 \newlength\railboxheight
       
    52 \newlength\railboxskip
       
    53 \newlength\railboxleft
       
    54 \newlength\railboxright
       
    55 \newlength\railovalspace
       
    56 \newlength\railframespace
       
    57 \newlength\railtextleft
       
    58 \newlength\railtextright
       
    59 \newlength\railtextup
       
    60 \newlength\railjoinsize
       
    61 \newlength\railjoinadjust
       
    62 \newlength\railnamesep
       
    63 
       
    64 % initialize the parameters
       
    65 
       
    66 \setlength\railunit{1sp}
       
    67 \setlength\railextra{4ex}
       
    68 \setlength\railboxleft{1ex}
       
    69 \setlength\railboxright{1ex}
       
    70 \setlength\railovalspace{2ex}
       
    71 \setlength\railframespace{2ex}
       
    72 \setlength\railtextleft{1ex}
       
    73 \setlength\railtextright{1ex}
       
    74 \setlength\railjoinadjust{0pt}
       
    75 \setlength\railnamesep{1ex}
       
    76 
       
    77 \DeclareOption{10pt}{
       
    78   \setlength\railboxheight{16pt}
       
    79   \setlength\railboxskip{24pt}
       
    80   \setlength\railtextup{5pt}
       
    81   \setlength\railjoinsize{16pt}
       
    82 }
       
    83 \DeclareOption{11pt}{
       
    84   \setlength\railboxheight{16pt}
       
    85   \setlength\railboxskip{24pt}
       
    86   \setlength\railtextup{5pt}
       
    87   \setlength\railjoinsize{16pt}
       
    88 }
       
    89 \DeclareOption{12pt}{
       
    90   \setlength\railboxheight{20pt}
       
    91   \setlength\railboxskip{28pt}
       
    92   \setlength\railtextup{6pt}
       
    93   \setlength\railjoinsize{20pt}
       
    94 }
       
    95 
       
    96 \ExecuteOptions{10pt}
       
    97 \ProcessOptions
       
    98 
       
    99 % internal versions of the formatting parameters
       
   100 %
       
   101 % \rail@extra   : \railextra
       
   102 % \rail@boxht   : \railboxheight
       
   103 % \rail@boxsp   : \railboxskip
       
   104 % \rail@boxlf   : \railboxleft
       
   105 % \rail@boxrt   : \railboxright
       
   106 % \rail@boxhht  : \railboxheight / 2
       
   107 % \rail@ovalsp  : \railovalspace
       
   108 % \rail@framesp : \railframespace
       
   109 % \rail@textlf  : \railtextleft
       
   110 % \rail@textrt  : \railtextright
       
   111 % \rail@textup  : \railtextup
       
   112 % \rail@joinsz  : \railjoinsize
       
   113 % \rail@joinhsz : \railjoinsize / 2
       
   114 % \rail@joinadj : \railjoinadjust
       
   115 %
       
   116 % \railinit : internalize all of the parameters.
       
   117 
       
   118 \newcount\rail@extra
       
   119 \newcount\rail@boxht
       
   120 \newcount\rail@boxsp
       
   121 \newcount\rail@boxlf
       
   122 \newcount\rail@boxrt
       
   123 \newcount\rail@boxhht
       
   124 \newcount\rail@ovalsp
       
   125 \newcount\rail@framesp
       
   126 \newcount\rail@textlf
       
   127 \newcount\rail@textrt
       
   128 \newcount\rail@textup
       
   129 \newcount\rail@joinsz
       
   130 \newcount\rail@joinhsz
       
   131 \newcount\rail@joinadj
       
   132 
       
   133 \newcommand\railinit{
       
   134 \rail@extra=\railextra
       
   135 \divide\rail@extra by \railunit
       
   136 \rail@boxht=\railboxheight
       
   137 \divide\rail@boxht by \railunit
       
   138 \rail@boxsp=\railboxskip
       
   139 \divide\rail@boxsp by \railunit
       
   140 \rail@boxlf=\railboxleft
       
   141 \divide\rail@boxlf by \railunit
       
   142 \rail@boxrt=\railboxright
       
   143 \divide\rail@boxrt by \railunit
       
   144 \rail@boxhht=\railboxheight
       
   145 \divide\rail@boxhht by \railunit
       
   146 \divide\rail@boxhht by 2
       
   147 \rail@ovalsp=\railovalspace
       
   148 \divide\rail@ovalsp by \railunit
       
   149 \rail@framesp=\railframespace
       
   150 \divide\rail@framesp by \railunit
       
   151 \rail@textlf=\railtextleft
       
   152 \divide\rail@textlf by \railunit
       
   153 \rail@textrt=\railtextright
       
   154 \divide\rail@textrt by \railunit
       
   155 \rail@textup=\railtextup
       
   156 \divide\rail@textup by \railunit
       
   157 \rail@joinsz=\railjoinsize
       
   158 \divide\rail@joinsz by \railunit
       
   159 \rail@joinhsz=\railjoinsize
       
   160 \divide\rail@joinhsz by \railunit
       
   161 \divide\rail@joinhsz by 2
       
   162 \rail@joinadj=\railjoinadjust
       
   163 \divide\rail@joinadj by \railunit
       
   164 }
       
   165 
       
   166 \AtBeginDocument{\railinit}
       
   167 
       
   168 % \rail@param : declarations for list environment
       
   169 %
       
   170 % \railparam{TEXT} : sets \rail@param to TEXT
       
   171 %
       
   172 % \rail@reserved : characters reserved for grammar
       
   173 
       
   174 \newcommand\railparam[1]{
       
   175 \def\rail@param{
       
   176   \setlength\leftmargin{0pt}\setlength\rightmargin{0pt}
       
   177   \setlength\labelwidth{0pt}\setlength\labelsep{0pt}
       
   178   \setlength\itemindent{0pt}\setlength\listparindent{0pt}
       
   179   #1
       
   180 }
       
   181 }
       
   182 \railparam{}
       
   183 
       
   184 \newtoks\rail@reserved
       
   185 \rail@reserved={:;|*+?[]()'"}
       
   186 
       
   187 % \rail@termfont : format setup for terminals
       
   188 %
       
   189 % \rail@nontfont : format setup for nonterminals
       
   190 %
       
   191 % \rail@annofont : format setup for annotations
       
   192 %
       
   193 % \rail@rulefont : format setup for rule names
       
   194 %
       
   195 % \rail@indexfont : format setup for index entry
       
   196 %
       
   197 % \railtermfont{TEXT} : set terminal format setup to TEXT
       
   198 %
       
   199 % \railnontermfont{TEXT} : set nonterminal format setup to TEXT
       
   200 %
       
   201 % \railannotatefont{TEXT} : set annotation format setup to TEXT
       
   202 %
       
   203 % \railnamefont{TEXT} : set rule name format setup to TEXT
       
   204 %
       
   205 % \railindexfont{TEXT} : set index entry format setup to TEXT
       
   206 
       
   207 \def\rail@termfont{\ttfamily\upshape}
       
   208 \def\rail@nontfont{\rmfamily\upshape}
       
   209 \def\rail@annofont{\rmfamily\itshape}
       
   210 \def\rail@namefont{\rmfamily\itshape}
       
   211 \def\rail@indexfont{\rmfamily\itshape}
       
   212 
       
   213 \newcommand\railtermfont[1]{
       
   214 \def\rail@termfont{#1}
       
   215 }
       
   216 
       
   217 \newcommand\railnontermfont[1]{
       
   218 \def\rail@nontfont{#1}
       
   219 }
       
   220 
       
   221 \newcommand\railannotatefont[1]{
       
   222 \def\rail@annofont{#1}
       
   223 }
       
   224 
       
   225 \newcommand\railnamefont[1]{
       
   226 \def\rail@namefont{#1}
       
   227 }
       
   228 
       
   229 \newcommand\railindexfont[1]{
       
   230 \def\rail@indexfont{#1}
       
   231 }
       
   232 
       
   233 % railroad read/write macros
       
   234 %
       
   235 % \begin{rail} TEXT \end{rail} : TEXT is written out to the .rai file,
       
   236 %                                as \rail@i{NR}{TEXT}. Then the matching
       
   237 %                                \rail@o{NR}{FMT} from the .rao file is
       
   238 %                                executed (if defined).
       
   239 %
       
   240 % \railoptions{OPTIONS} : OPTIONS are written out to the .rai file,
       
   241 %                         as \rail@p{OPTIONS}.
       
   242 %
       
   243 % \railterm{IDENT,IDENT,...} : format IDENT as terminals. writes out
       
   244 %                              \rail@t{IDENT} to the .rai file
       
   245 %
       
   246 % \railalias{IDENT}{TEXT} : format IDENT as TEXT. defines \rail@t@IDENT as
       
   247 %                           TEXT.
       
   248 %
       
   249 % \railtoken{IDENT}{TEXT} : abbreviates \railalias{IDENT}{TEXT}\railterm{IDENT}
       
   250 %                           (for backward compatibility)
       
   251 %
       
   252 % \rail@setcodes : guards special characters
       
   253 %
       
   254 % \rail@makeother{CHARACTER} : sets \catcode of CHARACTER to "other"
       
   255 %                              used inside a loop for \rail@setcodes
       
   256 %
       
   257 % \rail@nr : railroad diagram counter
       
   258 %
       
   259 % \ifrail@match : current \rail@i{NR}{TEXT} matches
       
   260 %
       
   261 % \rail@first : actions to be done first. read in .rao file,
       
   262 %               open .rai file if \@filesw true, undefine \rail@first.
       
   263 %               executed from \begin{rail}, \railoptions and \railterm.
       
   264 %
       
   265 % \rail@i{NR}{TEXT} : defines \rail@i@NR as TEXT. written to the .rai
       
   266 %                     file by \rail, read from the .rao file by
       
   267 %                     \rail@first
       
   268 %
       
   269 % \rail@t{IDENT} : tells Rail that IDENT is to be custom formatted,
       
   270 %                  written to the .rai file by \railterm.
       
   271 %
       
   272 % \rail@o{NR}{TEXT} : defines \rail@o@NR as TEXT, read from the .rao
       
   273 %                     file by \rail@first.
       
   274 %
       
   275 % \rail@p{OPTIONS} : pass options to rail, written to the .rai file by
       
   276 %                    \railoptions
       
   277 %
       
   278 % \rail@write{TEXT} : write TEXT to the .rai file
       
   279 %
       
   280 % \rail@warn : warn user for mismatching diagrams
       
   281 %
       
   282 % \rail@endwarn : either \relax or \rail@warn
       
   283 %
       
   284 % \ifrail@all : checked at the end of the document
       
   285 
       
   286 \def\rail@makeother#1{
       
   287   \expandafter\catcode\expandafter`\csname\string #1\endcsname=12
       
   288 }
       
   289 
       
   290 \def\rail@setcodes{
       
   291 \let\par=\relax
       
   292 \let\\=\relax
       
   293 \expandafter\@tfor\expandafter\rail@symbol\expandafter:\expandafter=%
       
   294   \the\rail@reserved
       
   295 \do{\expandafter\rail@makeother\rail@symbol}
       
   296 }
       
   297 
       
   298 \newcount\rail@nr
       
   299 
       
   300 \newif\ifrail@all
       
   301 \rail@alltrue
       
   302 
       
   303 \newif\ifrail@match
       
   304 
       
   305 \def\rail@first{
       
   306 \begingroup
       
   307 \makeatletter
       
   308 \rail@setcodes
       
   309 \InputIfFileExists{\jobname.rao}{}{\PackageInfo{rail}{No file \jobname.rao}}
       
   310 \makeatother
       
   311 \endgroup
       
   312 \if@filesw
       
   313 \newwrite\tf@rai
       
   314 \immediate\openout\tf@rai=\jobname.rai
       
   315 \fi
       
   316 \global\let\rail@first=\relax
       
   317 }
       
   318 
       
   319 \long\def\rail@body#1\end{
       
   320 {
       
   321 \newlinechar=`^^J
       
   322 \def\par{\string\par^^J}
       
   323 \rail@write{\string\rail@i{\number\rail@nr}{#1}}
       
   324 }
       
   325 \xdef\rail@i@{#1}
       
   326 \end
       
   327 }
       
   328 
       
   329 \newenvironment{rail}{
       
   330 \global\advance\rail@nr by 1
       
   331 \rail@first
       
   332 \begingroup
       
   333 \rail@setcodes
       
   334 \rail@body
       
   335 }{
       
   336 \endgroup
       
   337 \rail@matchtrue
       
   338 \@ifundefined{rail@o@\number\rail@nr}{\rail@matchfalse}{}
       
   339 \expandafter\ifx\csname rail@i@\number\rail@nr\endcsname\rail@i@
       
   340 \else
       
   341 \rail@matchfalse
       
   342 \fi
       
   343 \ifrail@match
       
   344 \csname rail@o@\number\rail@nr\endcsname
       
   345 \else
       
   346 \PackageWarning{rail}{Railroad diagram {\number\rail@nr} doesn't match}
       
   347 \global\let\rail@endwarn=\rail@warn
       
   348 \begin{list}{}{\rail@param}
       
   349 \rail@begin{1}{}
       
   350 \rail@setbox{\bfseries ???}
       
   351 \rail@oval
       
   352 \rail@end
       
   353 \end{list}
       
   354 \fi
       
   355 }
       
   356 
       
   357 \newcommand\railoptions[1]{
       
   358 \rail@first
       
   359 \rail@write{\string\rail@p{#1}}
       
   360 }
       
   361 
       
   362 \newcommand\railterm[1]{
       
   363 \rail@first
       
   364 \@for\rail@@:=#1\do{
       
   365 \rail@write{\string\rail@t{\rail@@}}
       
   366 }
       
   367 }
       
   368 
       
   369 \newcommand\railalias[2]{
       
   370 \expandafter\def\csname rail@t@#1\endcsname{#2}
       
   371 }
       
   372 
       
   373 \newcommand\railtoken[2]{\railalias{#1}{#2}\railterm{#1}}
       
   374 
       
   375 \long\def\rail@i#1#2{
       
   376 \expandafter\gdef\csname rail@i@#1\endcsname{#2}
       
   377 }
       
   378 
       
   379 \def\rail@o#1#2{
       
   380 \expandafter\gdef\csname rail@o@#1\endcsname{
       
   381 \begin{list}{}{\rail@param}
       
   382 #2
       
   383 \end{list}
       
   384 }
       
   385 }
       
   386 
       
   387 \def\rail@t#1{}
       
   388 
       
   389 \def\rail@p#1{}
       
   390 
       
   391 \long\def\rail@write#1{\@ifundefined{tf@rai}{}{\immediate\write\tf@rai{#1}}}
       
   392 
       
   393 \def\rail@warn{
       
   394 \PackageWarningNoLine{rail}{Railroad diagram(s) may have changed.
       
   395                             Use 'rail' and rerun}
       
   396 }
       
   397 
       
   398 \let\rail@endwarn=\relax
       
   399 
       
   400 \AtEndDocument{\rail@endwarn}
       
   401 
       
   402 % index entry macro
       
   403 %
       
   404 % \rail@index{IDENT} : add index entry for IDENT
       
   405 
       
   406 \def\rail@index#1{
       
   407 \index{\rail@indexfont#1}
       
   408 }
       
   409 
       
   410 % railroad formatting primitives
       
   411 %
       
   412 % \rail@x : current x
       
   413 % \rail@y : current y
       
   414 % \rail@ex : current end x
       
   415 % \rail@sx : starting x for \rail@cr
       
   416 % \rail@rx : rightmost previous x for \rail@cr
       
   417 %
       
   418 % \rail@tmpa : temporary count
       
   419 % \rail@tmpb : temporary count
       
   420 % \rail@tmpc : temporary count
       
   421 %
       
   422 % \rail@put : put at (\rail@x,\rail@y)
       
   423 % \rail@vput : put vector at (\rail@x,\rail@y)
       
   424 %
       
   425 % \rail@eline : end line by drawing from \rail@ex to \rail@x
       
   426 %
       
   427 % \rail@vreline : end line by drawing a vector from \rail@x to \rail@ex
       
   428 %
       
   429 % \rail@vleline : end line by drawing a vector from \rail@ex to \rail@x
       
   430 %
       
   431 % \rail@sety{LEVEL} : set \rail@y to level LEVEL
       
   432 
       
   433 \newcount\rail@x
       
   434 \newcount\rail@y
       
   435 \newcount\rail@ex
       
   436 \newcount\rail@sx
       
   437 \newcount\rail@rx
       
   438 
       
   439 \newcount\rail@tmpa
       
   440 \newcount\rail@tmpb
       
   441 \newcount\rail@tmpc
       
   442 
       
   443 \def\rail@put{\put(\number\rail@x,\number\rail@y)}
       
   444 
       
   445 \def\rail@vput{\put(\number\rail@ex,\number\rail@y)}
       
   446 
       
   447 \def\rail@eline{
       
   448 \rail@tmpb=\rail@x
       
   449 \advance\rail@tmpb by -\rail@ex
       
   450 \rail@put{\line(-1,0){\number\rail@tmpb}}
       
   451 }
       
   452 
       
   453 \def\rail@vreline{
       
   454 \rail@tmpb=\rail@x
       
   455 \advance\rail@tmpb by -\rail@ex
       
   456 \rail@vput{\vector(1,0){\number\rail@tmpb}}
       
   457 }
       
   458 
       
   459 \def\rail@vleline{
       
   460 \rail@tmpb=\rail@x
       
   461 \advance\rail@tmpb by -\rail@ex
       
   462 \rail@put{\vector(-1,0){\number\rail@tmpb}}
       
   463 }
       
   464 
       
   465 \def\rail@sety#1{
       
   466 \rail@y=#1
       
   467 \multiply\rail@y by -\rail@boxsp
       
   468 \advance\rail@y by -\rail@boxht
       
   469 }
       
   470 
       
   471 % \rail@begin{HEIGHT}{NAME} : begin a railroad diagram of height HEIGHT
       
   472 %
       
   473 % \rail@end : end a railroad diagram
       
   474 %
       
   475 % \rail@expand{IDENT} : expand IDENT
       
   476 
       
   477 \def\rail@begin#1#2{
       
   478 \item
       
   479 \begin{minipage}[t]{\linewidth}
       
   480 \ifx\@empty#2\else
       
   481 {\rail@namefont \rail@expand{#2}}\\*[\railnamesep]
       
   482 \fi
       
   483 \unitlength=\railunit
       
   484 \rail@tmpa=#1
       
   485 \multiply\rail@tmpa by \rail@boxsp
       
   486 \begin{picture}(0,\number\rail@tmpa)(0,-\number\rail@tmpa)
       
   487 \rail@ex=0
       
   488 \rail@rx=0
       
   489 \rail@x=\rail@extra
       
   490 \rail@sx=\rail@x
       
   491 \rail@sety{0}
       
   492 }
       
   493 
       
   494 \def\rail@end{
       
   495 \advance\rail@x by \rail@extra
       
   496 \rail@eline
       
   497 \end{picture}
       
   498 \end{minipage}
       
   499 }
       
   500 
       
   501 \def\rail@vend{
       
   502 \advance\rail@x by \rail@extra
       
   503 \rail@vreline
       
   504 \end{picture}
       
   505 \end{minipage}
       
   506 }
       
   507 
       
   508 \def\rail@expand#1{\@ifundefined{rail@t@#1}{#1}{\csname rail@t@#1\endcsname}}
       
   509 
       
   510 % \rail@token{TEXT}[ANNOT] : format token TEXT with annotation
       
   511 % \rail@ltoken{TEXT}[ANNOT] : format token TEXT with annotation, arrow left
       
   512 % \rail@rtoken{TEXT}[ANNOT] : format token TEXT with annotation, arrow right
       
   513 %
       
   514 % \rail@ctoken{TEXT}[ANNOT] : format token TEXT centered with annotation
       
   515 % \rail@lctoken{TEXT}[ANNOT] : format token TEXT centered with annotation, arrow left
       
   516 % \rail@rctoken{TEXT}[ANNOT] : format token TEXT centered with annotation, arrow right
       
   517 %
       
   518 % \rail@nont{TEXT}[ANNOT] : format nonterminal TEXT with annotation
       
   519 % \rail@lnont{TEXT}[ANNOT] : format nonterminal TEXT with annotation, arrow left
       
   520 % \rail@rnont{TEXT}[ANNOT] : format nonterminal TEXT with annotation. arrow right
       
   521 %
       
   522 % \rail@cnont{TEXT}[ANNOT] : format nonterminal TEXT centered with annotation
       
   523 % \rail@lcnont{TEXT}[ANNOT] : format nonterminal TEXT centered with annotation,
       
   524 %                             arrow left
       
   525 % \rail@rcnont{TEXT}[ANNOT] : format nonterminal TEXT centered with annotation,
       
   526 %                             arrow right
       
   527 %
       
   528 % \rail@term{TEXT}[ANNOT] : format terminal TEXT with annotation
       
   529 % \rail@lterm{TEXT}[ANNOT] : format terminal TEXT with annotation, arrow left
       
   530 % \rail@rterm{TEXT}[ANNOT] : format terminal TEXT with annotation, arrow right
       
   531 %
       
   532 % \rail@cterm{TEXT}[ANNOT] : format terminal TEXT centered with annotation
       
   533 % \rail@lcterm{TEXT}[ANNOT] : format terminal TEXT centered with annotation, arrow left
       
   534 % \rail@rcterm{TEXT}[ANNOT] : format terminal TEXT centered with annotation,
       
   535 %                             arrow right
       
   536 %
       
   537 % \rail@annote[TEXT] : format TEXT as annotation
       
   538 
       
   539 \def\rail@token#1[#2]{
       
   540 \rail@setbox{%
       
   541 {\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
       
   542 }
       
   543 \rail@oval
       
   544 }
       
   545 
       
   546 \def\rail@ltoken#1[#2]{
       
   547 \rail@setbox{%
       
   548 {\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
       
   549 }
       
   550 \rail@vloval
       
   551 }
       
   552 
       
   553 \def\rail@rtoken#1[#2]{
       
   554 \rail@setbox{%
       
   555 {\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
       
   556 }
       
   557 \rail@vroval
       
   558 }
       
   559 
       
   560 \def\rail@ctoken#1[#2]{
       
   561 \rail@setbox{%
       
   562 {\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
       
   563 }
       
   564 \rail@coval
       
   565 }
       
   566 
       
   567 \def\rail@lctoken#1[#2]{
       
   568 \rail@setbox{%
       
   569 {\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
       
   570 }
       
   571 \rail@vlcoval
       
   572 }
       
   573 
       
   574 \def\rail@rctoken#1[#2]{
       
   575 \rail@setbox{%
       
   576 {\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
       
   577 }
       
   578 \rail@vrcoval
       
   579 }
       
   580 
       
   581 \def\rail@nont#1[#2]{
       
   582 \rail@setbox{%
       
   583 {\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
       
   584 }
       
   585 \rail@frame
       
   586 }
       
   587 
       
   588 \def\rail@lnont#1[#2]{
       
   589 \rail@setbox{%
       
   590 {\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
       
   591 }
       
   592 \rail@vlframe
       
   593 }
       
   594 
       
   595 \def\rail@rnont#1[#2]{
       
   596 \rail@setbox{%
       
   597 {\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
       
   598 }
       
   599 \rail@vrframe
       
   600 }
       
   601 
       
   602 \def\rail@cnont#1[#2]{
       
   603 \rail@setbox{%
       
   604 {\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
       
   605 }
       
   606 \rail@cframe
       
   607 }
       
   608 
       
   609 \def\rail@lcnont#1[#2]{
       
   610 \rail@setbox{%
       
   611 {\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
       
   612 }
       
   613 \rail@vlcframe
       
   614 }
       
   615 
       
   616 \def\rail@rcnont#1[#2]{
       
   617 \rail@setbox{%
       
   618 {\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
       
   619 }
       
   620 \rail@vrcframe
       
   621 }
       
   622 
       
   623 \def\rail@term#1[#2]{
       
   624 \rail@setbox{%
       
   625 {\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
       
   626 }
       
   627 \rail@oval
       
   628 }
       
   629 
       
   630 \def\rail@lterm#1[#2]{
       
   631 \rail@setbox{%
       
   632 {\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
       
   633 }
       
   634 \rail@vloval
       
   635 }
       
   636 
       
   637 \def\rail@rterm#1[#2]{
       
   638 \rail@setbox{%
       
   639 {\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
       
   640 }
       
   641 \rail@vroval
       
   642 }
       
   643 
       
   644 \def\rail@cterm#1[#2]{
       
   645 \rail@setbox{%
       
   646 {\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
       
   647 }
       
   648 \rail@coval
       
   649 }
       
   650 
       
   651 \def\rail@lcterm#1[#2]{
       
   652 \rail@setbox{%
       
   653 {\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
       
   654 }
       
   655 \rail@vlcoval
       
   656 }
       
   657 
       
   658 \def\rail@rcterm#1[#2]{
       
   659 \rail@setbox{%
       
   660 {\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
       
   661 }
       
   662 \rail@vrcoval
       
   663 }
       
   664 
       
   665 \def\rail@annote[#1]{
       
   666 \rail@setbox{\rail@annofont #1}
       
   667 \rail@text
       
   668 }
       
   669 
       
   670 % \rail@box : temporary box for \rail@oval and \rail@frame
       
   671 %
       
   672 % \rail@setbox{TEXT} : set \rail@box to TEXT, set \rail@tmpa to width
       
   673 %
       
   674 % \rail@oval : format \rail@box of width \rail@tmpa inside an oval
       
   675 % \rail@vloval : format \rail@box of width \rail@tmpa inside an oval, vector left
       
   676 % \rail@vroval : format \rail@box of width \rail@tmpa inside an oval, vector right
       
   677 %
       
   678 % \rail@coval : same as \rail@oval, but centered between \rail@x and
       
   679 %               \rail@mx
       
   680 % \rail@vlcoval : same as \rail@oval, but centered between \rail@x and
       
   681 %                 \rail@mx, vector left
       
   682 % \rail@vrcoval : same as \rail@oval, but centered between \rail@x and
       
   683 %                 \rail@mx, vector right
       
   684 %
       
   685 % \rail@frame : format \rail@box of width \rail@tmpa inside a frame
       
   686 % \rail@vlframe : format \rail@box of width \rail@tmpa inside a frame, vector left
       
   687 % \rail@vrframe : format \rail@box of width \rail@tmpa inside a frame, vector right
       
   688 %
       
   689 % \rail@cframe : same as \rail@frame, but centered between \rail@x and
       
   690 %                \rail@mx
       
   691 % \rail@vlcframe : same as \rail@frame, but centered between \rail@x and
       
   692 %                  \rail@mx, vector left
       
   693 % \rail@vrcframe : same as \rail@frame, but centered between \rail@x and
       
   694 %                  \rail@mx, vector right
       
   695 %
       
   696 % \rail@text : format \rail@box of width \rail@tmpa above the line
       
   697 
       
   698 \newbox\rail@box
       
   699 
       
   700 \def\rail@setbox#1{
       
   701 \setbox\rail@box\hbox{\strut#1}
       
   702 \rail@tmpa=\wd\rail@box
       
   703 \divide\rail@tmpa by \railunit
       
   704 }
       
   705 
       
   706 \def\rail@oval{
       
   707 \advance\rail@x by \rail@boxlf
       
   708 \rail@eline
       
   709 \advance\rail@tmpa by \rail@ovalsp
       
   710 \ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi
       
   711 \rail@tmpb=\rail@tmpa
       
   712 \divide\rail@tmpb by 2
       
   713 \advance\rail@y by -\rail@boxhht
       
   714 \rail@put{\makebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}}
       
   715 \advance\rail@y by \rail@boxhht
       
   716 \advance\rail@x by \rail@tmpb
       
   717 \rail@put{\oval(\number\rail@tmpa,\number\rail@boxht)}
       
   718 \advance\rail@x by \rail@tmpb
       
   719 \rail@ex=\rail@x
       
   720 \advance\rail@x by \rail@boxrt
       
   721 }
       
   722 
       
   723 \def\rail@vloval{
       
   724 \advance\rail@x by \rail@boxlf
       
   725 \rail@eline
       
   726 \advance\rail@tmpa by \rail@ovalsp
       
   727 \ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi
       
   728 \rail@tmpb=\rail@tmpa
       
   729 \divide\rail@tmpb by 2
       
   730 \advance\rail@y by -\rail@boxhht
       
   731 \rail@put{\makebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}}
       
   732 \advance\rail@y by \rail@boxhht
       
   733 \advance\rail@x by \rail@tmpb
       
   734 \rail@put{\oval(\number\rail@tmpa,\number\rail@boxht)}
       
   735 \advance\rail@x by \rail@tmpb
       
   736 \rail@ex=\rail@x
       
   737 \advance\rail@x by \rail@boxrt
       
   738 \rail@vleline
       
   739 }
       
   740 
       
   741 \def\rail@vroval{
       
   742 \advance\rail@x by \rail@boxlf
       
   743 \rail@vreline
       
   744 \advance\rail@tmpa by \rail@ovalsp
       
   745 \ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi
       
   746 \rail@tmpb=\rail@tmpa
       
   747 \divide\rail@tmpb by 2
       
   748 \advance\rail@y by -\rail@boxhht
       
   749 \rail@put{\makebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}}
       
   750 \advance\rail@y by \rail@boxhht
       
   751 \advance\rail@x by \rail@tmpb
       
   752 \rail@put{\oval(\number\rail@tmpa,\number\rail@boxht)}
       
   753 \advance\rail@x by \rail@tmpb
       
   754 \rail@ex=\rail@x
       
   755 \advance\rail@x by \rail@boxrt
       
   756 }
       
   757 
       
   758 \def\rail@coval{
       
   759 \rail@tmpb=\rail@tmpa
       
   760 \advance\rail@tmpb by \rail@ovalsp
       
   761 \ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi
       
   762 \advance\rail@tmpb by \rail@boxlf
       
   763 \advance\rail@tmpb by \rail@boxrt
       
   764 \rail@tmpc=\rail@mx
       
   765 \advance\rail@tmpc by -\rail@x
       
   766 \advance\rail@tmpc by -\rail@tmpb
       
   767 \divide\rail@tmpc by 2
       
   768 \ifnum\rail@tmpc>0
       
   769 \advance\rail@x by \rail@tmpc
       
   770 \fi
       
   771 \rail@oval
       
   772 }
       
   773 
       
   774 \def\rail@vlcoval{
       
   775 \rail@tmpb=\rail@tmpa
       
   776 \advance\rail@tmpb by \rail@ovalsp
       
   777 \ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi
       
   778 \advance\rail@tmpb by \rail@boxlf
       
   779 \advance\rail@tmpb by \rail@boxrt
       
   780 \rail@tmpc=\rail@mx
       
   781 \advance\rail@tmpc by -\rail@x
       
   782 \advance\rail@tmpc by -\rail@tmpb
       
   783 \divide\rail@tmpc by 2
       
   784 \ifnum\rail@tmpc>0
       
   785 \advance\rail@x by \rail@tmpc
       
   786 \fi
       
   787 \rail@vloval
       
   788 }
       
   789 
       
   790 \def\rail@vrcoval{
       
   791 \rail@tmpb=\rail@tmpa
       
   792 \advance\rail@tmpb by \rail@ovalsp
       
   793 \ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi
       
   794 \advance\rail@tmpb by \rail@boxlf
       
   795 \advance\rail@tmpb by \rail@boxrt
       
   796 \rail@tmpc=\rail@mx
       
   797 \advance\rail@tmpc by -\rail@x
       
   798 \advance\rail@tmpc by -\rail@tmpb
       
   799 \divide\rail@tmpc by 2
       
   800 \ifnum\rail@tmpc>0
       
   801 \advance\rail@x by \rail@tmpc
       
   802 \fi
       
   803 \rail@vroval
       
   804 }
       
   805 
       
   806 \def\rail@frame{
       
   807 \advance\rail@x by \rail@boxlf
       
   808 \rail@eline
       
   809 \advance\rail@tmpa by \rail@framesp
       
   810 \ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi
       
   811 \advance\rail@y by -\rail@boxhht
       
   812 \rail@put{\framebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}}
       
   813 \advance\rail@y by \rail@boxhht
       
   814 \advance\rail@x by \rail@tmpa
       
   815 \rail@ex=\rail@x
       
   816 \advance\rail@x by \rail@boxrt
       
   817 }
       
   818 
       
   819 \def\rail@vlframe{
       
   820 \advance\rail@x by \rail@boxlf
       
   821 \rail@eline
       
   822 \advance\rail@tmpa by \rail@framesp
       
   823 \ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi
       
   824 \advance\rail@y by -\rail@boxhht
       
   825 \rail@put{\framebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}}
       
   826 \advance\rail@y by \rail@boxhht
       
   827 \advance\rail@x by \rail@tmpa
       
   828 \rail@ex=\rail@x
       
   829 \advance\rail@x by \rail@boxrt
       
   830 \rail@vleline
       
   831 }
       
   832 
       
   833 \def\rail@vrframe{
       
   834 \advance\rail@x by \rail@boxlf
       
   835 \rail@vreline
       
   836 \advance\rail@tmpa by \rail@framesp
       
   837 \ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi
       
   838 \advance\rail@y by -\rail@boxhht
       
   839 \rail@put{\framebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}}
       
   840 \advance\rail@y by \rail@boxhht
       
   841 \advance\rail@x by \rail@tmpa
       
   842 \rail@ex=\rail@x
       
   843 \advance\rail@x by \rail@boxrt
       
   844 }
       
   845 
       
   846 \def\rail@cframe{
       
   847 \rail@tmpb=\rail@tmpa
       
   848 \advance\rail@tmpb by \rail@framesp
       
   849 \ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi
       
   850 \advance\rail@tmpb by \rail@boxlf
       
   851 \advance\rail@tmpb by \rail@boxrt
       
   852 \rail@tmpc=\rail@mx
       
   853 \advance\rail@tmpc by -\rail@x
       
   854 \advance\rail@tmpc by -\rail@tmpb
       
   855 \divide\rail@tmpc by 2
       
   856 \ifnum\rail@tmpc>0
       
   857 \advance\rail@x by \rail@tmpc
       
   858 \fi
       
   859 \rail@frame
       
   860 }
       
   861 
       
   862 \def\rail@vlcframe{
       
   863 \rail@tmpb=\rail@tmpa
       
   864 \advance\rail@tmpb by \rail@framesp
       
   865 \ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi
       
   866 \advance\rail@tmpb by \rail@boxlf
       
   867 \advance\rail@tmpb by \rail@boxrt
       
   868 \rail@tmpc=\rail@mx
       
   869 \advance\rail@tmpc by -\rail@x
       
   870 \advance\rail@tmpc by -\rail@tmpb
       
   871 \divide\rail@tmpc by 2
       
   872 \ifnum\rail@tmpc>0
       
   873 \advance\rail@x by \rail@tmpc
       
   874 \fi
       
   875 \rail@vlframe
       
   876 }
       
   877 
       
   878 \def\rail@vrcframe{
       
   879 \rail@tmpb=\rail@tmpa
       
   880 \advance\rail@tmpb by \rail@framesp
       
   881 \ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi
       
   882 \advance\rail@tmpb by \rail@boxlf
       
   883 \advance\rail@tmpb by \rail@boxrt
       
   884 \rail@tmpc=\rail@mx
       
   885 \advance\rail@tmpc by -\rail@x
       
   886 \advance\rail@tmpc by -\rail@tmpb
       
   887 \divide\rail@tmpc by 2
       
   888 \ifnum\rail@tmpc>0
       
   889 \advance\rail@x by \rail@tmpc
       
   890 \fi
       
   891 \rail@vrframe
       
   892 }
       
   893 
       
   894 \def\rail@text{
       
   895 \advance\rail@x by \rail@textlf
       
   896 \advance\rail@y by \rail@textup
       
   897 \rail@put{\box\rail@box}
       
   898 \advance\rail@y by -\rail@textup
       
   899 \advance\rail@x by \rail@tmpa
       
   900 \advance\rail@x by \rail@textrt
       
   901 }
       
   902 
       
   903 % alternatives
       
   904 %
       
   905 % \rail@jx \rail@jy : current join point
       
   906 %
       
   907 % \rail@gx \rail@gy \rail@gex \rail@grx : global versions of \rail@x etc,
       
   908 %                                         to pass values over group closings
       
   909 %
       
   910 % \rail@mx : maximum x so far
       
   911 %
       
   912 % \rail@sy : starting \rail@y for alternatives
       
   913 %
       
   914 % \rail@jput : put at (\rail@jx,\rail@jy)
       
   915 %
       
   916 % \rail@joval[PART] : put \oval[PART] with adjust
       
   917 
       
   918 \newcount\rail@jx
       
   919 \newcount\rail@jy
       
   920 
       
   921 \newcount\rail@gx
       
   922 \newcount\rail@gy
       
   923 \newcount\rail@gex
       
   924 \newcount\rail@grx
       
   925 
       
   926 \newcount\rail@sy
       
   927 \newcount\rail@mx
       
   928 
       
   929 \def\rail@jput{
       
   930 \put(\number\rail@jx,\number\rail@jy)
       
   931 }
       
   932 
       
   933 \def\rail@joval[#1]{
       
   934 \advance\rail@jx by \rail@joinadj
       
   935 \rail@jput{\oval(\number\rail@joinsz,\number\rail@joinsz)[#1]}
       
   936 \advance\rail@jx by -\rail@joinadj
       
   937 }
       
   938 
       
   939 % \rail@barsplit : incoming split for '|'
       
   940 %
       
   941 % \rail@plussplit : incoming split for '+'
       
   942 %
       
   943 
       
   944 \def\rail@barsplit{
       
   945 \advance\rail@jy by -\rail@joinhsz
       
   946 \rail@joval[tr]
       
   947 \advance\rail@jx by \rail@joinhsz
       
   948 }
       
   949 
       
   950 \def\rail@plussplit{
       
   951 \advance\rail@jy by -\rail@joinhsz
       
   952 \advance\rail@jx by \rail@joinsz
       
   953 \rail@joval[tl]
       
   954 \advance\rail@jx by -\rail@joinhsz
       
   955 }
       
   956 
       
   957 % \rail@alt{SPLIT} : start alternatives with incoming split SPLIT
       
   958 %
       
   959 
       
   960 \def\rail@alt#1{
       
   961 \rail@sy=\rail@y
       
   962 \rail@jx=\rail@x
       
   963 \rail@jy=\rail@y
       
   964 \advance\rail@x by \rail@joinsz
       
   965 \rail@mx=0
       
   966 \let\rail@list=\@empty
       
   967 \let\rail@comma=\@empty
       
   968 \let\rail@split=#1
       
   969 \begingroup
       
   970 \rail@sx=\rail@x
       
   971 \rail@rx=0
       
   972 }
       
   973 
       
   974 % \rail@nextalt{FIX}{Y} : start next alternative at vertical position Y
       
   975 %                         and fix-up FIX
       
   976 %
       
   977 
       
   978 \def\rail@nextalt#1#2{
       
   979 \global\rail@gx=\rail@x
       
   980 \global\rail@gy=\rail@y
       
   981 \global\rail@gex=\rail@ex
       
   982 \global\rail@grx=\rail@rx
       
   983 \endgroup
       
   984 #1
       
   985 \ifnum\rail@gx>\rail@mx\rail@mx=\rail@gx\fi
       
   986 \ifnum\rail@grx>\rail@mx\rail@mx=\rail@grx\fi
       
   987 \edef\rail@list{\rail@list\rail@comma\number\rail@gex:\number\rail@gy}
       
   988 \def\rail@comma{,}
       
   989 \rail@split
       
   990 \let\rail@split=\@empty
       
   991 \rail@sety{#2}
       
   992 \rail@tmpa=\rail@jy
       
   993 \advance\rail@tmpa by -\rail@y
       
   994 \advance\rail@tmpa by -\rail@joinhsz
       
   995 \rail@jput{\line(0,-1){\number\rail@tmpa}}
       
   996 \rail@jy=\rail@y
       
   997 \advance\rail@jy by \rail@joinhsz
       
   998 \advance\rail@jx by \rail@joinhsz
       
   999 \rail@joval[bl]
       
  1000 \advance\rail@jx by -\rail@joinhsz
       
  1001 \rail@ex=\rail@x
       
  1002 \begingroup
       
  1003 \rail@sx=\rail@x
       
  1004 \rail@rx=0
       
  1005 }
       
  1006 
       
  1007 % \rail@barjoin : outgoing join for first '|' alternative
       
  1008 %
       
  1009 % \rail@plusjoin : outgoing join for first '+' alternative
       
  1010 %
       
  1011 % \rail@altjoin : join for subsequent alternative
       
  1012 %
       
  1013 
       
  1014 \def\rail@barjoin{
       
  1015 \ifnum\rail@y<\rail@sy
       
  1016 \global\rail@gex=\rail@jx
       
  1017 \else
       
  1018 \global\rail@gex=\rail@ex
       
  1019 \fi
       
  1020 \advance\rail@jy by -\rail@joinhsz
       
  1021 \rail@joval[tl]
       
  1022 \advance\rail@jx by -\rail@joinhsz
       
  1023 \ifnum\rail@y<\rail@sy
       
  1024 \rail@altjoin
       
  1025 \fi
       
  1026 }
       
  1027 
       
  1028 \def\rail@plusjoin{
       
  1029 \global\rail@gex=\rail@ex
       
  1030 \advance\rail@jy by -\rail@joinhsz
       
  1031 \advance\rail@jx by -\rail@joinsz
       
  1032 \rail@joval[tr]
       
  1033 \advance\rail@jx by \rail@joinhsz
       
  1034 }
       
  1035 
       
  1036 \def\rail@altjoin{
       
  1037 \rail@eline
       
  1038 \rail@tmpa=\rail@jy
       
  1039 \advance\rail@tmpa by -\rail@y
       
  1040 \advance\rail@tmpa by -\rail@joinhsz
       
  1041 \rail@jput{\line(0,-1){\number\rail@tmpa}}
       
  1042 \rail@jy=\rail@y
       
  1043 \advance\rail@jy by \rail@joinhsz
       
  1044 \advance\rail@jx by -\rail@joinhsz
       
  1045 \rail@joval[br]
       
  1046 \advance\rail@jx by \rail@joinhsz
       
  1047 }
       
  1048 
       
  1049 % \rail@eltsplit EX:Y; : split EX:Y into \rail@ex \rail@y
       
  1050 %
       
  1051 % \rail@endalt{JOIN} : end alternatives with outgoing join JOIN
       
  1052 
       
  1053 \def\rail@eltsplit#1:#2;{\rail@ex=#1\rail@y=#2}
       
  1054 
       
  1055 \def\rail@endalt#1{
       
  1056 \global\rail@gx=\rail@x
       
  1057 \global\rail@gy=\rail@y
       
  1058 \global\rail@gex=\rail@ex
       
  1059 \global\rail@grx=\rail@rx
       
  1060 \endgroup
       
  1061 \ifnum\rail@gx>\rail@mx\rail@mx=\rail@gx\fi
       
  1062 \ifnum\rail@grx>\rail@mx\rail@mx=\rail@grx\fi
       
  1063 \edef\rail@list{\rail@list\rail@comma\number\rail@gex:\number\rail@gy}
       
  1064 \rail@x=\rail@mx
       
  1065 \rail@jx=\rail@x
       
  1066 \rail@jy=\rail@sy
       
  1067 \advance\rail@jx by \rail@joinsz
       
  1068 \let\rail@join=#1
       
  1069 \@for\rail@elt:=\rail@list\do{
       
  1070 \expandafter\rail@eltsplit\rail@elt;
       
  1071 \rail@join
       
  1072 \let\rail@join=\rail@altjoin
       
  1073 }
       
  1074 \rail@x=\rail@mx
       
  1075 \rail@y=\rail@sy
       
  1076 \rail@ex=\rail@gex
       
  1077 \advance\rail@x by \rail@joinsz
       
  1078 }
       
  1079 
       
  1080 % \rail@bar : start '|' alternatives
       
  1081 %
       
  1082 % \rail@nextbar : next '|' alternative
       
  1083 %
       
  1084 % \rail@endbar : end '|' alternatives
       
  1085 %
       
  1086 
       
  1087 \def\rail@bar{
       
  1088 \rail@alt\rail@barsplit
       
  1089 }
       
  1090 
       
  1091 \def\rail@nextbar{
       
  1092 \rail@nextalt\relax
       
  1093 }
       
  1094 
       
  1095 \def\rail@endbar{
       
  1096 \rail@endalt\rail@barjoin
       
  1097 }
       
  1098 
       
  1099 % \rail@plus : start '+' alternatives
       
  1100 %
       
  1101 % \rail@nextplus: next '+' alternative
       
  1102 %
       
  1103 % \rail@endplus : end '+' alternatives
       
  1104 %
       
  1105 
       
  1106 \def\rail@plus{
       
  1107 \rail@alt\rail@plussplit
       
  1108 }
       
  1109 
       
  1110 \def\rail@nextplus{
       
  1111 \rail@nextalt\rail@fixplus
       
  1112 }
       
  1113 
       
  1114 \def\rail@fixplus{
       
  1115 \ifnum\rail@gy<\rail@sy
       
  1116 \begingroup
       
  1117 \rail@x=\rail@gx
       
  1118 \rail@y=\rail@gy
       
  1119 \rail@ex=\rail@gex
       
  1120 \rail@rx=\rail@grx
       
  1121 \ifnum\rail@x<\rail@rx
       
  1122 \rail@x=\rail@rx
       
  1123 \fi
       
  1124 \rail@eline
       
  1125 \rail@jx=\rail@x
       
  1126 \rail@jy=\rail@y
       
  1127 \advance\rail@jy by \rail@joinhsz
       
  1128 \rail@joval[br]
       
  1129 \advance\rail@jx by \rail@joinhsz
       
  1130 \rail@tmpa=\rail@sy
       
  1131 \advance\rail@tmpa by -\rail@joinhsz
       
  1132 \advance\rail@tmpa by -\rail@jy
       
  1133 \rail@jput{\line(0,1){\number\rail@tmpa}}
       
  1134 \rail@jy=\rail@sy
       
  1135 \advance\rail@jy by -\rail@joinhsz
       
  1136 \advance\rail@jx by \rail@joinhsz
       
  1137 \rail@joval[tl]
       
  1138 \advance\rail@jy by \rail@joinhsz
       
  1139 \global\rail@gx=\rail@jx
       
  1140 \global\rail@gy=\rail@jy
       
  1141 \global\rail@gex=\rail@gx
       
  1142 \global\rail@grx=\rail@rx
       
  1143 \endgroup
       
  1144 \fi
       
  1145 }
       
  1146 
       
  1147 \def\rail@endplus{
       
  1148 \rail@endalt\rail@plusjoin
       
  1149 }
       
  1150 
       
  1151 % \rail@cr{Y} : carriage return to vertical position Y
       
  1152 
       
  1153 \def\rail@cr#1{
       
  1154 \rail@tmpa=\rail@sx
       
  1155 \advance\rail@tmpa by \rail@joinsz
       
  1156 \ifnum\rail@x<\rail@tmpa\rail@x=\rail@tmpa\fi
       
  1157 \rail@eline
       
  1158 \rail@jx=\rail@x
       
  1159 \rail@jy=\rail@y
       
  1160 \advance\rail@x by \rail@joinsz
       
  1161 \ifnum\rail@x>\rail@rx\rail@rx=\rail@x\fi
       
  1162 \advance\rail@jy by -\rail@joinhsz
       
  1163 \rail@joval[tr]
       
  1164 \advance\rail@jx by \rail@joinhsz
       
  1165 \rail@sety{#1}
       
  1166 \rail@tmpa=\rail@jy
       
  1167 \advance\rail@tmpa by -\rail@y
       
  1168 \advance\rail@tmpa by -\rail@boxsp
       
  1169 \advance\rail@tmpa by -\rail@joinhsz
       
  1170 \rail@jput{\line(0,-1){\number\rail@tmpa}}
       
  1171 \rail@jy=\rail@y
       
  1172 \advance\rail@jy by \rail@boxsp
       
  1173 \advance\rail@jy by \rail@joinhsz
       
  1174 \advance\rail@jx by -\rail@joinhsz
       
  1175 \rail@joval[br]
       
  1176 \advance\rail@jy by -\rail@joinhsz
       
  1177 \rail@tmpa=\rail@jx
       
  1178 \advance\rail@tmpa by -\rail@sx
       
  1179 \advance\rail@tmpa by -\rail@joinhsz
       
  1180 \rail@jput{\line(-1,0){\number\rail@tmpa}}
       
  1181 \rail@jx=\rail@sx
       
  1182 \advance\rail@jx by \rail@joinhsz
       
  1183 \advance\rail@jy by -\rail@joinhsz
       
  1184 \rail@joval[tl]
       
  1185 \advance\rail@jx by -\rail@joinhsz
       
  1186 \rail@tmpa=\rail@boxsp
       
  1187 \advance\rail@tmpa by -\rail@joinsz
       
  1188 \rail@jput{\line(0,-1){\number\rail@tmpa}}
       
  1189 \advance\rail@jy by -\rail@tmpa
       
  1190 \advance\rail@jx by \rail@joinhsz
       
  1191 \rail@joval[bl]
       
  1192 \rail@x=\rail@jx
       
  1193 \rail@ex=\rail@x
       
  1194 }
       
  1195 
       
  1196 % default setup for Isabelle
       
  1197 \newenvironment{railoutput}%
       
  1198 {\begin{list}{}{\rail@param}\def\rail@expand{\relax}\makeatletter}{\makeatother\end{list}}
       
  1199 
       
  1200 \def\rail@termfont{\isabellestyle{tt}}
       
  1201 \def\rail@nontfont{\isabellestyle{it}}
       
  1202 \def\rail@namefont{\isabellestyle{it}}