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}} 1203