1.1 --- a/src/Tools/isac/Doc/ROOT Thu Apr 08 13:09:44 2021 +0200
1.2 +++ b/src/Tools/isac/Doc/ROOT Thu Apr 08 13:27:27 2021 +0200
1.3 @@ -5,10 +5,6 @@
1.4 "Interpret"
1.5 theories
1.6 "Lucas_Interpreter"
1.7 - document_files (in "../")
1.8 - "isabelle.sty"
1.9 - "isabellesym.sty"
1.10 - "pdfsetup.sty"
1.11 document_files
1.12 "bend-7-70-en.png"
1.13 "fun-pack-biegelinie-2.png"
1.14 @@ -23,10 +19,6 @@
1.15 "Specify"
1.16 theories
1.17 "Specify_Phase"
1.18 - document_files (in "../")
1.19 - "isabelle.sty"
1.20 - "isabellesym.sty"
1.21 - "pdfsetup.sty"
1.22 document_files
1.23 "root.bib"
1.24 "root.tex"
2.1 --- a/src/Tools/isac/Doc/comment.sty Thu Apr 08 13:09:44 2021 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,278 +0,0 @@
2.4 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2.5 -% Comment.sty version 3.6, October 1999
2.6 -%
2.7 -% Purpose:
2.8 -% selectively in/exclude pieces of text: the user can define new
2.9 -% comment versions, and each is controlled separately.
2.10 -% Special comments can be defined where the user specifies the
2.11 -% action that is to be taken with each comment line.
2.12 -%
2.13 -% Author
2.14 -% Victor Eijkhout
2.15 -% Department of Computer Science
2.16 -% University of Tennessee
2.17 -% 107 Ayres Hall
2.18 -% Knoxville TN 37996
2.19 -% USA
2.20 -%
2.21 -% victor@eijkhout.net
2.22 -%
2.23 -% This program is free software; you can redistribute it and/or
2.24 -% modify it under the terms of the GNU General Public License
2.25 -% as published by the Free Software Foundation; either version 2
2.26 -% of the License, or (at your option) any later version.
2.27 -%
2.28 -% This program is distributed in the hope that it will be useful,
2.29 -% but WITHOUT ANY WARRANTY; without even the implied warranty of
2.30 -% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
2.31 -% GNU General Public License for more details.
2.32 -%
2.33 -% For a copy of the GNU General Public License, write to the
2.34 -% Free Software Foundation, Inc.,
2.35 -% 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA,
2.36 -% or find it on the net, for instance at
2.37 -% http://www.gnu.org/copyleft/gpl.html
2.38 -%
2.39 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2.40 -% This style can be used with plain TeX or LaTeX, and probably
2.41 -% most other packages too.
2.42 -%
2.43 -% Usage: all text included between
2.44 -% \comment ... \endcomment
2.45 -% or \begin{comment} ... \end{comment}
2.46 -% is discarded.
2.47 -%
2.48 -% The opening and closing commands should appear on a line
2.49 -% of their own. No starting spaces, nothing after it.
2.50 -% This environment should work with arbitrary amounts
2.51 -% of comment, and the comment can be arbitrary text.
2.52 -%
2.53 -% Other `comment' environments are defined by
2.54 -% and are selected/deselected with
2.55 -% \includecomment{versiona}
2.56 -% \excludecoment{versionb}
2.57 -%
2.58 -% These environments are used as
2.59 -% \versiona ... \endversiona
2.60 -% or \begin{versiona} ... \end{versiona}
2.61 -% with the opening and closing commands again on a line of
2.62 -% their own.
2.63 -%
2.64 -% LaTeX users note: for an included comment, the
2.65 -% \begin and \end lines act as if they don't exist.
2.66 -% In particular, they don't imply grouping, so assignments
2.67 -% &c are not local.
2.68 -%
2.69 -% Special comments are defined as
2.70 -% \specialcomment{name}{before commands}{after commands}
2.71 -% where the second and third arguments are executed before
2.72 -% and after each comment block. You can use this for global
2.73 -% formatting commands.
2.74 -% To keep definitions &c local, you can include \begingroup
2.75 -% in the `before commands' and \endgroup in the `after commands'.
2.76 -% ex:
2.77 -% \specialcomment{smalltt}
2.78 -% {\begingroup\ttfamily\footnotesize}{\endgroup}
2.79 -% You do *not* have to do an additional
2.80 -% \includecomment{smalltt}
2.81 -% To remove 'smalltt' blocks, give \excludecomment{smalltt}
2.82 -% after the definition.
2.83 -%
2.84 -% Processing comments can apply processing to each line.
2.85 -% \processcomment{name}{each-line commands}%
2.86 -% {before commands}{after commands}
2.87 -% By defining a control sequence
2.88 -% \def\Thiscomment##1{...} in the before commands the user can
2.89 -% specify what is to be done with each comment line.
2.90 -% BUG this does not work quite yet BUG
2.91 -%
2.92 -% Trick for short in/exclude macros (such as \maybe{this snippet}):
2.93 -%\includecomment{cond}
2.94 -%\newcommand{\maybe}[1]{}
2.95 -%\begin{cond}
2.96 -%\renewcommand{\maybe}[1]{#1}
2.97 -%\end{cond}
2.98 -%
2.99 -% Basic approach of the implementation:
2.100 -% to comment something out, scoop up every line in verbatim mode
2.101 -% as macro argument, then throw it away.
2.102 -% For inclusions, in LaTeX the block is written out to
2.103 -% a file \CommentCutFile (default "comment.cut"), which is
2.104 -% then included.
2.105 -% In plain TeX (and other formats) both the opening and
2.106 -% closing comands are defined as noop.
2.107 -%
2.108 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2.109 -% Changes in version 3.1
2.110 -% - updated author's address
2.111 -% - cleaned up some code
2.112 -% - trailing contents on \begin{env} line is always discarded
2.113 -% even if you've done \includecomment{env}
2.114 -% - comments no longer define grouping!! you can even
2.115 -% \includecomment{env}
2.116 -% \begin{env}
2.117 -% \begin{itemize}
2.118 -% \end{env}
2.119 -% Isn't that something ...
2.120 -% - included comments are written to file and input again.
2.121 -% Changes in 3.2
2.122 -% - \specialcomment brought up to date (thanks to Ivo Welch).
2.123 -% Changes in 3.3
2.124 -% - updated author's address again
2.125 -% - parametrised \CommentCutFile
2.126 -% Changes in 3.4
2.127 -% - added GNU public license
2.128 -% - added \processcomment, because Ivo's fix (above) brought an
2.129 -% inconsistency to light.
2.130 -% Changes in 3.5
2.131 -% - corrected typo in header.
2.132 -% - changed author email
2.133 -% - corrected \specialcomment yet again.
2.134 -% - fixed excludecomment of an earlier defined environment.
2.135 -% Changes in 3.6
2.136 -% - The 'cut' file is now written more verbatim, using \meaning;
2.137 -% some people reported having trouble with ISO latin 1, or umlaute.sty.
2.138 -% - removed some \newif statements.
2.139 -% Has this suddenly become \outer again?
2.140 -%
2.141 -% Known bugs:
2.142 -% - excludecomment leads to one superfluous space
2.143 -% - processcomment leads to a superfluous line break
2.144 -%
2.145 -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2.146 -
2.147 -\def\makeinnocent#1{\catcode`#1=12 }
2.148 -\def\csarg#1#2{\expandafter#1\csname#2\endcsname}
2.149 -\def\latexname{lplain}\def\latexename{LaTeX2e}
2.150 -\newwrite\CommentStream
2.151 -\def\CommentCutFile{comment.cut}
2.152 -
2.153 -\def\ProcessComment#1% start it all of
2.154 - {\begingroup
2.155 - \def\CurrentComment{#1}%
2.156 - \let\do\makeinnocent \dospecials
2.157 - \makeinnocent\^^L% and whatever other special cases
2.158 - \endlinechar`\^^M \catcode`\^^M=12 \xComment}
2.159 -%\def\ProcessCommentWithArg#1#2% to be used in \leveledcomment
2.160 -% {\begingroup
2.161 -% \def\CurrentComment{#1}%
2.162 -% \let\do\makeinnocent \dospecials
2.163 -% \makeinnocent\^^L% and whatever other special cases
2.164 -% \endlinechar`\^^M \catcode`\^^M=12 \xComment}
2.165 -{\catcode`\^^M=12 \endlinechar=-1 %
2.166 - \gdef\xComment#1^^M{%
2.167 - \expandafter\ProcessCommentLine}
2.168 - \gdef\ProcessCommentLine#1^^M{\def\test{#1}
2.169 - \csarg\ifx{End\CurrentComment Test}\test
2.170 - \edef\next{\noexpand\EndOfComment{\CurrentComment}}%
2.171 - \else \ThisComment{#1}\let\next\ProcessCommentLine
2.172 - \fi \next}
2.173 -}
2.174 -
2.175 -\def\CSstringmeaning#1{\expandafter\CSgobblearrow\meaning#1}
2.176 -\def\CSstringcsnoescape#1{\expandafter\CSgobbleescape\string#1}
2.177 -{\escapechar-1
2.178 -\expandafter\expandafter\expandafter\gdef
2.179 - \expandafter\expandafter\expandafter\CSgobblearrow
2.180 - \expandafter\string\csname macro:->\endcsname{}
2.181 -}
2.182 -\def\CSgobbleescape#1{\ifnum`\\=`#1 \else #1\fi}
2.183 -\def\WriteCommentLine#1{\def\CStmp{#1}%
2.184 - \immediate\write\CommentStream{\CSstringmeaning\CStmp}}
2.185 -
2.186 -% 3.1 change: in LaTeX and LaTeX2e prevent grouping
2.187 -\if 0%
2.188 -\ifx\fmtname\latexename
2.189 - 0%
2.190 -\else \ifx\fmtname\latexname
2.191 - 0%
2.192 - \else
2.193 - 1%
2.194 -\fi \fi
2.195 -%%%%
2.196 -%%%% definitions for LaTeX
2.197 -%%%%
2.198 -\def\AfterIncludedComment
2.199 - {\immediate\closeout\CommentStream
2.200 - \input{\CommentCutFile}\relax
2.201 - }%
2.202 -\def\TossComment{\immediate\closeout\CommentStream}
2.203 -\def\BeforeIncludedComment
2.204 - {\immediate\openout\CommentStream=\CommentCutFile
2.205 - \let\ThisComment\WriteCommentLine}
2.206 -\def\includecomment
2.207 - #1{\message{Include comment '#1'}%
2.208 - \csarg\let{After#1Comment}\AfterIncludedComment
2.209 - \csarg\def{#1}{\BeforeIncludedComment
2.210 - \ProcessComment{#1}}%
2.211 - \CommentEndDef{#1}}
2.212 -\long\def\specialcomment
2.213 - #1#2#3{\message{Special comment '#1'}%
2.214 - % note: \AfterIncludedComment does \input, so #2 goes here!
2.215 - \csarg\def{After#1Comment}{#2\AfterIncludedComment#3}%
2.216 - \csarg\def{#1}{\BeforeIncludedComment\relax
2.217 - \ProcessComment{#1}}%
2.218 - \CommentEndDef{#1}}
2.219 -\long\def\processcomment
2.220 - #1#2#3#4{\message{Lines-Processing comment '#1'}%
2.221 - \csarg\def{After#1Comment}{#3\AfterIncludedComment#4}%
2.222 - \csarg\def{#1}{\BeforeIncludedComment#2\relax
2.223 - \ProcessComment{#1}}%
2.224 - \CommentEndDef{#1}}
2.225 -\def\leveledcomment
2.226 - #1#2{\message{Include comment '#1' up to level '#2'}%
2.227 - %\csname #1IsLeveledCommenttrue\endcsname
2.228 - \csarg\let{After#1Comment}\AfterIncludedComment
2.229 - \csarg\def{#1}{\BeforeIncludedComment
2.230 - \ProcessCommentWithArg{#1}}%
2.231 - \CommentEndDef{#1}}
2.232 -\else
2.233 -%%%%
2.234 -%%%%plain TeX and other formats
2.235 -%%%%
2.236 -\def\includecomment
2.237 - #1{\message{Including comment '#1'}%
2.238 - \csarg\def{#1}{}%
2.239 - \csarg\def{end#1}{}}
2.240 -\long\def\specialcomment
2.241 - #1#2#3{\message{Special comment '#1'}%
2.242 - \csarg\def{#1}{\def\ThisComment{}\def\AfterComment{#3}#2%
2.243 - \ProcessComment{#1}}%
2.244 - \CommentEndDef{#1}}
2.245 -\fi
2.246 -
2.247 -%%%%
2.248 -%%%% general definition of skipped comment
2.249 -%%%%
2.250 -\def\excludecomment
2.251 - #1{\message{Excluding comment '#1'}%
2.252 - \csarg\def{#1}{\let\AfterComment\relax
2.253 - \def\ThisComment####1{}\ProcessComment{#1}}%
2.254 - \csarg\let{After#1Comment}\TossComment
2.255 - \CommentEndDef{#1}}
2.256 -
2.257 -\if 0%
2.258 -\ifx\fmtname\latexename
2.259 - 0%
2.260 -\else \ifx\fmtname\latexname
2.261 - 0%
2.262 - \else
2.263 - 1%
2.264 -\fi \fi
2.265 -% latex & latex2e:
2.266 -\def\EndOfComment#1{\endgroup\end{#1}%
2.267 - \csname After#1Comment\endcsname}
2.268 -\def\CommentEndDef#1{{\escapechar=-1\relax
2.269 - \csarg\xdef{End#1Test}{\string\\end\string\{#1\string\}}%
2.270 - }}
2.271 -\else
2.272 -% plain & other
2.273 -\def\EndOfComment#1{\endgroup\AfterComment}
2.274 -\def\CommentEndDef#1{{\escapechar=-1\relax
2.275 - \csarg\xdef{End#1Test}{\string\\end#1}%
2.276 - }}
2.277 -\fi
2.278 -
2.279 -\excludecomment{comment}
2.280 -
2.281 -\endinput
3.1 --- a/src/Tools/isac/Doc/isabelle.sty Thu Apr 08 13:09:44 2021 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,269 +0,0 @@
3.4 -%%
3.5 -%% macros for Isabelle generated LaTeX output
3.6 -%%
3.7 -
3.8 -%%% Simple document preparation (based on theory token language and symbols)
3.9 -
3.10 -% isabelle environments
3.11 -
3.12 -\newcommand{\isabellecontext}{UNKNOWN}
3.13 -\newcommand{\setisabellecontext}[1]{\def\isabellecontext{#1}}
3.14 -
3.15 -\newcommand{\isastyle}{\UNDEF}
3.16 -\newcommand{\isastylett}{\UNDEF}
3.17 -\newcommand{\isastyleminor}{\UNDEF}
3.18 -\newcommand{\isastyleminortt}{\UNDEF}
3.19 -\newcommand{\isastylescript}{\UNDEF}
3.20 -\newcommand{\isastyletext}{\normalsize\normalfont\rmfamily}
3.21 -\newcommand{\isastyletxt}{\normalfont\rmfamily}
3.22 -\newcommand{\isastylecmt}{\normalfont\rmfamily}
3.23 -
3.24 -\newcommand{\isaspacing}{%
3.25 - \sfcode 42 1000 % .
3.26 - \sfcode 63 1000 % ?
3.27 - \sfcode 33 1000 % !
3.28 - \sfcode 58 1000 % :
3.29 - \sfcode 59 1000 % ;
3.30 - \sfcode 44 1000 % ,
3.31 -}
3.32 -
3.33 -%symbol markup -- \emph achieves decent spacing via italic corrections
3.34 -\newcommand{\isamath}[1]{\emph{$#1$}}
3.35 -\newcommand{\isatext}[1]{\emph{#1}}
3.36 -\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isaspacing\isastylescript##1}}}
3.37 -\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
3.38 -\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
3.39 -\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isaspacing\isastylescript}
3.40 -\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
3.41 -\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isaspacing\isastylescript}
3.42 -\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
3.43 -\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
3.44 -
3.45 -\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
3.46 -
3.47 -\newdimen\isa@parindent\newdimen\isa@parskip
3.48 -
3.49 -\newenvironment{isabellebody}{%
3.50 -\isamarkuptrue\par%
3.51 -\isa@parindent\parindent\parindent0pt%
3.52 -\isa@parskip\parskip\parskip0pt%
3.53 -\isaspacing\isastyle}{\par}
3.54 -
3.55 -\newenvironment{isabellebodytt}{%
3.56 -\isamarkuptrue\par%
3.57 -\isa@parindent\parindent\parindent0pt%
3.58 -\isa@parskip\parskip\parskip0pt%
3.59 -\isaspacing\isastylett}{\par}
3.60 -
3.61 -\newenvironment{isabelle}
3.62 -{\begin{trivlist}\begin{isabellebody}\item\relax}
3.63 -{\end{isabellebody}\end{trivlist}}
3.64 -
3.65 -\newenvironment{isabellett}
3.66 -{\begin{trivlist}\begin{isabellebodytt}\item\relax}
3.67 -{\end{isabellebodytt}\end{trivlist}}
3.68 -
3.69 -\newcommand{\isa}[1]{\emph{\isaspacing\isastyleminor #1}}
3.70 -\newcommand{\isatt}[1]{\emph{\isaspacing\isastyleminortt #1}}
3.71 -
3.72 -\newcommand{\isaindent}[1]{\hphantom{#1}}
3.73 -\newcommand{\isanewline}{\mbox{}\par\mbox{}}
3.74 -\newcommand{\isasep}{}
3.75 -\newcommand{\isadigit}[1]{#1}
3.76 -
3.77 -\newcommand{\isachardefaults}{%
3.78 -\def\isacharbell{\isamath{\bigbox}}%requires stmaryrd
3.79 -\chardef\isacharbang=`\!%
3.80 -\chardef\isachardoublequote=`\"%
3.81 -\chardef\isachardoublequoteopen=`\"%
3.82 -\chardef\isachardoublequoteclose=`\"%
3.83 -\chardef\isacharhash=`\#%
3.84 -\chardef\isachardollar=`\$%
3.85 -\chardef\isacharpercent=`\%%
3.86 -\chardef\isacharampersand=`\&%
3.87 -\chardef\isacharprime=`\'%
3.88 -\chardef\isacharparenleft=`\(%
3.89 -\chardef\isacharparenright=`\)%
3.90 -\chardef\isacharasterisk=`\*%
3.91 -\chardef\isacharplus=`\+%
3.92 -\chardef\isacharcomma=`\,%
3.93 -\chardef\isacharminus=`\-%
3.94 -\chardef\isachardot=`\.%
3.95 -\chardef\isacharslash=`\/%
3.96 -\chardef\isacharcolon=`\:%
3.97 -\chardef\isacharsemicolon=`\;%
3.98 -\chardef\isacharless=`\<%
3.99 -\chardef\isacharequal=`\=%
3.100 -\chardef\isachargreater=`\>%
3.101 -\chardef\isacharquery=`\?%
3.102 -\chardef\isacharat=`\@%
3.103 -\chardef\isacharbrackleft=`\[%
3.104 -\chardef\isacharbackslash=`\\%
3.105 -\chardef\isacharbrackright=`\]%
3.106 -\chardef\isacharcircum=`\^%
3.107 -\chardef\isacharunderscore=`\_%
3.108 -\def\isacharunderscorekeyword{\_}%
3.109 -\chardef\isacharbackquote=`\`%
3.110 -\chardef\isacharbackquoteopen=`\`%
3.111 -\chardef\isacharbackquoteclose=`\`%
3.112 -\chardef\isacharbraceleft=`\{%
3.113 -\chardef\isacharbar=`\|%
3.114 -\chardef\isacharbraceright=`\}%
3.115 -\chardef\isachartilde=`\~%
3.116 -\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%
3.117 -\def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
3.118 -\def\isacartoucheopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
3.119 -\def\isacartoucheclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
3.120 -}
3.121 -
3.122 -
3.123 -% keyword and section markup
3.124 -
3.125 -\newcommand{\isakeyword}[1]
3.126 -{\emph{\normalfont\bfseries\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
3.127 -\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
3.128 -\newcommand{\isacommand}[1]{\isakeyword{#1}}
3.129 -
3.130 -\newcommand{\isakeywordcontrol}[1]
3.131 -{\emph{\normalfont\bfseries\itshape\def\isacharunderscore{\isacharunderscorekeyword}#1\,}}
3.132 -
3.133 -\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
3.134 -\newcommand{\isamarkupsection}[1]{\section{#1}}
3.135 -\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
3.136 -\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
3.137 -\newcommand{\isamarkupparagraph}[1]{\paragraph{#1}}
3.138 -\newcommand{\isamarkupsubparagraph}[1]{\subparagraph{#1}}
3.139 -
3.140 -\newif\ifisamarkup
3.141 -\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
3.142 -\newcommand{\isaendpar}{\par\medskip}
3.143 -\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
3.144 -\newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}
3.145 -\newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}
3.146 -\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
3.147 -
3.148 -
3.149 -% styles
3.150 -
3.151 -\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
3.152 -
3.153 -\newcommand{\isabellestyledefault}{%
3.154 -\def\isastyle{\small\normalfont\ttfamily\slshape}%
3.155 -\def\isastylett{\small\normalfont\ttfamily}%
3.156 -\def\isastyleminor{\small\normalfont\ttfamily\slshape}%
3.157 -\def\isastyleminortt{\small\normalfont\ttfamily}%
3.158 -\def\isastylescript{\footnotesize\normalfont\ttfamily\slshape}%
3.159 -\isachardefaults%
3.160 -}
3.161 -\isabellestyledefault
3.162 -
3.163 -\newcommand{\isabellestylett}{%
3.164 -\def\isastyle{\small\normalfont\ttfamily}%
3.165 -\def\isastylett{\small\normalfont\ttfamily}%
3.166 -\def\isastyleminor{\small\normalfont\ttfamily}%
3.167 -\def\isastyleminortt{\small\normalfont\ttfamily}%
3.168 -\def\isastylescript{\footnotesize\normalfont\ttfamily}%
3.169 -\isachardefaults%
3.170 -}
3.171 -
3.172 -\newcommand{\isabellestyleit}{%
3.173 -\def\isastyle{\small\normalfont\itshape}%
3.174 -\def\isastylett{\small\normalfont\ttfamily}%
3.175 -\def\isastyleminor{\normalfont\itshape}%
3.176 -\def\isastyleminortt{\normalfont\ttfamily}%
3.177 -\def\isastylescript{\footnotesize\normalfont\itshape}%
3.178 -\isachardefaults%
3.179 -\def\isacharunderscorekeyword{\mbox{-}}%
3.180 -\def\isacharbang{\isamath{!}}%
3.181 -\def\isachardoublequote{}%
3.182 -\def\isachardoublequoteopen{}%
3.183 -\def\isachardoublequoteclose{}%
3.184 -\def\isacharhash{\isamath{\#}}%
3.185 -\def\isachardollar{\isamath{\$}}%
3.186 -\def\isacharpercent{\isamath{\%}}%
3.187 -\def\isacharampersand{\isamath{\&}}%
3.188 -\def\isacharprime{\isamath{\mskip2mu{'}\mskip-2mu}}%
3.189 -\def\isacharparenleft{\isamath{(}}%
3.190 -\def\isacharparenright{\isamath{)}}%
3.191 -\def\isacharasterisk{\isamath{*}}%
3.192 -\def\isacharplus{\isamath{+}}%
3.193 -\def\isacharcomma{\isamath{\mathord,}}%
3.194 -\def\isacharminus{\isamath{-}}%
3.195 -\def\isachardot{\isamath{\mathord.}}%
3.196 -\def\isacharslash{\isamath{/}}%
3.197 -\def\isacharcolon{\isamath{\mathord:}}%
3.198 -\def\isacharsemicolon{\isamath{\mathord;}}%
3.199 -\def\isacharless{\isamath{<}}%
3.200 -\def\isacharequal{\isamath{=}}%
3.201 -\def\isachargreater{\isamath{>}}%
3.202 -\def\isacharat{\isamath{@}}%
3.203 -\def\isacharbrackleft{\isamath{[}}%
3.204 -\def\isacharbackslash{\isamath{\backslash}}%
3.205 -\def\isacharbrackright{\isamath{]}}%
3.206 -\def\isacharunderscore{\mbox{-}}%
3.207 -\def\isacharbraceleft{\isamath{\{}}%
3.208 -\def\isacharbar{\isamath{\mid}}%
3.209 -\def\isacharbraceright{\isamath{\}}}%
3.210 -\def\isachartilde{\isamath{{}\sp{\sim}}}%
3.211 -\def\isacharbackquoteopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
3.212 -\def\isacharbackquoteclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
3.213 -\def\isacharverbatimopen{\isamath{\langle\!\langle}}%
3.214 -\def\isacharverbatimclose{\isamath{\rangle\!\rangle}}%
3.215 -}
3.216 -
3.217 -\newcommand{\isabellestyleliteral}{%
3.218 -\isabellestyleit%
3.219 -\def\isacharunderscore{\_}%
3.220 -\def\isacharunderscorekeyword{\_}%
3.221 -\chardef\isacharbackquoteopen=`\`%
3.222 -\chardef\isacharbackquoteclose=`\`%
3.223 -}
3.224 -
3.225 -\newcommand{\isabellestyleliteralunderscore}{%
3.226 -\isabellestyleliteral%
3.227 -\def\isacharunderscore{\textunderscore}%
3.228 -\def\isacharunderscorekeyword{\textunderscore}%
3.229 -}
3.230 -
3.231 -\newcommand{\isabellestylesl}{%
3.232 -\isabellestyleit%
3.233 -\def\isastyle{\small\normalfont\slshape}%
3.234 -\def\isastylett{\small\normalfont\ttfamily}%
3.235 -\def\isastyleminor{\normalfont\slshape}%
3.236 -\def\isastyleminortt{\normalfont\ttfamily}%
3.237 -\def\isastylescript{\footnotesize\normalfont\slshape}%
3.238 -}
3.239 -
3.240 -
3.241 -% cancel text
3.242 -
3.243 -\usepackage[normalem]{ulem}
3.244 -\newcommand{\isamarkupcancel}[1]{\isa{\xout{#1}}}
3.245 -
3.246 -
3.247 -% tagged regions
3.248 -
3.249 -%plain TeX version of comment package -- much faster!
3.250 -\let\isafmtname\fmtname\def\fmtname{plain}
3.251 -\usepackage{comment}
3.252 -\let\fmtname\isafmtname
3.253 -
3.254 -\newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}}
3.255 -
3.256 -\newcommand{\isakeeptag}[1]%
3.257 -{\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
3.258 -\newcommand{\isadroptag}[1]%
3.259 -{\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
3.260 -\newcommand{\isafoldtag}[1]%
3.261 -{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
3.262 -
3.263 -\isakeeptag{document}
3.264 -\isakeeptag{theory}
3.265 -\isakeeptag{proof}
3.266 -\isakeeptag{ML}
3.267 -\isakeeptag{visible}
3.268 -\isadroptag{invisible}
3.269 -\isakeeptag{important}
3.270 -\isakeeptag{unimportant}
3.271 -
3.272 -\IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{}
4.1 --- a/src/Tools/isac/Doc/isabellesym.sty Thu Apr 08 13:09:44 2021 +0200
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,417 +0,0 @@
4.4 -%%
4.5 -%% definitions of standard Isabelle symbols
4.6 -%%
4.7 -
4.8 -\newcommand{\isasymzero}{\isamath{\mathbf{0}}} %requires amssymb
4.9 -\newcommand{\isasymone}{\isamath{\mathbf{1}}} %requires amssymb
4.10 -\newcommand{\isasymtwo}{\isamath{\mathbf{2}}} %requires amssymb
4.11 -\newcommand{\isasymthree}{\isamath{\mathbf{3}}} %requires amssymb
4.12 -\newcommand{\isasymfour}{\isamath{\mathbf{4}}} %requires amssymb
4.13 -\newcommand{\isasymfive}{\isamath{\mathbf{5}}} %requires amssymb
4.14 -\newcommand{\isasymsix}{\isamath{\mathbf{6}}} %requires amssymb
4.15 -\newcommand{\isasymseven}{\isamath{\mathbf{7}}} %requires amssymb
4.16 -\newcommand{\isasymeight}{\isamath{\mathbf{8}}} %requires amssymb
4.17 -\newcommand{\isasymnine}{\isamath{\mathbf{9}}} %requires amssymb
4.18 -\newcommand{\isasymA}{\isamath{\mathcal{A}}}
4.19 -\newcommand{\isasymB}{\isamath{\mathcal{B}}}
4.20 -\newcommand{\isasymC}{\isamath{\mathcal{C}}}
4.21 -\newcommand{\isasymD}{\isamath{\mathcal{D}}}
4.22 -\newcommand{\isasymE}{\isamath{\mathcal{E}}}
4.23 -\newcommand{\isasymF}{\isamath{\mathcal{F}}}
4.24 -\newcommand{\isasymG}{\isamath{\mathcal{G}}}
4.25 -\newcommand{\isasymH}{\isamath{\mathcal{H}}}
4.26 -\newcommand{\isasymI}{\isamath{\mathcal{I}}}
4.27 -\newcommand{\isasymJ}{\isamath{\mathcal{J}}}
4.28 -\newcommand{\isasymK}{\isamath{\mathcal{K}}}
4.29 -\newcommand{\isasymL}{\isamath{\mathcal{L}}}
4.30 -\newcommand{\isasymM}{\isamath{\mathcal{M}}}
4.31 -\newcommand{\isasymN}{\isamath{\mathcal{N}}}
4.32 -\newcommand{\isasymO}{\isamath{\mathcal{O}}}
4.33 -\newcommand{\isasymP}{\isamath{\mathcal{P}}}
4.34 -\newcommand{\isasymQ}{\isamath{\mathcal{Q}}}
4.35 -\newcommand{\isasymR}{\isamath{\mathcal{R}}}
4.36 -\newcommand{\isasymS}{\isamath{\mathcal{S}}}
4.37 -\newcommand{\isasymT}{\isamath{\mathcal{T}}}
4.38 -\newcommand{\isasymU}{\isamath{\mathcal{U}}}
4.39 -\newcommand{\isasymV}{\isamath{\mathcal{V}}}
4.40 -\newcommand{\isasymW}{\isamath{\mathcal{W}}}
4.41 -\newcommand{\isasymX}{\isamath{\mathcal{X}}}
4.42 -\newcommand{\isasymY}{\isamath{\mathcal{Y}}}
4.43 -\newcommand{\isasymZ}{\isamath{\mathcal{Z}}}
4.44 -\newcommand{\isasyma}{\isamath{\mathrm{a}}}
4.45 -\newcommand{\isasymb}{\isamath{\mathrm{b}}}
4.46 -\newcommand{\isasymc}{\isamath{\mathrm{c}}}
4.47 -\newcommand{\isasymd}{\isamath{\mathrm{d}}}
4.48 -\newcommand{\isasyme}{\isamath{\mathrm{e}}}
4.49 -\newcommand{\isasymf}{\isamath{\mathrm{f}}}
4.50 -\newcommand{\isasymg}{\isamath{\mathrm{g}}}
4.51 -\newcommand{\isasymh}{\isamath{\mathrm{h}}}
4.52 -\newcommand{\isasymi}{\isamath{\mathrm{i}}}
4.53 -\newcommand{\isasymj}{\isamath{\mathrm{j}}}
4.54 -\newcommand{\isasymk}{\isamath{\mathrm{k}}}
4.55 -\newcommand{\isasyml}{\isamath{\mathrm{l}}}
4.56 -\newcommand{\isasymm}{\isamath{\mathrm{m}}}
4.57 -\newcommand{\isasymn}{\isamath{\mathrm{n}}}
4.58 -\newcommand{\isasymo}{\isamath{\mathrm{o}}}
4.59 -\newcommand{\isasymp}{\isamath{\mathrm{p}}}
4.60 -\newcommand{\isasymq}{\isamath{\mathrm{q}}}
4.61 -\newcommand{\isasymr}{\isamath{\mathrm{r}}}
4.62 -\newcommand{\isasyms}{\isamath{\mathrm{s}}}
4.63 -\newcommand{\isasymt}{\isamath{\mathrm{t}}}
4.64 -\newcommand{\isasymu}{\isamath{\mathrm{u}}}
4.65 -\newcommand{\isasymv}{\isamath{\mathrm{v}}}
4.66 -\newcommand{\isasymw}{\isamath{\mathrm{w}}}
4.67 -\newcommand{\isasymx}{\isamath{\mathrm{x}}}
4.68 -\newcommand{\isasymy}{\isamath{\mathrm{y}}}
4.69 -\newcommand{\isasymz}{\isamath{\mathrm{z}}}
4.70 -\newcommand{\isasymAA}{\isamath{\mathfrak{A}}} %requires eufrak
4.71 -\newcommand{\isasymBB}{\isamath{\mathfrak{B}}} %requires eufrak
4.72 -\newcommand{\isasymCC}{\isamath{\mathfrak{C}}} %requires eufrak
4.73 -\newcommand{\isasymDD}{\isamath{\mathfrak{D}}} %requires eufrak
4.74 -\newcommand{\isasymEE}{\isamath{\mathfrak{E}}} %requires eufrak
4.75 -\newcommand{\isasymFF}{\isamath{\mathfrak{F}}} %requires eufrak
4.76 -\newcommand{\isasymGG}{\isamath{\mathfrak{G}}} %requires eufrak
4.77 -\newcommand{\isasymHH}{\isamath{\mathfrak{H}}} %requires eufrak
4.78 -\newcommand{\isasymII}{\isamath{\mathfrak{I}}} %requires eufrak
4.79 -\newcommand{\isasymJJ}{\isamath{\mathfrak{J}}} %requires eufrak
4.80 -\newcommand{\isasymKK}{\isamath{\mathfrak{K}}} %requires eufrak
4.81 -\newcommand{\isasymLL}{\isamath{\mathfrak{L}}} %requires eufrak
4.82 -\newcommand{\isasymMM}{\isamath{\mathfrak{M}}} %requires eufrak
4.83 -\newcommand{\isasymNN}{\isamath{\mathfrak{N}}} %requires eufrak
4.84 -\newcommand{\isasymOO}{\isamath{\mathfrak{O}}} %requires eufrak
4.85 -\newcommand{\isasymPP}{\isamath{\mathfrak{P}}} %requires eufrak
4.86 -\newcommand{\isasymQQ}{\isamath{\mathfrak{Q}}} %requires eufrak
4.87 -\newcommand{\isasymRR}{\isamath{\mathfrak{R}}} %requires eufrak
4.88 -\newcommand{\isasymSS}{\isamath{\mathfrak{S}}} %requires eufrak
4.89 -\newcommand{\isasymTT}{\isamath{\mathfrak{T}}} %requires eufrak
4.90 -\newcommand{\isasymUU}{\isamath{\mathfrak{U}}} %requires eufrak
4.91 -\newcommand{\isasymVV}{\isamath{\mathfrak{V}}} %requires eufrak
4.92 -\newcommand{\isasymWW}{\isamath{\mathfrak{W}}} %requires eufrak
4.93 -\newcommand{\isasymXX}{\isamath{\mathfrak{X}}} %requires eufrak
4.94 -\newcommand{\isasymYY}{\isamath{\mathfrak{Y}}} %requires eufrak
4.95 -\newcommand{\isasymZZ}{\isamath{\mathfrak{Z}}} %requires eufrak
4.96 -\newcommand{\isasymaa}{\isamath{\mathfrak{a}}} %requires eufrak
4.97 -\newcommand{\isasymbb}{\isamath{\mathfrak{b}}} %requires eufrak
4.98 -\newcommand{\isasymcc}{\isamath{\mathfrak{c}}} %requires eufrak
4.99 -\newcommand{\isasymdd}{\isamath{\mathfrak{d}}} %requires eufrak
4.100 -\newcommand{\isasymee}{\isamath{\mathfrak{e}}} %requires eufrak
4.101 -\newcommand{\isasymff}{\isamath{\mathfrak{f}}} %requires eufrak
4.102 -\newcommand{\isasymgg}{\isamath{\mathfrak{g}}} %requires eufrak
4.103 -\newcommand{\isasymhh}{\isamath{\mathfrak{h}}} %requires eufrak
4.104 -\newcommand{\isasymii}{\isamath{\mathfrak{i}}} %requires eufrak
4.105 -\newcommand{\isasymjj}{\isamath{\mathfrak{j}}} %requires eufrak
4.106 -\newcommand{\isasymkk}{\isamath{\mathfrak{k}}} %requires eufrak
4.107 -\newcommand{\isasymll}{\isamath{\mathfrak{l}}} %requires eufrak
4.108 -\newcommand{\isasymmm}{\isamath{\mathfrak{m}}} %requires eufrak
4.109 -\newcommand{\isasymnn}{\isamath{\mathfrak{n}}} %requires eufrak
4.110 -\newcommand{\isasymoo}{\isamath{\mathfrak{o}}} %requires eufrak
4.111 -\newcommand{\isasympp}{\isamath{\mathfrak{p}}} %requires eufrak
4.112 -\newcommand{\isasymqq}{\isamath{\mathfrak{q}}} %requires eufrak
4.113 -\newcommand{\isasymrr}{\isamath{\mathfrak{r}}} %requires eufrak
4.114 -\newcommand{\isasymss}{\isamath{\mathfrak{s}}} %requires eufrak
4.115 -\newcommand{\isasymtt}{\isamath{\mathfrak{t}}} %requires eufrak
4.116 -\newcommand{\isasymuu}{\isamath{\mathfrak{u}}} %requires eufrak
4.117 -\newcommand{\isasymvv}{\isamath{\mathfrak{v}}} %requires eufrak
4.118 -\newcommand{\isasymww}{\isamath{\mathfrak{w}}} %requires eufrak
4.119 -\newcommand{\isasymxx}{\isamath{\mathfrak{x}}} %requires eufrak
4.120 -\newcommand{\isasymyy}{\isamath{\mathfrak{y}}} %requires eufrak
4.121 -\newcommand{\isasymzz}{\isamath{\mathfrak{z}}} %requires eufrak
4.122 -\newcommand{\isasymalpha}{\isamath{\alpha}}
4.123 -\newcommand{\isasymbeta}{\isamath{\beta}}
4.124 -\newcommand{\isasymgamma}{\isamath{\gamma}}
4.125 -\newcommand{\isasymdelta}{\isamath{\delta}}
4.126 -\newcommand{\isasymepsilon}{\isamath{\varepsilon}}
4.127 -\newcommand{\isasymzeta}{\isamath{\zeta}}
4.128 -\newcommand{\isasymeta}{\isamath{\eta}}
4.129 -\newcommand{\isasymtheta}{\isamath{\vartheta}}
4.130 -\newcommand{\isasymiota}{\isamath{\iota}}
4.131 -\newcommand{\isasymkappa}{\isamath{\kappa}}
4.132 -\newcommand{\isasymlambda}{\isamath{\lambda}}
4.133 -\newcommand{\isasymmu}{\isamath{\mu}}
4.134 -\newcommand{\isasymnu}{\isamath{\nu}}
4.135 -\newcommand{\isasymxi}{\isamath{\xi}}
4.136 -\newcommand{\isasympi}{\isamath{\pi}}
4.137 -\newcommand{\isasymrho}{\isamath{\varrho}}
4.138 -\newcommand{\isasymsigma}{\isamath{\sigma}}
4.139 -\newcommand{\isasymtau}{\isamath{\tau}}
4.140 -\newcommand{\isasymupsilon}{\isamath{\upsilon}}
4.141 -\newcommand{\isasymphi}{\isamath{\varphi}}
4.142 -\newcommand{\isasymchi}{\isamath{\chi}}
4.143 -\newcommand{\isasympsi}{\isamath{\psi}}
4.144 -\newcommand{\isasymomega}{\isamath{\omega}}
4.145 -\newcommand{\isasymGamma}{\isamath{\Gamma}}
4.146 -\newcommand{\isasymDelta}{\isamath{\Delta}}
4.147 -\newcommand{\isasymTheta}{\isamath{\Theta}}
4.148 -\newcommand{\isasymLambda}{\isamath{\Lambda}}
4.149 -\newcommand{\isasymXi}{\isamath{\Xi}}
4.150 -\newcommand{\isasymPi}{\isamath{\Pi}}
4.151 -\newcommand{\isasymSigma}{\isamath{\Sigma}}
4.152 -\newcommand{\isasymUpsilon}{\isamath{\Upsilon}}
4.153 -\newcommand{\isasymPhi}{\isamath{\Phi}}
4.154 -\newcommand{\isasymPsi}{\isamath{\Psi}}
4.155 -\newcommand{\isasymOmega}{\isamath{\Omega}}
4.156 -\newcommand{\isasymbool}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{B}}}
4.157 -\newcommand{\isasymcomplex}{\isamath{\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu}}
4.158 -\newcommand{\isasymnat}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
4.159 -\newcommand{\isasymrat}{\isamath{\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu}}
4.160 -\newcommand{\isasymreal}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{R}}}
4.161 -\newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}}
4.162 -\newcommand{\isasymleftarrow}{\isamath{\leftarrow}}
4.163 -\newcommand{\isasymrightarrow}{\isamath{\rightarrow}}
4.164 -\newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}}
4.165 -\newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}}
4.166 -\newcommand{\isasymlonglongleftarrow}{\isamath{\xleftarrow{\hphantom{AAA}}}} %requires amsmath
4.167 -\newcommand{\isasymlonglongrightarrow}{\isamath{\xrightarrow{\hphantom{AAA}}}} %requires amsmath
4.168 -\newcommand{\isasymlonglonglongleftarrow}{\isamath{\xleftarrow{\hphantom{AAAA}}}} %requires amsmath
4.169 -\newcommand{\isasymlonglonglongrightarrow}{\isamath{\xrightarrow{\hphantom{AAAA}}}} %requires amsmath
4.170 -\newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}}
4.171 -\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
4.172 -\newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}}
4.173 -\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}}
4.174 -\newcommand{\isasymLleftarrow}{\isamath{\Lleftarrow}} %requires amssymb
4.175 -\newcommand{\isasymRrightarrow}{\isamath{\Rrightarrow}} %requires amssymb
4.176 -\newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}}
4.177 -\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}}
4.178 -\newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}}
4.179 -\newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}}
4.180 -\newcommand{\isasymmapsto}{\isamath{\mapsto}}
4.181 -\newcommand{\isasymlongmapsto}{\isamath{\longmapsto}}
4.182 -\newcommand{\isasymmidarrow}{\isamath{\relbar}}
4.183 -\newcommand{\isasymMidarrow}{\isamath{\Relbar}}
4.184 -\newcommand{\isasymhookleftarrow}{\isamath{\hookleftarrow}}
4.185 -\newcommand{\isasymhookrightarrow}{\isamath{\hookrightarrow}}
4.186 -\newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}}
4.187 -\newcommand{\isasymrightharpoondown}{\isamath{\rightharpoondown}}
4.188 -\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
4.189 -\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
4.190 -\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
4.191 -\newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssymb
4.192 -\newcommand{\isasymdownharpoonleft}{\isamath{\downharpoonleft}} %requires amssymb
4.193 -\newcommand{\isasymdownharpoonright}{\isamath{\downharpoonright}} %requires amssymb
4.194 -\newcommand{\isasymupharpoonleft}{\isamath{\upharpoonleft}} %requires amssymb
4.195 -\newcommand{\isasymupharpoonright}{\isamath{\upharpoonright}} %requires amssymb
4.196 -\newcommand{\isasymrestriction}{\isamath{\restriction}} %requires amssymb
4.197 -\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
4.198 -\newcommand{\isasymup}{\isamath{\uparrow}}
4.199 -\newcommand{\isasymUp}{\isamath{\Uparrow}}
4.200 -\newcommand{\isasymdown}{\isamath{\downarrow}}
4.201 -\newcommand{\isasymDown}{\isamath{\Downarrow}}
4.202 -\newcommand{\isasymupdown}{\isamath{\updownarrow}}
4.203 -\newcommand{\isasymUpdown}{\isamath{\Updownarrow}}
4.204 -\newcommand{\isasymlangle}{\isamath{\langle}}
4.205 -\newcommand{\isasymrangle}{\isamath{\rangle}}
4.206 -\newcommand{\isasymlceil}{\isamath{\lceil}}
4.207 -\newcommand{\isasymrceil}{\isamath{\rceil}}
4.208 -\newcommand{\isasymlfloor}{\isamath{\lfloor}}
4.209 -\newcommand{\isasymrfloor}{\isamath{\rfloor}}
4.210 -\newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3mu\mid}}}
4.211 -\newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3mu)}}}
4.212 -\newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}}
4.213 -\newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}}
4.214 -\newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.5mu\mid}}}
4.215 -\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
4.216 -\newcommand{\isasymguillemotleft}{\isatext{\flqq}} %requires babel
4.217 -\newcommand{\isasymguillemotright}{\isatext{\frqq}} %requires babel
4.218 -\newcommand{\isasymbottom}{\isamath{\bot}}
4.219 -\newcommand{\isasymtop}{\isamath{\top}}
4.220 -\newcommand{\isasymand}{\isamath{\wedge}}
4.221 -\newcommand{\isasymAnd}{\isamath{\bigwedge}}
4.222 -\newcommand{\isasymor}{\isamath{\vee}}
4.223 -\newcommand{\isasymOr}{\isamath{\bigvee}}
4.224 -\newcommand{\isasymforall}{\isamath{\forall\,}}
4.225 -\newcommand{\isasymexists}{\isamath{\exists\,}}
4.226 -\newcommand{\isasymnot}{\isamath{\neg}}
4.227 -\newcommand{\isasymnexists}{\isamath{\nexists\,}} %requires amssymb
4.228 -\newcommand{\isasymcircle}{\isamath{\ocircle}} %requires wasysym
4.229 -\newcommand{\isasymbox}{\isamath{\Box}} %requires amssymb
4.230 -\newcommand{\isasymdiamond}{\isamath{\Diamond}} %requires amssymb
4.231 -\newcommand{\isasymdiamondop}{\isamath{\diamond}}
4.232 -\newcommand{\isasymsurd}{\isamath{\surd}}
4.233 -\newcommand{\isasymturnstile}{\isamath{\vdash}}
4.234 -\newcommand{\isasymTurnstile}{\isamath{\models}}
4.235 -\newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}
4.236 -\newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}}
4.237 -\newcommand{\isasymstileturn}{\isamath{\dashv}}
4.238 -\newcommand{\isasymle}{\isamath{\le}}
4.239 -\newcommand{\isasymge}{\isamath{\ge}}
4.240 -\newcommand{\isasymlless}{\isamath{\ll}}
4.241 -\newcommand{\isasymggreater}{\isamath{\gg}}
4.242 -\newcommand{\isasymlesssim}{\isamath{\lesssim}} %requires amssymb
4.243 -\newcommand{\isasymgreatersim}{\isamath{\gtrsim}} %requires amssymb
4.244 -\newcommand{\isasymlessapprox}{\isamath{\lessapprox}} %requires amssymb
4.245 -\newcommand{\isasymgreaterapprox}{\isamath{\gtrapprox}} %requires amssymb
4.246 -\newcommand{\isasymin}{\isamath{\in}}
4.247 -\newcommand{\isasymnotin}{\isamath{\notin}}
4.248 -\newcommand{\isasymsubset}{\isamath{\subset}}
4.249 -\newcommand{\isasymsupset}{\isamath{\supset}}
4.250 -\newcommand{\isasymsubseteq}{\isamath{\subseteq}}
4.251 -\newcommand{\isasymsupseteq}{\isamath{\supseteq}}
4.252 -\newcommand{\isasymsqsubset}{\isamath{\sqsubset}} %requires amssymb
4.253 -\newcommand{\isasymsqsupset}{\isamath{\sqsupset}} %requires amssymb
4.254 -\newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}}
4.255 -\newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}}
4.256 -\newcommand{\isasyminter}{\isamath{\cap}}
4.257 -\newcommand{\isasymInter}{\isamath{\bigcap\,}}
4.258 -\newcommand{\isasymunion}{\isamath{\cup}}
4.259 -\newcommand{\isasymUnion}{\isamath{\bigcup\,}}
4.260 -\newcommand{\isasymsqunion}{\isamath{\sqcup}}
4.261 -\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
4.262 -\newcommand{\isasymsqinter}{\isamath{\sqcap}}
4.263 -\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires stmaryrd
4.264 -\newcommand{\isasymsetminus}{\isamath{\setminus}}
4.265 -\newcommand{\isasympropto}{\isamath{\propto}}
4.266 -\newcommand{\isasymuplus}{\isamath{\uplus}}
4.267 -\newcommand{\isasymUplus}{\isamath{\biguplus\,}}
4.268 -\newcommand{\isasymnoteq}{\isamath{\not=}}
4.269 -\newcommand{\isasymsim}{\isamath{\sim}}
4.270 -\newcommand{\isasymdoteq}{\isamath{\doteq}}
4.271 -\newcommand{\isasymsimeq}{\isamath{\simeq}}
4.272 -\newcommand{\isasymapprox}{\isamath{\approx}}
4.273 -\newcommand{\isasymasymp}{\isamath{\asymp}}
4.274 -\newcommand{\isasymcong}{\isamath{\cong}}
4.275 -\newcommand{\isasymsmile}{\isamath{\smile}}
4.276 -\newcommand{\isasymequiv}{\isamath{\equiv}}
4.277 -\newcommand{\isasymfrown}{\isamath{\frown}}
4.278 -\newcommand{\isasymJoin}{\isamath{\Join}} %requires amssymb
4.279 -\newcommand{\isasymbowtie}{\isamath{\bowtie}}
4.280 -\newcommand{\isasymprec}{\isamath{\prec}}
4.281 -\newcommand{\isasymsucc}{\isamath{\succ}}
4.282 -\newcommand{\isasympreceq}{\isamath{\preceq}}
4.283 -\newcommand{\isasymsucceq}{\isamath{\succeq}}
4.284 -\newcommand{\isasymparallel}{\isamath{\parallel}}
4.285 -\newcommand{\isasymbar}{\isamath{\mid}}
4.286 -\newcommand{\isasymplusminus}{\isamath{\pm}}
4.287 -\newcommand{\isasymminusplus}{\isamath{\mp}}
4.288 -\newcommand{\isasymtimes}{\isamath{\times}}
4.289 -\newcommand{\isasymdiv}{\isamath{\div}}
4.290 -\newcommand{\isasymcdot}{\isamath{\cdot}}
4.291 -\newcommand{\isasymstar}{\isamath{\star}}
4.292 -\newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}}
4.293 -\newcommand{\isasymcirc}{\isamath{\circ}}
4.294 -\newcommand{\isasymdagger}{\isamath{\dagger}}
4.295 -\newcommand{\isasymddagger}{\isamath{\ddagger}}
4.296 -\newcommand{\isasymlhd}{\isamath{\lhd}} %requires amssymb
4.297 -\newcommand{\isasymrhd}{\isamath{\rhd}} %requires amssymb
4.298 -\newcommand{\isasymunlhd}{\isamath{\unlhd}} %requires amssymb
4.299 -\newcommand{\isasymunrhd}{\isamath{\unrhd}} %requires amssymb
4.300 -\newcommand{\isasymtriangleleft}{\isamath{\triangleleft}}
4.301 -\newcommand{\isasymtriangleright}{\isamath{\triangleright}}
4.302 -\newcommand{\isasymtriangle}{\isamath{\triangle}}
4.303 -\newcommand{\isasymtriangleq}{\isamath{\triangleq}} %requires amssymb
4.304 -\newcommand{\isasymoplus}{\isamath{\oplus}}
4.305 -\newcommand{\isasymOplus}{\isamath{\bigoplus\,}}
4.306 -\newcommand{\isasymotimes}{\isamath{\otimes}}
4.307 -\newcommand{\isasymOtimes}{\isamath{\bigotimes\,}}
4.308 -\newcommand{\isasymodot}{\isamath{\odot}}
4.309 -\newcommand{\isasymOdot}{\isamath{\bigodot\,}}
4.310 -\newcommand{\isasymominus}{\isamath{\ominus}}
4.311 -\newcommand{\isasymoslash}{\isamath{\oslash}}
4.312 -\newcommand{\isasymdots}{\isamath{\dots}}
4.313 -\newcommand{\isasymcdots}{\isamath{\cdots}}
4.314 -\newcommand{\isasymSum}{\isamath{\sum\,}}
4.315 -\newcommand{\isasymProd}{\isamath{\prod\,}}
4.316 -\newcommand{\isasymCoprod}{\isamath{\coprod\,}}
4.317 -\newcommand{\isasyminfinity}{\isamath{\infty}}
4.318 -\newcommand{\isasymintegral}{\isamath{\int\,}}
4.319 -\newcommand{\isasymointegral}{\isamath{\oint\,}}
4.320 -\newcommand{\isasymclubsuit}{\isamath{\clubsuit}}
4.321 -\newcommand{\isasymdiamondsuit}{\isamath{\diamondsuit}}
4.322 -\newcommand{\isasymheartsuit}{\isamath{\heartsuit}}
4.323 -\newcommand{\isasymspadesuit}{\isamath{\spadesuit}}
4.324 -\newcommand{\isasymaleph}{\isamath{\aleph}}
4.325 -\newcommand{\isasymemptyset}{\isamath{\emptyset}}
4.326 -\newcommand{\isasymnabla}{\isamath{\nabla}}
4.327 -\newcommand{\isasympartial}{\isamath{\partial}}
4.328 -\newcommand{\isasymRe}{\isamath{\Re}}
4.329 -\newcommand{\isasymIm}{\isamath{\Im}}
4.330 -\newcommand{\isasymflat}{\isamath{\flat}}
4.331 -\newcommand{\isasymnatural}{\isamath{\natural}}
4.332 -\newcommand{\isasymsharp}{\isamath{\sharp}}
4.333 -\newcommand{\isasymangle}{\isamath{\angle}}
4.334 -\newcommand{\isasymcopyright}{\isatext{\normalfont\rmfamily\copyright}}
4.335 -\newcommand{\isasymregistered}{\isatext{\normalfont\rmfamily\textregistered}}
4.336 -\newcommand{\isasyminverse}{\isamath{{}^{-1}}}
4.337 -\newcommand{\isasymonequarter}{\isatext{\normalfont\rmfamily\textonequarter}} %requires textcomp
4.338 -\newcommand{\isasymonehalf}{\isatext{\normalfont\rmfamily\textonehalf}} %requires textcomp
4.339 -\newcommand{\isasymthreequarters}{\isatext{\normalfont\rmfamily\textthreequarters}} %requires textcomp
4.340 -\newcommand{\isasymordfeminine}{\isatext{\normalfont\rmfamily\textordfeminine}}
4.341 -\newcommand{\isasymordmasculine}{\isatext{\normalfont\rmfamily\textordmasculine}}
4.342 -\newcommand{\isasymsection}{\isatext{\normalfont\rmfamily\S}}
4.343 -\newcommand{\isasymparagraph}{\isatext{\normalfont\rmfamily\P}}
4.344 -\newcommand{\isasymexclamdown}{\isatext{\normalfont\rmfamily\textexclamdown}}
4.345 -\newcommand{\isasymquestiondown}{\isatext{\normalfont\rmfamily\textquestiondown}}
4.346 -\newcommand{\isasymeuro}{\isatext{\euro}} %requires eurosym
4.347 -\newcommand{\isasympounds}{\isamath{\pounds}}
4.348 -\newcommand{\isasymyen}{\isatext{\yen}} %requires amssymb
4.349 -\newcommand{\isasymcent}{\isatext{\textcent}} %requires textcomp
4.350 -\newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
4.351 -\newcommand{\isasymdegree}{\isatext{\normalfont\rmfamily\textdegree}} %requires textcomp
4.352 -\newcommand{\isasymhyphen}{\isatext{\normalfont\rmfamily-}}
4.353 -\newcommand{\isasymamalg}{\isamath{\amalg}}
4.354 -\newcommand{\isasymmho}{\isamath{\mho}} %requires amssymb
4.355 -\newcommand{\isasymlozenge}{\isamath{\lozenge}} %requires amssymb
4.356 -\newcommand{\isasymwp}{\isamath{\wp}}
4.357 -\newcommand{\isasymwrong}{\isamath{\wr}}
4.358 -\newcommand{\isasymacute}{\isatext{\'\relax}}
4.359 -\newcommand{\isasymindex}{\isatext{\i}}
4.360 -\newcommand{\isasymdieresis}{\isatext{\"\relax}}
4.361 -\newcommand{\isasymcedilla}{\isatext{\c\relax}}
4.362 -\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
4.363 -\newcommand{\isasymsome}{\isamath{\epsilon\,}}
4.364 -\newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}
4.365 -\newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}}
4.366 -\newcommand{\isasymopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}
4.367 -\newcommand{\isasymclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}
4.368 -\newcommand{\isasymhole}{\isatext{\normalfont\rmfamily\wasylozenge}} %requires wasysym
4.369 -\newcommand{\isasymnewline}{\isatext{\fbox{$\hookleftarrow$}}}
4.370 -\newcommand{\isasymcomment}{\isatext{\isastylecmt---}}
4.371 -\newcommand{\isasymproof}{\isamath{\,\langle\mathit{proof}\rangle}}
4.372 -
4.373 -\newcommand{\isactrlmarker}{\isatext{\ding{48}}} %requires pifont
4.374 -\newcommand{\isactrlassert}{\isakeywordcontrol{assert}}
4.375 -\newcommand{\isactrlcancel}{\isakeywordcontrol{cancel}}
4.376 -\newcommand{\isactrlbinding}{\isakeywordcontrol{binding}}
4.377 -\newcommand{\isactrlclass}{\isakeywordcontrol{class}}
4.378 -\newcommand{\isactrlclassUNDERSCOREsyntax}{\isakeywordcontrol{class{\isacharunderscore}syntax}}
4.379 -\newcommand{\isactrlcommandUNDERSCOREkeyword}{\isakeywordcontrol{command{\isacharunderscore}keyword}}
4.380 -\newcommand{\isactrlconst}{\isakeywordcontrol{const}}
4.381 -\newcommand{\isactrlconstUNDERSCOREabbrev}{\isakeywordcontrol{const{\isacharunderscore}abbrev}}
4.382 -\newcommand{\isactrlconstUNDERSCOREname}{\isakeywordcontrol{const{\isacharunderscore}name}}
4.383 -\newcommand{\isactrlconstUNDERSCOREsyntax}{\isakeywordcontrol{const{\isacharunderscore}syntax}}
4.384 -\newcommand{\isactrlcontext}{\isakeywordcontrol{context}}
4.385 -\newcommand{\isactrlcprop}{\isakeywordcontrol{cprop}}
4.386 -\newcommand{\isactrlcterm}{\isakeywordcontrol{cterm}}
4.387 -\newcommand{\isactrlctyp}{\isakeywordcontrol{ctyp}}
4.388 -\newcommand{\isactrldir}{\isakeywordcontrol{dir}}
4.389 -\newcommand{\isactrlfile}{\isakeywordcontrol{file}}
4.390 -\newcommand{\isactrlhere}{\isakeywordcontrol{here}}
4.391 -\newcommand{\isactrlkeyword}{\isakeywordcontrol{keyword}}
4.392 -\newcommand{\isactrllatex}{\isakeywordcontrol{latex}}
4.393 -\newcommand{\isactrllocale}{\isakeywordcontrol{locale}}
4.394 -\newcommand{\isactrlmakeUNDERSCOREstring}{\isakeywordcontrol{make{\isacharunderscore}string}}
4.395 -\newcommand{\isactrlmasterUNDERSCOREdir}{\isakeywordcontrol{master{\isacharunderscore}dir}}
4.396 -\newcommand{\isactrlmethod}{\isakeywordcontrol{method}}
4.397 -\newcommand{\isactrlnamedUNDERSCOREtheorems}{\isakeywordcontrol{named{\isacharunderscore}theorems}}
4.398 -\newcommand{\isactrlnonterminal}{\isakeywordcontrol{nonterminal}}
4.399 -\newcommand{\isactrlpath}{\isakeywordcontrol{path}}
4.400 -\newcommand{\isactrlpathUNDERSCOREbinding}{\isakeywordcontrol{path{\isacharunderscore}binding}}
4.401 -\newcommand{\isactrlplugin}{\isakeywordcontrol{plugin}}
4.402 -\newcommand{\isactrlprint}{\isakeywordcontrol{print}}
4.403 -\newcommand{\isactrlprop}{\isakeywordcontrol{prop}}
4.404 -\newcommand{\isactrlsimproc}{\isakeywordcontrol{simproc}}
4.405 -\newcommand{\isactrlsort}{\isakeywordcontrol{sort}}
4.406 -\newcommand{\isactrlsyntaxUNDERSCOREconst}{\isakeywordcontrol{syntax{\isacharunderscore}const}}
4.407 -\newcommand{\isactrlsystemUNDERSCOREoption}{\isakeywordcontrol{system{\isacharunderscore}option}}
4.408 -\newcommand{\isactrlterm}{\isakeywordcontrol{term}}
4.409 -\newcommand{\isactrltheory}{\isakeywordcontrol{theory}}
4.410 -\newcommand{\isactrltheoryUNDERSCOREcontext}{\isakeywordcontrol{theory{\isacharunderscore}context}}
4.411 -\newcommand{\isactrltyp}{\isakeywordcontrol{typ}}
4.412 -\newcommand{\isactrltypeUNDERSCOREabbrev}{\isakeywordcontrol{type{\isacharunderscore}abbrev}}
4.413 -\newcommand{\isactrltypeUNDERSCOREname}{\isakeywordcontrol{type{\isacharunderscore}name}}
4.414 -\newcommand{\isactrltypeUNDERSCOREsyntax}{\isakeywordcontrol{type{\isacharunderscore}syntax}}
4.415 -\newcommand{\isactrlundefined}{\isakeywordcontrol{undefined}}
4.416 -
4.417 -\newcommand{\isactrlcode}{\isakeywordcontrol{code}}
4.418 -\newcommand{\isactrlcomputation}{\isakeywordcontrol{computation}}
4.419 -\newcommand{\isactrlcomputationUNDERSCOREconv}{\isakeywordcontrol{computation{\isacharunderscore}conv}}
4.420 -\newcommand{\isactrlcomputationUNDERSCOREcheck}{\isakeywordcontrol{computation{\isacharunderscore}check}}
5.1 --- a/src/Tools/isac/Doc/isabelletags.sty Thu Apr 08 13:09:44 2021 +0200
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,1 +0,0 @@
5.4 -
6.1 --- a/src/Tools/isac/Doc/pdfsetup.sty Thu Apr 08 13:09:44 2021 +0200
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,7 +0,0 @@
6.4 -%%
6.5 -%% default hyperref setup (both for pdf and dvi output)
6.6 -%%
6.7 -
6.8 -\usepackage{color}
6.9 -\definecolor{linkcolor}{rgb}{0,0,0.5}
6.10 -\usepackage[colorlinks=true,linkcolor=linkcolor,citecolor=linkcolor,filecolor=linkcolor,urlcolor=linkcolor,pdfpagelabels]{hyperref}
7.1 --- a/src/Tools/isac/Doc/railsetup.sty Thu Apr 08 13:09:44 2021 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,1202 +0,0 @@
7.4 -% rail.sty - style file to support railroad diagrams
7.5 -%
7.6 -% 09-Jul-90 L. Rooijakkers
7.7 -% 08-Oct-90 L. Rooijakkers fixed centering bug when \rail@tmpc<0.
7.8 -% 07-Feb-91 L. Rooijakkers added \railoptions command, indexing
7.9 -% 08-Feb-91 L. Rooijakkers minor fixes
7.10 -% 28-Jun-94 K. Barthelmann turned into LaTeX2e package
7.11 -% 08-Dec-96 K. Barthelmann replaced \@writefile
7.12 -% 13-Dec-96 K. Barthelmann cleanup
7.13 -% 22-Feb-98 K. Barthelmann fixed catcodes of special characters
7.14 -% 18-Apr-98 K. Barthelmann fixed \par handling
7.15 -% 19-May-98 J. Olsson Added new macros to support arrow heads.
7.16 -% 26-Jul-98 K. Barthelmann changed \par to output newlines
7.17 -% 02-May-11 M. Wenzel default setup for Isabelle
7.18 -%
7.19 -% This style file needs to be used in conjunction with the 'rail'
7.20 -% program. Running LaTeX as 'latex file' produces file.rai, which should be
7.21 -% processed by Rail with 'rail file'. This produces file.rao, which will
7.22 -% be picked up by LaTeX on the next 'latex file' run.
7.23 -%
7.24 -% LaTeX will warn if there is no file.rao or it's out of date.
7.25 -%
7.26 -% The macros in this file thus consist of two parts: those that read and
7.27 -% write the .rai and .rao files, and those that do the actual formatting
7.28 -% of the railroad diagrams.
7.29 -
7.30 -\NeedsTeXFormat{LaTeX2e}
7.31 -\ProvidesPackage{rail}[1998/05/19]
7.32 -
7.33 -% railroad diagram formatting parameters (user level)
7.34 -% all of these are copied into their internal versions by \railinit
7.35 -%
7.36 -% \railunit : \unitlength within railroad diagrams
7.37 -% \railextra : extra length at outside of diagram
7.38 -% \railboxheight : height of ovals and frames
7.39 -% \railboxskip : vertical space between lines
7.40 -% \railboxleft : space to the left of a box
7.41 -% \railboxright : space to the right of a box
7.42 -% \railovalspace : extra space around contents of oval
7.43 -% \railframespace : extra space around contents of frame
7.44 -% \railtextleft : space to the left of text
7.45 -% \railtextright : space to the right of text
7.46 -% \railtextup : space to lift text up
7.47 -% \railjoinsize : circle size of join/split arcs
7.48 -% \railjoinadjust : space to adjust join
7.49 -%
7.50 -% \railnamesep : separator between name and rule body
7.51 -
7.52 -\newlength\railunit
7.53 -\newlength\railextra
7.54 -\newlength\railboxheight
7.55 -\newlength\railboxskip
7.56 -\newlength\railboxleft
7.57 -\newlength\railboxright
7.58 -\newlength\railovalspace
7.59 -\newlength\railframespace
7.60 -\newlength\railtextleft
7.61 -\newlength\railtextright
7.62 -\newlength\railtextup
7.63 -\newlength\railjoinsize
7.64 -\newlength\railjoinadjust
7.65 -\newlength\railnamesep
7.66 -
7.67 -% initialize the parameters
7.68 -
7.69 -\setlength\railunit{1sp}
7.70 -\setlength\railextra{4ex}
7.71 -\setlength\railboxleft{1ex}
7.72 -\setlength\railboxright{1ex}
7.73 -\setlength\railovalspace{2ex}
7.74 -\setlength\railframespace{2ex}
7.75 -\setlength\railtextleft{1ex}
7.76 -\setlength\railtextright{1ex}
7.77 -\setlength\railjoinadjust{0pt}
7.78 -\setlength\railnamesep{1ex}
7.79 -
7.80 -\DeclareOption{10pt}{
7.81 - \setlength\railboxheight{16pt}
7.82 - \setlength\railboxskip{24pt}
7.83 - \setlength\railtextup{5pt}
7.84 - \setlength\railjoinsize{16pt}
7.85 -}
7.86 -\DeclareOption{11pt}{
7.87 - \setlength\railboxheight{16pt}
7.88 - \setlength\railboxskip{24pt}
7.89 - \setlength\railtextup{5pt}
7.90 - \setlength\railjoinsize{16pt}
7.91 -}
7.92 -\DeclareOption{12pt}{
7.93 - \setlength\railboxheight{20pt}
7.94 - \setlength\railboxskip{28pt}
7.95 - \setlength\railtextup{6pt}
7.96 - \setlength\railjoinsize{20pt}
7.97 -}
7.98 -
7.99 -\ExecuteOptions{10pt}
7.100 -\ProcessOptions
7.101 -
7.102 -% internal versions of the formatting parameters
7.103 -%
7.104 -% \rail@extra : \railextra
7.105 -% \rail@boxht : \railboxheight
7.106 -% \rail@boxsp : \railboxskip
7.107 -% \rail@boxlf : \railboxleft
7.108 -% \rail@boxrt : \railboxright
7.109 -% \rail@boxhht : \railboxheight / 2
7.110 -% \rail@ovalsp : \railovalspace
7.111 -% \rail@framesp : \railframespace
7.112 -% \rail@textlf : \railtextleft
7.113 -% \rail@textrt : \railtextright
7.114 -% \rail@textup : \railtextup
7.115 -% \rail@joinsz : \railjoinsize
7.116 -% \rail@joinhsz : \railjoinsize / 2
7.117 -% \rail@joinadj : \railjoinadjust
7.118 -%
7.119 -% \railinit : internalize all of the parameters.
7.120 -
7.121 -\newcount\rail@extra
7.122 -\newcount\rail@boxht
7.123 -\newcount\rail@boxsp
7.124 -\newcount\rail@boxlf
7.125 -\newcount\rail@boxrt
7.126 -\newcount\rail@boxhht
7.127 -\newcount\rail@ovalsp
7.128 -\newcount\rail@framesp
7.129 -\newcount\rail@textlf
7.130 -\newcount\rail@textrt
7.131 -\newcount\rail@textup
7.132 -\newcount\rail@joinsz
7.133 -\newcount\rail@joinhsz
7.134 -\newcount\rail@joinadj
7.135 -
7.136 -\newcommand\railinit{
7.137 -\rail@extra=\railextra
7.138 -\divide\rail@extra by \railunit
7.139 -\rail@boxht=\railboxheight
7.140 -\divide\rail@boxht by \railunit
7.141 -\rail@boxsp=\railboxskip
7.142 -\divide\rail@boxsp by \railunit
7.143 -\rail@boxlf=\railboxleft
7.144 -\divide\rail@boxlf by \railunit
7.145 -\rail@boxrt=\railboxright
7.146 -\divide\rail@boxrt by \railunit
7.147 -\rail@boxhht=\railboxheight
7.148 -\divide\rail@boxhht by \railunit
7.149 -\divide\rail@boxhht by 2
7.150 -\rail@ovalsp=\railovalspace
7.151 -\divide\rail@ovalsp by \railunit
7.152 -\rail@framesp=\railframespace
7.153 -\divide\rail@framesp by \railunit
7.154 -\rail@textlf=\railtextleft
7.155 -\divide\rail@textlf by \railunit
7.156 -\rail@textrt=\railtextright
7.157 -\divide\rail@textrt by \railunit
7.158 -\rail@textup=\railtextup
7.159 -\divide\rail@textup by \railunit
7.160 -\rail@joinsz=\railjoinsize
7.161 -\divide\rail@joinsz by \railunit
7.162 -\rail@joinhsz=\railjoinsize
7.163 -\divide\rail@joinhsz by \railunit
7.164 -\divide\rail@joinhsz by 2
7.165 -\rail@joinadj=\railjoinadjust
7.166 -\divide\rail@joinadj by \railunit
7.167 -}
7.168 -
7.169 -\AtBeginDocument{\railinit}
7.170 -
7.171 -% \rail@param : declarations for list environment
7.172 -%
7.173 -% \railparam{TEXT} : sets \rail@param to TEXT
7.174 -%
7.175 -% \rail@reserved : characters reserved for grammar
7.176 -
7.177 -\newcommand\railparam[1]{
7.178 -\def\rail@param{
7.179 - \setlength\leftmargin{0pt}\setlength\rightmargin{0pt}
7.180 - \setlength\labelwidth{0pt}\setlength\labelsep{0pt}
7.181 - \setlength\itemindent{0pt}\setlength\listparindent{0pt}
7.182 - #1
7.183 -}
7.184 -}
7.185 -\railparam{}
7.186 -
7.187 -\newtoks\rail@reserved
7.188 -\rail@reserved={:;|*+?[]()'"}
7.189 -
7.190 -% \rail@termfont : format setup for terminals
7.191 -%
7.192 -% \rail@nontfont : format setup for nonterminals
7.193 -%
7.194 -% \rail@annofont : format setup for annotations
7.195 -%
7.196 -% \rail@rulefont : format setup for rule names
7.197 -%
7.198 -% \rail@indexfont : format setup for index entry
7.199 -%
7.200 -% \railtermfont{TEXT} : set terminal format setup to TEXT
7.201 -%
7.202 -% \railnontermfont{TEXT} : set nonterminal format setup to TEXT
7.203 -%
7.204 -% \railannotatefont{TEXT} : set annotation format setup to TEXT
7.205 -%
7.206 -% \railnamefont{TEXT} : set rule name format setup to TEXT
7.207 -%
7.208 -% \railindexfont{TEXT} : set index entry format setup to TEXT
7.209 -
7.210 -\def\rail@termfont{\ttfamily\upshape}
7.211 -\def\rail@nontfont{\rmfamily\upshape}
7.212 -\def\rail@annofont{\rmfamily\itshape}
7.213 -\def\rail@namefont{\rmfamily\itshape}
7.214 -\def\rail@indexfont{\rmfamily\itshape}
7.215 -
7.216 -\newcommand\railtermfont[1]{
7.217 -\def\rail@termfont{#1}
7.218 -}
7.219 -
7.220 -\newcommand\railnontermfont[1]{
7.221 -\def\rail@nontfont{#1}
7.222 -}
7.223 -
7.224 -\newcommand\railannotatefont[1]{
7.225 -\def\rail@annofont{#1}
7.226 -}
7.227 -
7.228 -\newcommand\railnamefont[1]{
7.229 -\def\rail@namefont{#1}
7.230 -}
7.231 -
7.232 -\newcommand\railindexfont[1]{
7.233 -\def\rail@indexfont{#1}
7.234 -}
7.235 -
7.236 -% railroad read/write macros
7.237 -%
7.238 -% \begin{rail} TEXT \end{rail} : TEXT is written out to the .rai file,
7.239 -% as \rail@i{NR}{TEXT}. Then the matching
7.240 -% \rail@o{NR}{FMT} from the .rao file is
7.241 -% executed (if defined).
7.242 -%
7.243 -% \railoptions{OPTIONS} : OPTIONS are written out to the .rai file,
7.244 -% as \rail@p{OPTIONS}.
7.245 -%
7.246 -% \railterm{IDENT,IDENT,...} : format IDENT as terminals. writes out
7.247 -% \rail@t{IDENT} to the .rai file
7.248 -%
7.249 -% \railalias{IDENT}{TEXT} : format IDENT as TEXT. defines \rail@t@IDENT as
7.250 -% TEXT.
7.251 -%
7.252 -% \railtoken{IDENT}{TEXT} : abbreviates \railalias{IDENT}{TEXT}\railterm{IDENT}
7.253 -% (for backward compatibility)
7.254 -%
7.255 -% \rail@setcodes : guards special characters
7.256 -%
7.257 -% \rail@makeother{CHARACTER} : sets \catcode of CHARACTER to "other"
7.258 -% used inside a loop for \rail@setcodes
7.259 -%
7.260 -% \rail@nr : railroad diagram counter
7.261 -%
7.262 -% \ifrail@match : current \rail@i{NR}{TEXT} matches
7.263 -%
7.264 -% \rail@first : actions to be done first. read in .rao file,
7.265 -% open .rai file if \@filesw true, undefine \rail@first.
7.266 -% executed from \begin{rail}, \railoptions and \railterm.
7.267 -%
7.268 -% \rail@i{NR}{TEXT} : defines \rail@i@NR as TEXT. written to the .rai
7.269 -% file by \rail, read from the .rao file by
7.270 -% \rail@first
7.271 -%
7.272 -% \rail@t{IDENT} : tells Rail that IDENT is to be custom formatted,
7.273 -% written to the .rai file by \railterm.
7.274 -%
7.275 -% \rail@o{NR}{TEXT} : defines \rail@o@NR as TEXT, read from the .rao
7.276 -% file by \rail@first.
7.277 -%
7.278 -% \rail@p{OPTIONS} : pass options to rail, written to the .rai file by
7.279 -% \railoptions
7.280 -%
7.281 -% \rail@write{TEXT} : write TEXT to the .rai file
7.282 -%
7.283 -% \rail@warn : warn user for mismatching diagrams
7.284 -%
7.285 -% \rail@endwarn : either \relax or \rail@warn
7.286 -%
7.287 -% \ifrail@all : checked at the end of the document
7.288 -
7.289 -\def\rail@makeother#1{
7.290 - \expandafter\catcode\expandafter`\csname\string #1\endcsname=12
7.291 -}
7.292 -
7.293 -\def\rail@setcodes{
7.294 -\let\par=\relax
7.295 -\let\\=\relax
7.296 -\expandafter\@tfor\expandafter\rail@symbol\expandafter:\expandafter=%
7.297 - \the\rail@reserved
7.298 -\do{\expandafter\rail@makeother\rail@symbol}
7.299 -}
7.300 -
7.301 -\newcount\rail@nr
7.302 -
7.303 -\newif\ifrail@all
7.304 -\rail@alltrue
7.305 -
7.306 -\newif\ifrail@match
7.307 -
7.308 -\def\rail@first{
7.309 -\begingroup
7.310 -\makeatletter
7.311 -\rail@setcodes
7.312 -\InputIfFileExists{\jobname.rao}{}{\PackageInfo{rail}{No file \jobname.rao}}
7.313 -\makeatother
7.314 -\endgroup
7.315 -\if@filesw
7.316 -\newwrite\tf@rai
7.317 -\immediate\openout\tf@rai=\jobname.rai
7.318 -\fi
7.319 -\global\let\rail@first=\relax
7.320 -}
7.321 -
7.322 -\long\def\rail@body#1\end{
7.323 -{
7.324 -\newlinechar=`^^J
7.325 -\def\par{\string\par^^J}
7.326 -\rail@write{\string\rail@i{\number\rail@nr}{#1}}
7.327 -}
7.328 -\xdef\rail@i@{#1}
7.329 -\end
7.330 -}
7.331 -
7.332 -\newenvironment{rail}{
7.333 -\global\advance\rail@nr by 1
7.334 -\rail@first
7.335 -\begingroup
7.336 -\rail@setcodes
7.337 -\rail@body
7.338 -}{
7.339 -\endgroup
7.340 -\rail@matchtrue
7.341 -\@ifundefined{rail@o@\number\rail@nr}{\rail@matchfalse}{}
7.342 -\expandafter\ifx\csname rail@i@\number\rail@nr\endcsname\rail@i@
7.343 -\else
7.344 -\rail@matchfalse
7.345 -\fi
7.346 -\ifrail@match
7.347 -\csname rail@o@\number\rail@nr\endcsname
7.348 -\else
7.349 -\PackageWarning{rail}{Railroad diagram {\number\rail@nr} doesn't match}
7.350 -\global\let\rail@endwarn=\rail@warn
7.351 -\begin{list}{}{\rail@param}
7.352 -\rail@begin{1}{}
7.353 -\rail@setbox{\bfseries ???}
7.354 -\rail@oval
7.355 -\rail@end
7.356 -\end{list}
7.357 -\fi
7.358 -}
7.359 -
7.360 -\newcommand\railoptions[1]{
7.361 -\rail@first
7.362 -\rail@write{\string\rail@p{#1}}
7.363 -}
7.364 -
7.365 -\newcommand\railterm[1]{
7.366 -\rail@first
7.367 -\@for\rail@@:=#1\do{
7.368 -\rail@write{\string\rail@t{\rail@@}}
7.369 -}
7.370 -}
7.371 -
7.372 -\newcommand\railalias[2]{
7.373 -\expandafter\def\csname rail@t@#1\endcsname{#2}
7.374 -}
7.375 -
7.376 -\newcommand\railtoken[2]{\railalias{#1}{#2}\railterm{#1}}
7.377 -
7.378 -\long\def\rail@i#1#2{
7.379 -\expandafter\gdef\csname rail@i@#1\endcsname{#2}
7.380 -}
7.381 -
7.382 -\def\rail@o#1#2{
7.383 -\expandafter\gdef\csname rail@o@#1\endcsname{
7.384 -\begin{list}{}{\rail@param}
7.385 -#2
7.386 -\end{list}
7.387 -}
7.388 -}
7.389 -
7.390 -\def\rail@t#1{}
7.391 -
7.392 -\def\rail@p#1{}
7.393 -
7.394 -\long\def\rail@write#1{\@ifundefined{tf@rai}{}{\immediate\write\tf@rai{#1}}}
7.395 -
7.396 -\def\rail@warn{
7.397 -\PackageWarningNoLine{rail}{Railroad diagram(s) may have changed.
7.398 - Use 'rail' and rerun}
7.399 -}
7.400 -
7.401 -\let\rail@endwarn=\relax
7.402 -
7.403 -\AtEndDocument{\rail@endwarn}
7.404 -
7.405 -% index entry macro
7.406 -%
7.407 -% \rail@index{IDENT} : add index entry for IDENT
7.408 -
7.409 -\def\rail@index#1{
7.410 -\index{\rail@indexfont#1}
7.411 -}
7.412 -
7.413 -% railroad formatting primitives
7.414 -%
7.415 -% \rail@x : current x
7.416 -% \rail@y : current y
7.417 -% \rail@ex : current end x
7.418 -% \rail@sx : starting x for \rail@cr
7.419 -% \rail@rx : rightmost previous x for \rail@cr
7.420 -%
7.421 -% \rail@tmpa : temporary count
7.422 -% \rail@tmpb : temporary count
7.423 -% \rail@tmpc : temporary count
7.424 -%
7.425 -% \rail@put : put at (\rail@x,\rail@y)
7.426 -% \rail@vput : put vector at (\rail@x,\rail@y)
7.427 -%
7.428 -% \rail@eline : end line by drawing from \rail@ex to \rail@x
7.429 -%
7.430 -% \rail@vreline : end line by drawing a vector from \rail@x to \rail@ex
7.431 -%
7.432 -% \rail@vleline : end line by drawing a vector from \rail@ex to \rail@x
7.433 -%
7.434 -% \rail@sety{LEVEL} : set \rail@y to level LEVEL
7.435 -
7.436 -\newcount\rail@x
7.437 -\newcount\rail@y
7.438 -\newcount\rail@ex
7.439 -\newcount\rail@sx
7.440 -\newcount\rail@rx
7.441 -
7.442 -\newcount\rail@tmpa
7.443 -\newcount\rail@tmpb
7.444 -\newcount\rail@tmpc
7.445 -
7.446 -\def\rail@put{\put(\number\rail@x,\number\rail@y)}
7.447 -
7.448 -\def\rail@vput{\put(\number\rail@ex,\number\rail@y)}
7.449 -
7.450 -\def\rail@eline{
7.451 -\rail@tmpb=\rail@x
7.452 -\advance\rail@tmpb by -\rail@ex
7.453 -\rail@put{\line(-1,0){\number\rail@tmpb}}
7.454 -}
7.455 -
7.456 -\def\rail@vreline{
7.457 -\rail@tmpb=\rail@x
7.458 -\advance\rail@tmpb by -\rail@ex
7.459 -\rail@vput{\vector(1,0){\number\rail@tmpb}}
7.460 -}
7.461 -
7.462 -\def\rail@vleline{
7.463 -\rail@tmpb=\rail@x
7.464 -\advance\rail@tmpb by -\rail@ex
7.465 -\rail@put{\vector(-1,0){\number\rail@tmpb}}
7.466 -}
7.467 -
7.468 -\def\rail@sety#1{
7.469 -\rail@y=#1
7.470 -\multiply\rail@y by -\rail@boxsp
7.471 -\advance\rail@y by -\rail@boxht
7.472 -}
7.473 -
7.474 -% \rail@begin{HEIGHT}{NAME} : begin a railroad diagram of height HEIGHT
7.475 -%
7.476 -% \rail@end : end a railroad diagram
7.477 -%
7.478 -% \rail@expand{IDENT} : expand IDENT
7.479 -
7.480 -\def\rail@begin#1#2{
7.481 -\item
7.482 -\begin{minipage}[t]{\linewidth}
7.483 -\ifx\@empty#2\else
7.484 -{\rail@namefont \rail@expand{#2}}\\*[\railnamesep]
7.485 -\fi
7.486 -\unitlength=\railunit
7.487 -\rail@tmpa=#1
7.488 -\multiply\rail@tmpa by \rail@boxsp
7.489 -\begin{picture}(0,\number\rail@tmpa)(0,-\number\rail@tmpa)
7.490 -\rail@ex=0
7.491 -\rail@rx=0
7.492 -\rail@x=\rail@extra
7.493 -\rail@sx=\rail@x
7.494 -\rail@sety{0}
7.495 -}
7.496 -
7.497 -\def\rail@end{
7.498 -\advance\rail@x by \rail@extra
7.499 -\rail@eline
7.500 -\end{picture}
7.501 -\end{minipage}
7.502 -}
7.503 -
7.504 -\def\rail@vend{
7.505 -\advance\rail@x by \rail@extra
7.506 -\rail@vreline
7.507 -\end{picture}
7.508 -\end{minipage}
7.509 -}
7.510 -
7.511 -\def\rail@expand#1{\@ifundefined{rail@t@#1}{#1}{\csname rail@t@#1\endcsname}}
7.512 -
7.513 -% \rail@token{TEXT}[ANNOT] : format token TEXT with annotation
7.514 -% \rail@ltoken{TEXT}[ANNOT] : format token TEXT with annotation, arrow left
7.515 -% \rail@rtoken{TEXT}[ANNOT] : format token TEXT with annotation, arrow right
7.516 -%
7.517 -% \rail@ctoken{TEXT}[ANNOT] : format token TEXT centered with annotation
7.518 -% \rail@lctoken{TEXT}[ANNOT] : format token TEXT centered with annotation, arrow left
7.519 -% \rail@rctoken{TEXT}[ANNOT] : format token TEXT centered with annotation, arrow right
7.520 -%
7.521 -% \rail@nont{TEXT}[ANNOT] : format nonterminal TEXT with annotation
7.522 -% \rail@lnont{TEXT}[ANNOT] : format nonterminal TEXT with annotation, arrow left
7.523 -% \rail@rnont{TEXT}[ANNOT] : format nonterminal TEXT with annotation. arrow right
7.524 -%
7.525 -% \rail@cnont{TEXT}[ANNOT] : format nonterminal TEXT centered with annotation
7.526 -% \rail@lcnont{TEXT}[ANNOT] : format nonterminal TEXT centered with annotation,
7.527 -% arrow left
7.528 -% \rail@rcnont{TEXT}[ANNOT] : format nonterminal TEXT centered with annotation,
7.529 -% arrow right
7.530 -%
7.531 -% \rail@term{TEXT}[ANNOT] : format terminal TEXT with annotation
7.532 -% \rail@lterm{TEXT}[ANNOT] : format terminal TEXT with annotation, arrow left
7.533 -% \rail@rterm{TEXT}[ANNOT] : format terminal TEXT with annotation, arrow right
7.534 -%
7.535 -% \rail@cterm{TEXT}[ANNOT] : format terminal TEXT centered with annotation
7.536 -% \rail@lcterm{TEXT}[ANNOT] : format terminal TEXT centered with annotation, arrow left
7.537 -% \rail@rcterm{TEXT}[ANNOT] : format terminal TEXT centered with annotation,
7.538 -% arrow right
7.539 -%
7.540 -% \rail@annote[TEXT] : format TEXT as annotation
7.541 -
7.542 -\def\rail@token#1[#2]{
7.543 -\rail@setbox{%
7.544 -{\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
7.545 -}
7.546 -\rail@oval
7.547 -}
7.548 -
7.549 -\def\rail@ltoken#1[#2]{
7.550 -\rail@setbox{%
7.551 -{\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
7.552 -}
7.553 -\rail@vloval
7.554 -}
7.555 -
7.556 -\def\rail@rtoken#1[#2]{
7.557 -\rail@setbox{%
7.558 -{\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
7.559 -}
7.560 -\rail@vroval
7.561 -}
7.562 -
7.563 -\def\rail@ctoken#1[#2]{
7.564 -\rail@setbox{%
7.565 -{\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
7.566 -}
7.567 -\rail@coval
7.568 -}
7.569 -
7.570 -\def\rail@lctoken#1[#2]{
7.571 -\rail@setbox{%
7.572 -{\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
7.573 -}
7.574 -\rail@vlcoval
7.575 -}
7.576 -
7.577 -\def\rail@rctoken#1[#2]{
7.578 -\rail@setbox{%
7.579 -{\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
7.580 -}
7.581 -\rail@vrcoval
7.582 -}
7.583 -
7.584 -\def\rail@nont#1[#2]{
7.585 -\rail@setbox{%
7.586 -{\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
7.587 -}
7.588 -\rail@frame
7.589 -}
7.590 -
7.591 -\def\rail@lnont#1[#2]{
7.592 -\rail@setbox{%
7.593 -{\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
7.594 -}
7.595 -\rail@vlframe
7.596 -}
7.597 -
7.598 -\def\rail@rnont#1[#2]{
7.599 -\rail@setbox{%
7.600 -{\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
7.601 -}
7.602 -\rail@vrframe
7.603 -}
7.604 -
7.605 -\def\rail@cnont#1[#2]{
7.606 -\rail@setbox{%
7.607 -{\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
7.608 -}
7.609 -\rail@cframe
7.610 -}
7.611 -
7.612 -\def\rail@lcnont#1[#2]{
7.613 -\rail@setbox{%
7.614 -{\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
7.615 -}
7.616 -\rail@vlcframe
7.617 -}
7.618 -
7.619 -\def\rail@rcnont#1[#2]{
7.620 -\rail@setbox{%
7.621 -{\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
7.622 -}
7.623 -\rail@vrcframe
7.624 -}
7.625 -
7.626 -\def\rail@term#1[#2]{
7.627 -\rail@setbox{%
7.628 -{\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
7.629 -}
7.630 -\rail@oval
7.631 -}
7.632 -
7.633 -\def\rail@lterm#1[#2]{
7.634 -\rail@setbox{%
7.635 -{\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
7.636 -}
7.637 -\rail@vloval
7.638 -}
7.639 -
7.640 -\def\rail@rterm#1[#2]{
7.641 -\rail@setbox{%
7.642 -{\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
7.643 -}
7.644 -\rail@vroval
7.645 -}
7.646 -
7.647 -\def\rail@cterm#1[#2]{
7.648 -\rail@setbox{%
7.649 -{\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
7.650 -}
7.651 -\rail@coval
7.652 -}
7.653 -
7.654 -\def\rail@lcterm#1[#2]{
7.655 -\rail@setbox{%
7.656 -{\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
7.657 -}
7.658 -\rail@vlcoval
7.659 -}
7.660 -
7.661 -\def\rail@rcterm#1[#2]{
7.662 -\rail@setbox{%
7.663 -{\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi
7.664 -}
7.665 -\rail@vrcoval
7.666 -}
7.667 -
7.668 -\def\rail@annote[#1]{
7.669 -\rail@setbox{\rail@annofont #1}
7.670 -\rail@text
7.671 -}
7.672 -
7.673 -% \rail@box : temporary box for \rail@oval and \rail@frame
7.674 -%
7.675 -% \rail@setbox{TEXT} : set \rail@box to TEXT, set \rail@tmpa to width
7.676 -%
7.677 -% \rail@oval : format \rail@box of width \rail@tmpa inside an oval
7.678 -% \rail@vloval : format \rail@box of width \rail@tmpa inside an oval, vector left
7.679 -% \rail@vroval : format \rail@box of width \rail@tmpa inside an oval, vector right
7.680 -%
7.681 -% \rail@coval : same as \rail@oval, but centered between \rail@x and
7.682 -% \rail@mx
7.683 -% \rail@vlcoval : same as \rail@oval, but centered between \rail@x and
7.684 -% \rail@mx, vector left
7.685 -% \rail@vrcoval : same as \rail@oval, but centered between \rail@x and
7.686 -% \rail@mx, vector right
7.687 -%
7.688 -% \rail@frame : format \rail@box of width \rail@tmpa inside a frame
7.689 -% \rail@vlframe : format \rail@box of width \rail@tmpa inside a frame, vector left
7.690 -% \rail@vrframe : format \rail@box of width \rail@tmpa inside a frame, vector right
7.691 -%
7.692 -% \rail@cframe : same as \rail@frame, but centered between \rail@x and
7.693 -% \rail@mx
7.694 -% \rail@vlcframe : same as \rail@frame, but centered between \rail@x and
7.695 -% \rail@mx, vector left
7.696 -% \rail@vrcframe : same as \rail@frame, but centered between \rail@x and
7.697 -% \rail@mx, vector right
7.698 -%
7.699 -% \rail@text : format \rail@box of width \rail@tmpa above the line
7.700 -
7.701 -\newbox\rail@box
7.702 -
7.703 -\def\rail@setbox#1{
7.704 -\setbox\rail@box\hbox{\strut#1}
7.705 -\rail@tmpa=\wd\rail@box
7.706 -\divide\rail@tmpa by \railunit
7.707 -}
7.708 -
7.709 -\def\rail@oval{
7.710 -\advance\rail@x by \rail@boxlf
7.711 -\rail@eline
7.712 -\advance\rail@tmpa by \rail@ovalsp
7.713 -\ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi
7.714 -\rail@tmpb=\rail@tmpa
7.715 -\divide\rail@tmpb by 2
7.716 -\advance\rail@y by -\rail@boxhht
7.717 -\rail@put{\makebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}}
7.718 -\advance\rail@y by \rail@boxhht
7.719 -\advance\rail@x by \rail@tmpb
7.720 -\rail@put{\oval(\number\rail@tmpa,\number\rail@boxht)}
7.721 -\advance\rail@x by \rail@tmpb
7.722 -\rail@ex=\rail@x
7.723 -\advance\rail@x by \rail@boxrt
7.724 -}
7.725 -
7.726 -\def\rail@vloval{
7.727 -\advance\rail@x by \rail@boxlf
7.728 -\rail@eline
7.729 -\advance\rail@tmpa by \rail@ovalsp
7.730 -\ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi
7.731 -\rail@tmpb=\rail@tmpa
7.732 -\divide\rail@tmpb by 2
7.733 -\advance\rail@y by -\rail@boxhht
7.734 -\rail@put{\makebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}}
7.735 -\advance\rail@y by \rail@boxhht
7.736 -\advance\rail@x by \rail@tmpb
7.737 -\rail@put{\oval(\number\rail@tmpa,\number\rail@boxht)}
7.738 -\advance\rail@x by \rail@tmpb
7.739 -\rail@ex=\rail@x
7.740 -\advance\rail@x by \rail@boxrt
7.741 -\rail@vleline
7.742 -}
7.743 -
7.744 -\def\rail@vroval{
7.745 -\advance\rail@x by \rail@boxlf
7.746 -\rail@vreline
7.747 -\advance\rail@tmpa by \rail@ovalsp
7.748 -\ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi
7.749 -\rail@tmpb=\rail@tmpa
7.750 -\divide\rail@tmpb by 2
7.751 -\advance\rail@y by -\rail@boxhht
7.752 -\rail@put{\makebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}}
7.753 -\advance\rail@y by \rail@boxhht
7.754 -\advance\rail@x by \rail@tmpb
7.755 -\rail@put{\oval(\number\rail@tmpa,\number\rail@boxht)}
7.756 -\advance\rail@x by \rail@tmpb
7.757 -\rail@ex=\rail@x
7.758 -\advance\rail@x by \rail@boxrt
7.759 -}
7.760 -
7.761 -\def\rail@coval{
7.762 -\rail@tmpb=\rail@tmpa
7.763 -\advance\rail@tmpb by \rail@ovalsp
7.764 -\ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi
7.765 -\advance\rail@tmpb by \rail@boxlf
7.766 -\advance\rail@tmpb by \rail@boxrt
7.767 -\rail@tmpc=\rail@mx
7.768 -\advance\rail@tmpc by -\rail@x
7.769 -\advance\rail@tmpc by -\rail@tmpb
7.770 -\divide\rail@tmpc by 2
7.771 -\ifnum\rail@tmpc>0
7.772 -\advance\rail@x by \rail@tmpc
7.773 -\fi
7.774 -\rail@oval
7.775 -}
7.776 -
7.777 -\def\rail@vlcoval{
7.778 -\rail@tmpb=\rail@tmpa
7.779 -\advance\rail@tmpb by \rail@ovalsp
7.780 -\ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi
7.781 -\advance\rail@tmpb by \rail@boxlf
7.782 -\advance\rail@tmpb by \rail@boxrt
7.783 -\rail@tmpc=\rail@mx
7.784 -\advance\rail@tmpc by -\rail@x
7.785 -\advance\rail@tmpc by -\rail@tmpb
7.786 -\divide\rail@tmpc by 2
7.787 -\ifnum\rail@tmpc>0
7.788 -\advance\rail@x by \rail@tmpc
7.789 -\fi
7.790 -\rail@vloval
7.791 -}
7.792 -
7.793 -\def\rail@vrcoval{
7.794 -\rail@tmpb=\rail@tmpa
7.795 -\advance\rail@tmpb by \rail@ovalsp
7.796 -\ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi
7.797 -\advance\rail@tmpb by \rail@boxlf
7.798 -\advance\rail@tmpb by \rail@boxrt
7.799 -\rail@tmpc=\rail@mx
7.800 -\advance\rail@tmpc by -\rail@x
7.801 -\advance\rail@tmpc by -\rail@tmpb
7.802 -\divide\rail@tmpc by 2
7.803 -\ifnum\rail@tmpc>0
7.804 -\advance\rail@x by \rail@tmpc
7.805 -\fi
7.806 -\rail@vroval
7.807 -}
7.808 -
7.809 -\def\rail@frame{
7.810 -\advance\rail@x by \rail@boxlf
7.811 -\rail@eline
7.812 -\advance\rail@tmpa by \rail@framesp
7.813 -\ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi
7.814 -\advance\rail@y by -\rail@boxhht
7.815 -\rail@put{\framebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}}
7.816 -\advance\rail@y by \rail@boxhht
7.817 -\advance\rail@x by \rail@tmpa
7.818 -\rail@ex=\rail@x
7.819 -\advance\rail@x by \rail@boxrt
7.820 -}
7.821 -
7.822 -\def\rail@vlframe{
7.823 -\advance\rail@x by \rail@boxlf
7.824 -\rail@eline
7.825 -\advance\rail@tmpa by \rail@framesp
7.826 -\ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi
7.827 -\advance\rail@y by -\rail@boxhht
7.828 -\rail@put{\framebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}}
7.829 -\advance\rail@y by \rail@boxhht
7.830 -\advance\rail@x by \rail@tmpa
7.831 -\rail@ex=\rail@x
7.832 -\advance\rail@x by \rail@boxrt
7.833 -\rail@vleline
7.834 -}
7.835 -
7.836 -\def\rail@vrframe{
7.837 -\advance\rail@x by \rail@boxlf
7.838 -\rail@vreline
7.839 -\advance\rail@tmpa by \rail@framesp
7.840 -\ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi
7.841 -\advance\rail@y by -\rail@boxhht
7.842 -\rail@put{\framebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}}
7.843 -\advance\rail@y by \rail@boxhht
7.844 -\advance\rail@x by \rail@tmpa
7.845 -\rail@ex=\rail@x
7.846 -\advance\rail@x by \rail@boxrt
7.847 -}
7.848 -
7.849 -\def\rail@cframe{
7.850 -\rail@tmpb=\rail@tmpa
7.851 -\advance\rail@tmpb by \rail@framesp
7.852 -\ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi
7.853 -\advance\rail@tmpb by \rail@boxlf
7.854 -\advance\rail@tmpb by \rail@boxrt
7.855 -\rail@tmpc=\rail@mx
7.856 -\advance\rail@tmpc by -\rail@x
7.857 -\advance\rail@tmpc by -\rail@tmpb
7.858 -\divide\rail@tmpc by 2
7.859 -\ifnum\rail@tmpc>0
7.860 -\advance\rail@x by \rail@tmpc
7.861 -\fi
7.862 -\rail@frame
7.863 -}
7.864 -
7.865 -\def\rail@vlcframe{
7.866 -\rail@tmpb=\rail@tmpa
7.867 -\advance\rail@tmpb by \rail@framesp
7.868 -\ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi
7.869 -\advance\rail@tmpb by \rail@boxlf
7.870 -\advance\rail@tmpb by \rail@boxrt
7.871 -\rail@tmpc=\rail@mx
7.872 -\advance\rail@tmpc by -\rail@x
7.873 -\advance\rail@tmpc by -\rail@tmpb
7.874 -\divide\rail@tmpc by 2
7.875 -\ifnum\rail@tmpc>0
7.876 -\advance\rail@x by \rail@tmpc
7.877 -\fi
7.878 -\rail@vlframe
7.879 -}
7.880 -
7.881 -\def\rail@vrcframe{
7.882 -\rail@tmpb=\rail@tmpa
7.883 -\advance\rail@tmpb by \rail@framesp
7.884 -\ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi
7.885 -\advance\rail@tmpb by \rail@boxlf
7.886 -\advance\rail@tmpb by \rail@boxrt
7.887 -\rail@tmpc=\rail@mx
7.888 -\advance\rail@tmpc by -\rail@x
7.889 -\advance\rail@tmpc by -\rail@tmpb
7.890 -\divide\rail@tmpc by 2
7.891 -\ifnum\rail@tmpc>0
7.892 -\advance\rail@x by \rail@tmpc
7.893 -\fi
7.894 -\rail@vrframe
7.895 -}
7.896 -
7.897 -\def\rail@text{
7.898 -\advance\rail@x by \rail@textlf
7.899 -\advance\rail@y by \rail@textup
7.900 -\rail@put{\box\rail@box}
7.901 -\advance\rail@y by -\rail@textup
7.902 -\advance\rail@x by \rail@tmpa
7.903 -\advance\rail@x by \rail@textrt
7.904 -}
7.905 -
7.906 -% alternatives
7.907 -%
7.908 -% \rail@jx \rail@jy : current join point
7.909 -%
7.910 -% \rail@gx \rail@gy \rail@gex \rail@grx : global versions of \rail@x etc,
7.911 -% to pass values over group closings
7.912 -%
7.913 -% \rail@mx : maximum x so far
7.914 -%
7.915 -% \rail@sy : starting \rail@y for alternatives
7.916 -%
7.917 -% \rail@jput : put at (\rail@jx,\rail@jy)
7.918 -%
7.919 -% \rail@joval[PART] : put \oval[PART] with adjust
7.920 -
7.921 -\newcount\rail@jx
7.922 -\newcount\rail@jy
7.923 -
7.924 -\newcount\rail@gx
7.925 -\newcount\rail@gy
7.926 -\newcount\rail@gex
7.927 -\newcount\rail@grx
7.928 -
7.929 -\newcount\rail@sy
7.930 -\newcount\rail@mx
7.931 -
7.932 -\def\rail@jput{
7.933 -\put(\number\rail@jx,\number\rail@jy)
7.934 -}
7.935 -
7.936 -\def\rail@joval[#1]{
7.937 -\advance\rail@jx by \rail@joinadj
7.938 -\rail@jput{\oval(\number\rail@joinsz,\number\rail@joinsz)[#1]}
7.939 -\advance\rail@jx by -\rail@joinadj
7.940 -}
7.941 -
7.942 -% \rail@barsplit : incoming split for '|'
7.943 -%
7.944 -% \rail@plussplit : incoming split for '+'
7.945 -%
7.946 -
7.947 -\def\rail@barsplit{
7.948 -\advance\rail@jy by -\rail@joinhsz
7.949 -\rail@joval[tr]
7.950 -\advance\rail@jx by \rail@joinhsz
7.951 -}
7.952 -
7.953 -\def\rail@plussplit{
7.954 -\advance\rail@jy by -\rail@joinhsz
7.955 -\advance\rail@jx by \rail@joinsz
7.956 -\rail@joval[tl]
7.957 -\advance\rail@jx by -\rail@joinhsz
7.958 -}
7.959 -
7.960 -% \rail@alt{SPLIT} : start alternatives with incoming split SPLIT
7.961 -%
7.962 -
7.963 -\def\rail@alt#1{
7.964 -\rail@sy=\rail@y
7.965 -\rail@jx=\rail@x
7.966 -\rail@jy=\rail@y
7.967 -\advance\rail@x by \rail@joinsz
7.968 -\rail@mx=0
7.969 -\let\rail@list=\@empty
7.970 -\let\rail@comma=\@empty
7.971 -\let\rail@split=#1
7.972 -\begingroup
7.973 -\rail@sx=\rail@x
7.974 -\rail@rx=0
7.975 -}
7.976 -
7.977 -% \rail@nextalt{FIX}{Y} : start next alternative at vertical position Y
7.978 -% and fix-up FIX
7.979 -%
7.980 -
7.981 -\def\rail@nextalt#1#2{
7.982 -\global\rail@gx=\rail@x
7.983 -\global\rail@gy=\rail@y
7.984 -\global\rail@gex=\rail@ex
7.985 -\global\rail@grx=\rail@rx
7.986 -\endgroup
7.987 -#1
7.988 -\ifnum\rail@gx>\rail@mx\rail@mx=\rail@gx\fi
7.989 -\ifnum\rail@grx>\rail@mx\rail@mx=\rail@grx\fi
7.990 -\edef\rail@list{\rail@list\rail@comma\number\rail@gex:\number\rail@gy}
7.991 -\def\rail@comma{,}
7.992 -\rail@split
7.993 -\let\rail@split=\@empty
7.994 -\rail@sety{#2}
7.995 -\rail@tmpa=\rail@jy
7.996 -\advance\rail@tmpa by -\rail@y
7.997 -\advance\rail@tmpa by -\rail@joinhsz
7.998 -\rail@jput{\line(0,-1){\number\rail@tmpa}}
7.999 -\rail@jy=\rail@y
7.1000 -\advance\rail@jy by \rail@joinhsz
7.1001 -\advance\rail@jx by \rail@joinhsz
7.1002 -\rail@joval[bl]
7.1003 -\advance\rail@jx by -\rail@joinhsz
7.1004 -\rail@ex=\rail@x
7.1005 -\begingroup
7.1006 -\rail@sx=\rail@x
7.1007 -\rail@rx=0
7.1008 -}
7.1009 -
7.1010 -% \rail@barjoin : outgoing join for first '|' alternative
7.1011 -%
7.1012 -% \rail@plusjoin : outgoing join for first '+' alternative
7.1013 -%
7.1014 -% \rail@altjoin : join for subsequent alternative
7.1015 -%
7.1016 -
7.1017 -\def\rail@barjoin{
7.1018 -\ifnum\rail@y<\rail@sy
7.1019 -\global\rail@gex=\rail@jx
7.1020 -\else
7.1021 -\global\rail@gex=\rail@ex
7.1022 -\fi
7.1023 -\advance\rail@jy by -\rail@joinhsz
7.1024 -\rail@joval[tl]
7.1025 -\advance\rail@jx by -\rail@joinhsz
7.1026 -\ifnum\rail@y<\rail@sy
7.1027 -\rail@altjoin
7.1028 -\fi
7.1029 -}
7.1030 -
7.1031 -\def\rail@plusjoin{
7.1032 -\global\rail@gex=\rail@ex
7.1033 -\advance\rail@jy by -\rail@joinhsz
7.1034 -\advance\rail@jx by -\rail@joinsz
7.1035 -\rail@joval[tr]
7.1036 -\advance\rail@jx by \rail@joinhsz
7.1037 -}
7.1038 -
7.1039 -\def\rail@altjoin{
7.1040 -\rail@eline
7.1041 -\rail@tmpa=\rail@jy
7.1042 -\advance\rail@tmpa by -\rail@y
7.1043 -\advance\rail@tmpa by -\rail@joinhsz
7.1044 -\rail@jput{\line(0,-1){\number\rail@tmpa}}
7.1045 -\rail@jy=\rail@y
7.1046 -\advance\rail@jy by \rail@joinhsz
7.1047 -\advance\rail@jx by -\rail@joinhsz
7.1048 -\rail@joval[br]
7.1049 -\advance\rail@jx by \rail@joinhsz
7.1050 -}
7.1051 -
7.1052 -% \rail@eltsplit EX:Y; : split EX:Y into \rail@ex \rail@y
7.1053 -%
7.1054 -% \rail@endalt{JOIN} : end alternatives with outgoing join JOIN
7.1055 -
7.1056 -\def\rail@eltsplit#1:#2;{\rail@ex=#1\rail@y=#2}
7.1057 -
7.1058 -\def\rail@endalt#1{
7.1059 -\global\rail@gx=\rail@x
7.1060 -\global\rail@gy=\rail@y
7.1061 -\global\rail@gex=\rail@ex
7.1062 -\global\rail@grx=\rail@rx
7.1063 -\endgroup
7.1064 -\ifnum\rail@gx>\rail@mx\rail@mx=\rail@gx\fi
7.1065 -\ifnum\rail@grx>\rail@mx\rail@mx=\rail@grx\fi
7.1066 -\edef\rail@list{\rail@list\rail@comma\number\rail@gex:\number\rail@gy}
7.1067 -\rail@x=\rail@mx
7.1068 -\rail@jx=\rail@x
7.1069 -\rail@jy=\rail@sy
7.1070 -\advance\rail@jx by \rail@joinsz
7.1071 -\let\rail@join=#1
7.1072 -\@for\rail@elt:=\rail@list\do{
7.1073 -\expandafter\rail@eltsplit\rail@elt;
7.1074 -\rail@join
7.1075 -\let\rail@join=\rail@altjoin
7.1076 -}
7.1077 -\rail@x=\rail@mx
7.1078 -\rail@y=\rail@sy
7.1079 -\rail@ex=\rail@gex
7.1080 -\advance\rail@x by \rail@joinsz
7.1081 -}
7.1082 -
7.1083 -% \rail@bar : start '|' alternatives
7.1084 -%
7.1085 -% \rail@nextbar : next '|' alternative
7.1086 -%
7.1087 -% \rail@endbar : end '|' alternatives
7.1088 -%
7.1089 -
7.1090 -\def\rail@bar{
7.1091 -\rail@alt\rail@barsplit
7.1092 -}
7.1093 -
7.1094 -\def\rail@nextbar{
7.1095 -\rail@nextalt\relax
7.1096 -}
7.1097 -
7.1098 -\def\rail@endbar{
7.1099 -\rail@endalt\rail@barjoin
7.1100 -}
7.1101 -
7.1102 -% \rail@plus : start '+' alternatives
7.1103 -%
7.1104 -% \rail@nextplus: next '+' alternative
7.1105 -%
7.1106 -% \rail@endplus : end '+' alternatives
7.1107 -%
7.1108 -
7.1109 -\def\rail@plus{
7.1110 -\rail@alt\rail@plussplit
7.1111 -}
7.1112 -
7.1113 -\def\rail@nextplus{
7.1114 -\rail@nextalt\rail@fixplus
7.1115 -}
7.1116 -
7.1117 -\def\rail@fixplus{
7.1118 -\ifnum\rail@gy<\rail@sy
7.1119 -\begingroup
7.1120 -\rail@x=\rail@gx
7.1121 -\rail@y=\rail@gy
7.1122 -\rail@ex=\rail@gex
7.1123 -\rail@rx=\rail@grx
7.1124 -\ifnum\rail@x<\rail@rx
7.1125 -\rail@x=\rail@rx
7.1126 -\fi
7.1127 -\rail@eline
7.1128 -\rail@jx=\rail@x
7.1129 -\rail@jy=\rail@y
7.1130 -\advance\rail@jy by \rail@joinhsz
7.1131 -\rail@joval[br]
7.1132 -\advance\rail@jx by \rail@joinhsz
7.1133 -\rail@tmpa=\rail@sy
7.1134 -\advance\rail@tmpa by -\rail@joinhsz
7.1135 -\advance\rail@tmpa by -\rail@jy
7.1136 -\rail@jput{\line(0,1){\number\rail@tmpa}}
7.1137 -\rail@jy=\rail@sy
7.1138 -\advance\rail@jy by -\rail@joinhsz
7.1139 -\advance\rail@jx by \rail@joinhsz
7.1140 -\rail@joval[tl]
7.1141 -\advance\rail@jy by \rail@joinhsz
7.1142 -\global\rail@gx=\rail@jx
7.1143 -\global\rail@gy=\rail@jy
7.1144 -\global\rail@gex=\rail@gx
7.1145 -\global\rail@grx=\rail@rx
7.1146 -\endgroup
7.1147 -\fi
7.1148 -}
7.1149 -
7.1150 -\def\rail@endplus{
7.1151 -\rail@endalt\rail@plusjoin
7.1152 -}
7.1153 -
7.1154 -% \rail@cr{Y} : carriage return to vertical position Y
7.1155 -
7.1156 -\def\rail@cr#1{
7.1157 -\rail@tmpa=\rail@sx
7.1158 -\advance\rail@tmpa by \rail@joinsz
7.1159 -\ifnum\rail@x<\rail@tmpa\rail@x=\rail@tmpa\fi
7.1160 -\rail@eline
7.1161 -\rail@jx=\rail@x
7.1162 -\rail@jy=\rail@y
7.1163 -\advance\rail@x by \rail@joinsz
7.1164 -\ifnum\rail@x>\rail@rx\rail@rx=\rail@x\fi
7.1165 -\advance\rail@jy by -\rail@joinhsz
7.1166 -\rail@joval[tr]
7.1167 -\advance\rail@jx by \rail@joinhsz
7.1168 -\rail@sety{#1}
7.1169 -\rail@tmpa=\rail@jy
7.1170 -\advance\rail@tmpa by -\rail@y
7.1171 -\advance\rail@tmpa by -\rail@boxsp
7.1172 -\advance\rail@tmpa by -\rail@joinhsz
7.1173 -\rail@jput{\line(0,-1){\number\rail@tmpa}}
7.1174 -\rail@jy=\rail@y
7.1175 -\advance\rail@jy by \rail@boxsp
7.1176 -\advance\rail@jy by \rail@joinhsz
7.1177 -\advance\rail@jx by -\rail@joinhsz
7.1178 -\rail@joval[br]
7.1179 -\advance\rail@jy by -\rail@joinhsz
7.1180 -\rail@tmpa=\rail@jx
7.1181 -\advance\rail@tmpa by -\rail@sx
7.1182 -\advance\rail@tmpa by -\rail@joinhsz
7.1183 -\rail@jput{\line(-1,0){\number\rail@tmpa}}
7.1184 -\rail@jx=\rail@sx
7.1185 -\advance\rail@jx by \rail@joinhsz
7.1186 -\advance\rail@jy by -\rail@joinhsz
7.1187 -\rail@joval[tl]
7.1188 -\advance\rail@jx by -\rail@joinhsz
7.1189 -\rail@tmpa=\rail@boxsp
7.1190 -\advance\rail@tmpa by -\rail@joinsz
7.1191 -\rail@jput{\line(0,-1){\number\rail@tmpa}}
7.1192 -\advance\rail@jy by -\rail@tmpa
7.1193 -\advance\rail@jx by \rail@joinhsz
7.1194 -\rail@joval[bl]
7.1195 -\rail@x=\rail@jx
7.1196 -\rail@ex=\rail@x
7.1197 -}
7.1198 -
7.1199 -% default setup for Isabelle
7.1200 -\newenvironment{railoutput}%
7.1201 -{\begin{list}{}{\rail@param}\def\rail@expand{\relax}\makeatletter}{\makeatother\end{list}}
7.1202 -
7.1203 -\def\rail@termfont{\isabellestyle{tt}}
7.1204 -\def\rail@nontfont{\isabellestyle{it}}
7.1205 -\def\rail@namefont{\isabellestyle{it}}