avoid odd clones of Isabelle latex styles:
authorwenzelm
Thu, 08 Apr 2021 13:27:27 +0200
changeset 60188422186a35be8
parent 60187 751b8a13c271
child 60189 6b021e8cb8da
avoid odd clones of Isabelle latex styles:
these diverge over time, when the originals in $ISABELLE_HOME/lib/texinputs change;
src/Tools/isac/Doc/ROOT
src/Tools/isac/Doc/comment.sty
src/Tools/isac/Doc/isabelle.sty
src/Tools/isac/Doc/isabellesym.sty
src/Tools/isac/Doc/isabelletags.sty
src/Tools/isac/Doc/pdfsetup.sty
src/Tools/isac/Doc/railsetup.sty
     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}}