| author | wenzelm |
| Fri, 30 Jul 1999 15:56:58 +0200 | |
| changeset 7137 | e5d18fd42430 |
| child 7170 | cb8afc731bee |
| permissions | -rw-r--r-- |
| wenzelm@7137 | 1 |
|
| wenzelm@7137 | 2 |
\railalias{lbrace}{\ttlbrace}
|
| wenzelm@7137 | 3 |
\railalias{rbrace}{\ttrbrace}
|
| wenzelm@7137 | 4 |
\railalias{llbrace}{\ttlbrace\ttlbrace}
|
| wenzelm@7137 | 5 |
\railalias{rrbrace}{\ttrbrace\ttrbrace}
|
| wenzelm@7137 | 6 |
|
| wenzelm@7137 | 7 |
\setlength\railextra{3.6ex}
|
| wenzelm@7137 | 8 |
\setlength\railboxleft{0.9ex}
|
| wenzelm@7137 | 9 |
\setlength\railboxright{0.9ex}
|
| wenzelm@7137 | 10 |
\setlength\railovalspace{1.8ex}
|
| wenzelm@7137 | 11 |
\setlength\railframespace{1.8ex}
|
| wenzelm@7137 | 12 |
\setlength\railtextleft{0.9ex}
|
| wenzelm@7137 | 13 |
\setlength\railtextright{0.9ex}
|
| wenzelm@7137 | 14 |
\setlength\railnamesep{0.9ex}
|
| wenzelm@7137 | 15 |
|
| wenzelm@7137 | 16 |
\setlength\railboxheight{16pt}
|
| wenzelm@7137 | 17 |
\setlength\railboxskip{24pt}
|
| wenzelm@7137 | 18 |
\setlength\railtextup{5pt}
|
| wenzelm@7137 | 19 |
\setlength\railjoinsize{16pt}
|
| wenzelm@7137 | 20 |
|
| wenzelm@7137 | 21 |
\def\rail@termfont{\small\ttfamily\upshape}
|
| wenzelm@7137 | 22 |
\def\rail@nontfont{\small\rmfamily\upshape}
|
| wenzelm@7137 | 23 |
\def\rail@annofont{\small\rmfamily\itshape}
|
| wenzelm@7137 | 24 |
\def\rail@namefont{\small\rmfamily\itshape}
|
| wenzelm@7137 | 25 |
\def\rail@indexfont{\small\rmfamily\itshape}
|
| wenzelm@7137 | 26 |
\newcommand{\railtoken}[1]{{\texttt{#1}}}
|
| wenzelm@7137 | 27 |
\newcommand{\railqtoken}[1]{{\textsl{#1}}}
|
| wenzelm@7137 | 28 |
\newcommand{\railnonterm}[1]{{\emph{#1}}}
|
| wenzelm@7137 | 29 |
|
| wenzelm@7137 | 30 |
\newcommand\indexoutertoken[1]{\index{#1@\railtoken{#1} (outer syntax)|bold}}
|
| wenzelm@7137 | 31 |
\newcommand\indexouternonterm[1]{\index{#1@\railnonterm{#1} (outer syntax)|bold}}
|