path: root/macros/latex/contrib/semantic/semantic.dtx

% \RCS$Revision: 1.11 $
% \RCS$Date: 2003/10/28 13:45:57 $
%
%\iffalse metacomment
% 
%%
%% semantic.dtx  (c)1995--2002 Peter Møller Neergaard and 
%%                             Arne John Glenstrup
%%
%
% This program may be distributed and/or modified under the
% conditions of the LaTeX Project Public License, either version 1.2
% of this license or (at your option) any later version.
% The latest version of this license is in
%   http://www.latex-project.org/lppl.txt
% and version 1.2 or later is part of all distributions of LaTeX 
% version 1999/12/01 or later.
%
% This program consists of the files semantic.dtx and semantic.ins
%
% This file is the source code containing the package.  
%
% You install the package by running tex on semantic.ins, i.e.,
% 
%   tex semantic.ins
%
%\fi
% \DeleteShortVerb{\|}
% \CheckSum{1918}
% \CharacterTable
%  {Upper-case    \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z
%   Lower-case    \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z
%   Digits        \0\1\2\3\4\5\6\7\8\9
%   Exclamation   \!     Double quote  \"     Hash (number) \#
%   Dollar        \$     Percent       \%     Ampersand     \&
%   Acute accent  \'     Left paren    \(     Right paren   \)
%   Asterisk      \*     Plus          \+     Comma         \,
%   Minus         \-     Point         \.     Solidus       \/
%   Colon         \:     Semicolon     \;     Less than     \<
%   Equals        \=     Greater than  \>     Question mark \?
%   Commercial at \@     Left bracket  \[     Backslash     \\
%   Right bracket \]     Circumflex    \^     Underscore    \_
%   Grave accent  \`     Left brace    \{     Vertical bar  \|
%   Right brace   \}     Tilde         \~}
%
% ^^A I do not want the LaTeX-commands in the index
% ^^A This is borrowed from the standard package ``doc.dtx'' 
% \DoNotIndex{\@,\@@par,\@beginparpenalty,\@empty}
% \DoNotIndex{\@flushglue,\@gobble,\@input}
% \DoNotIndex{\@makefnmark,\@makeother,\@maketitle}
% \DoNotIndex{\@namedef,\@ne,\@spaces,\@tempa}
% \DoNotIndex{\@tempb,\@tempswafalse,\@tempswatrue}
% \DoNotIndex{\@thanks,\@thefnmark,\@topnum}
% \DoNotIndex{\@@,\@elt,\@forloop,\@fortmp,\@gtempa,\@totalleftmargin}
% \DoNotIndex{\",\/,\@ifundefined,\@nil,\@verbatim,\@vobeyspaces}
% \DoNotIndex{\|,\~,\ ,\active,\advance,\aftergroup,\begingroup,\bgroup}
% \DoNotIndex{\mathcal,\csname,\def,\documentstyle,\dospecials,\edef}
% \DoNotIndex{\egroup}
% \DoNotIndex{\else,\endcsname,\endgroup,\endinput,\endtrivlist}
% \DoNotIndex{\expandafter,\fi,\fnsymbol,\futurelet,\gdef,\global}
% \DoNotIndex{\hbox,\hss,\if,\if@inlabel,\if@tempswa,\if@twocolumn}
% \DoNotIndex{\ifcase}
% \DoNotIndex{\ifcat,\iffalse,\ifx,\ignorespaces,\index,\input,\item}
% \DoNotIndex{\jobname,\kern,\leavevmode,\leftskip,\let,\llap,\lower}
% \DoNotIndex{\m@ne,\next,\newpage,\nobreak,\noexpand,\nonfrenchspacing}
% \DoNotIndex{\obeylines,\or,\protect,\raggedleft,\rightskip,\rm,\sc}
% \DoNotIndex{\setbox,\setcounter,\small,\space,\string,\strut}
% \DoNotIndex{\strutbox}
% \DoNotIndex{\thefootnote,\thispagestyle,\topmargin,\trivlist,\tt}
% \DoNotIndex{\twocolumn,\typeout,\vss,\vtop,\xdef,\z@}
% \DoNotIndex{\,,\@bsphack,\@esphack,\@noligs,\@vobeyspaces,\@xverbatim}
% \DoNotIndex{\`,\catcode,\end,\escapechar,\frenchspacing,\glossary}
% \DoNotIndex{\hangindent,\hfil,\hfill,\hskip,\hspace,\ht,\it,\langle}
% \DoNotIndex{\leaders,\long,\makelabel,\marginpar,\markboth,\mathcode}
% \DoNotIndex{\mathsurround,\mbox,\newcount,\newdimen,\newskip}
% \DoNotIndex{\nopagebreak}
% \DoNotIndex{\parfillskip,\parindent,\parskip,\penalty,\raise,\rangle}
% \DoNotIndex{\section,\setlength,\TeX,\topsep,\underline,\unskip,\verb}
% \DoNotIndex{\vskip,\vspace,\widetilde,\\,\%,\@date,\@defpar}
% \DoNotIndex{\[,\{,\},\]}
% \DoNotIndex{\count@,\ifnum,\loop,\today,\uppercase,\uccode}
% \DoNotIndex{\baselineskip,\begin,\tw@}
% \DoNotIndex{\a,\b,\c,\d,\e,\f,\g,\h,\i,\j,\k,\l,\m,\n,\o,\p,\q}
% \DoNotIndex{\r,\s,\t,\u,\v,\w,\x,\y,\z,\A,\B,\C,\D,\E,\F,\G,\H}
% \DoNotIndex{\I,\J,\K,\L,\M,\N,\O,\P,\Q,\R,\S,\T,\U,\V,\W,\X,\Y,\Z}
% \DoNotIndex{\1,\2,\3,\4,\5,\6,\7,\8,\9,\0}
% \DoNotIndex{\!,\#,\$,\&,\',\(,\),\+,\.,\:,\;,\<,\=,\>,\?,\_}
% \DoNotIndex{\discretionary,\immediate,\makeatletter,\makeatother}
% \DoNotIndex{\meaning,\newenvironment,\par,\relax,\renewenvironment}
% \DoNotIndex{\repeat,\scriptsize,\selectfont,\the,\undefined}
% \DoNotIndex{\arabic,\do,\makeindex,\null,\number,\show,\write,\@ehc}
% \DoNotIndex{\@author,\@ehc,\@ifstar,\@sanitize,\@title,\everypar}
% \DoNotIndex{\if@minipage,\if@restonecol,\ifeof,\ifmmode}
% \DoNotIndex{\lccode,\newtoks,\onecolumn,\openin,\p@,\SelfDocumenting}
% \DoNotIndex{\settowidth,\@resetonecoltrue,\@resetonecolfalse,\bf}
% \DoNotIndex{\clearpage,\closein,\lowercase,\@inlabelfalse}
% \DoNotIndex{\selectfont,\mathcode,\newmathalphabet,\rmdefault}
% \DoNotIndex{\bfdefault}
%
% ^^A I also exclude the commands used to generate the index
% \DoNotIndex{\CodelineIndex,\DeleteShortVerb,\DisableCrossrefs}
% \DoNotIndex{\EnableCrossrefs,\OnlyDescription,\RecordChanges}
%
% \MakeShortVerb{\"}
%
% \title{The \semantic\ package\thanks
%  {This file has version \semanticVersionPrint\ and is dated
%  \semanticDate. It is CVS revision \RCSRevision, dated \RCSDate.}\thanks{Michael John Downes of AMS provided a patch to
%  make the \semantic compatible with \texttt{amsmath} v.2.01.}}
% \author{Peter M{\o}ller Neergaard^^A
%     \thanks{\texttt{turtle}@\texttt{turtle@linearity.org},
%             \texttt{http://linearity.org/turtle}} \\
%   Arne John Glenstrup^^A
%     \thanks{\texttt{panic}@\texttt{diku.dk}, 
%             \texttt{http://www.diku.dk/\lower0.7ex\hbox{\~{}}panic}}}
% \maketitle
%
% \begin{abstract}
%   The aim of this package is to help people doing programming
%   languages using \LaTeX.  The package provides commands that
%   facilitates the use of the notation of semantics and compilation
%   in your documents. It provides an easy way to define new
%   ligatures, \eg making "=>" a short hand for \cmd{\RightArrow}.  It
%   fascilitates the drawing of inference rules and allows you to draw
%   T-diagrams in the "picture" environment.  It supports writing
%   extracts of computer languages in a uniform way. It comes with a
%   predefined set of shorthand suiting most people.
% \end{abstract}
%
% ^^A Table of contents in two columns --- borrowed from the standard 
% ^^A package of ``doc.dtx''
% \ifmulticols
%   \addtocontents{toc}{\protect\begin{multicols}{2}}
% \fi
%
% {\parskip 0pt                ^^A We have to reset \parskip (bug in \LaTeX)
% \sloppy
% \tableofcontents
% }
%
% \ifmulticols
%   \begin{multicols}{2}[\noindent \medskip \rule{\textwidth}{.3pt}]
% \fi
% 
% \noindent \semantic\ is a \LaTeXe\ package facilitating the writing
% of notation of programming languages and compilation. To use it, the
% file "semantic.sty" should be placed so that \LaTeX\ can find
% it.
%
% The \semantic\ package consists of several parts, which can be used
% independently.  The different parts are
% 
% \begin{description}
% \item[Ligatures] providing an easy way to define ligatures for often used
%   symbols like $\Rightarrow$ and $\vdash$.
% \item[Inference Rules] fascilitating the presentation of inference rules and
%   derivations using inference rules.
% \item[T-diagrams] providing T-diagrams as an extension the "picture"
%   environment.
% \item[Reserved word\footnote{A better name is highly needed.}] fascilitating
%   getting a uniform appearance of langugage constructions.
% \item[Short hands] for often used symbols.
% \end{description}
% 
% In the following we describe the use of the various parts of
% \semantic and  the installation.  We also give a short introduction to the
% two files "semantic.dtx" and "semantic.ins".
% 
% This package is---like most other computer-programs---provided with
% several bugs, insuffiencies and inconsistencies. They should be regarded
% as features of the package. To increase the excitement of using the package
% these features appear in unpredictable places. If they 
% however get too annoying and seriously reduce your satisfaction with 
% \semantic, please notify us. You could also drop us a note if you 
% would like to be informed when \semantic\ is updated.
% 
% \ifmulticols
%   \end{multicols}
% \fi
%
% \iffalse^^A At the moment no bugs are known
%   \ifmulticols
%     \begin{multicols}{2}[\section*{Known Bugs}
%   \fi
%   \begin{columnItemize} 
%   \end{columnItemize}
%
%   \ifmulticols
%     \end{multicols}
%   \fi
% \fi
%
% \section{Loading}
%
% There is two ways of loading the \semantic\ package.  You can either load
% it with all the parts, or to save time and space, you can load, only the
% parts you will use.
%
% In the first case you just include 
% \begin{code}
%   \cmd{\usepackage}\marg{semantic}  
% \end{code}
% in your document preamble.
% 
% In the other case you include
% \begin{code}
%   \cmd{usepackage}\oarg{parts}\marg{semantic}
% \end{code} 
% in your document preamble.  \meta{parts} is a comma
% separated list of the parts you wants to include.  The possibilities
% are: "ligature", "inference", "tdiagram", "reserved", and
% "shorthand".  The different parts are described in detail below.
%
% \section{Math Ligatures}
% \subsection{Defining New Math Ligatures}
% \label{sec:DefiningNewMathLigatures}
%
% \DescribeMacro{\mathlig} When the package is loaded, you can define new
% ligatures for use in the math environments by using the
% \cmd{\mathlig}\marg{character sequence}\marg{ligature commands}
% command. \meta{character sequence} is a sequence of
% \DeleteShortVerb{\"}\DeleteShortVerb{\|}^^A
% characters\footnote{There are some restrictions on the characters you can
% use. This should be described here but isn't; basically you should stick
% to using the characters 
% \texttt{\frenchspacing ` " ' \~{}
% ! ? @ * ( ) [ ] < > - + = | : ; . , / 0\ldots 9}, and certainly this
% should suffice for any sane person.}^^A
% \MakeShortVerb{\"}
% that must be entered in the source file to achieve the effect of the
% \meta{ligature command}. If for example you write
% `"\mathlig{-><-}{\rightarrow\leftarrow}"', subsequently typing `"$-><-$"'
% will produce $\rightarrow\leftarrow$.
%
% \subsection{Turning Math Ligatures On and Off}
% \label{sec:TurningMathLigaturesOnAndOff}
%
% \DescribeMacro{\mathligson}\DescribeMacro{\mathligsoff} By default, math
% ligatures are in effect when the \package{mathligs} package is loaded,
% but this can be turned off and on by using the commands \cmd{\mathligsoff} and
% \cmd{\mathligson}. Thus, typing `"$-><-$" \cmd{\mathligsoff} "$-><-$"
% \cmd{\mathligson} "$-><-$"' 
% will produce $\rightarrow\leftarrow$ $-{}>{}<{}-$ $\rightarrow\leftarrow$.
%
% \subsection{Protecting Fragile Math Commands}
% \label{sec:ProtectingFragileMathCommands}
%
% \DescribeMacro{\mathligprotect} Unfortunately, some macros used in math
% mode will break when using 
% \package{mathligs}, so they need to be turned into protected macros with the
% declaration \cmd{\mathligprotect}\marg{macro}. \emph{NOTE:} This
% declaration only needs to be issued once, best in the preamble.
%
% 
% \section{Inference Rules}
% 
% \DescribeMacro{\inference}
% \DescribeMacro{\inference*}
% Inference rules like
% {\def\predicatebegin#1|-#2=>#3\predicateend{$#1 \vdash \texttt{#2} \Rightarrow #3$}
%   \[
%     \inference[It(1) :]{\rho|-$E$=>\textsc{False}}
%     {\rho|-while $E$ do $s$=>\rho } 
% \quad\quad 
%     \inference*[It(2) :]{\rho|-$E$=>\textsc{True} & \rho|-$s$=>\rho' \\
%                \rho'|-while $E$ do $s$=>\rho''}^^A
%     {\rho|-while $E$ do $s$=>\rho''}
% \]}
% and
% \[
%   \inference[$->*_1$]{p,\mathrm{M} ->* p',\mathrm{M'} \\ 
%                       p',\mathrm{M'} -> p'',\mathrm{M''}}
%       {p,\mathrm{M} ->* p'',\mathrm{M''}} \;\;\;\;
%   \inference[$->*_2$]{}{p,\mathrm{M} ->* p,\mathrm{M}}
% \]
% are easily set using \cmd{\inference} and \cmd{\inference*}. The syntax is 
% \begin{code}
%   \cmd{\inference}\oarg{name}"{"\meta{line$_1$}" \\ \cmd{\lttdots} \\ "\meta{line$_n$}"}"\marg{conclusion} 
% \end{code}
% and 
% \begin{code}
%   \cmd{\inference}"*"\oarg{name}"{"\meta{line$_1$}" \\ \cmd{\lttdots} \\ "\meta{line$_n$}"}"\marg{conclusion}
% \end{code}
% where $n \geq 0$ so that you  can also type axioms.  When using
% \cmd{\inference} the bar will be as wide as the conclusion and the premise,
% whichever is widest; while \cmd{\inference*} only will make the
% bar as wide as the conclusion (It(2) above). The 
% optional names are typeset on the side of the inferences that they appear.
%
% Each line consists of premises seperated by "&":
% \begin{code}
%   \meta{premise$_1$}"&\cmd{\lttdots}&"\meta{premise$_m$}
% \end{code}
% Note that $m$ can also be zero, which is used when typing axioms. Each
% premise and the conclusion are by default set in math mode (\see however
% \pageref{ref:changePredicateBegin}). 
% 
% The rules are set so that the line flushes with the center of small
% letters in the surrounding text. In this way, secondary conditions
% or names (like the first example above) can be written in the
% surrounding text. One may also set the rules in a table as shown
% below:
%
%   \begin{tabular}{ll}
%     Transitive (1): & 
%      \inference{p,\mathrm{M} ->* p',\mathrm{M}' \\ 
%                 p',\mathrm{M'} -> p'',\mathrm{M''}}
%          {p,\mathrm{M} ->* p'',\mathrm{M''}} \\
%     Transitive (2): &
%      \inference{}{p,\mathrm{M} ->* p,\mathrm{M}}
%   \end{tabular}
%
% An inference rule can  be nested within another rule without problems,
% like in:
% \[
%   \inference[$->*_1$]{
%     \inference[$->*_1$]{
%       \inference[$->*_2$]{}
%       {p,\mathrm{M} ->* p,\mathrm{M}} & 
%       p,\mathrm{M} ->* p',\mathrm{M'}}
%     {p,\mathrm{M} ->* p',\mathrm{M'}} & 
%     p',\mathrm{M'} -> p'',\mathrm{M''}}
%   {p,\mathrm{M} ->* p'',\mathrm{M''}}
% \]
%
% \subsection{Controlling the Appearance}
% \DescribeMacro{\setpremisesend}
% \DescribeMacro{\setpremisesspace}
% \DescribeMacro{\setnamespace}
% The appearance of the inferences rules can be partly controlled by the
% following lengths:
% {\makeatletter
%  \setnamespace{3em}
%  \setpremisesend{2em}
%  \setpremisesspace{4em}
%  \[
%   \inference[^^A
%     \llap{\raisebox{0.1em}{$\overbrace{\hskip\@@nSpace}^{\makebox[0pt]{\footnotesize namespace}}$}}^^A
%     name
%   ]{^^A
%     \llap{$\overbrace{\hskip\@@pEnd}^{\makebox[0pt]{\footnotesize premisesend}}$}^^A
%     premise &
%     \llap{$\overbrace{\hskip\@@pSpace}^{\makebox[0pt]{\footnotesize premisesSpace}}$}^^A
%     premise
%   }{
%     conclusion
%   }
%  \]
%  \makeatother^^A
% }^^A
% The lengths are changed using the three commands
% \cmd{\setnamespace}\marg{length}, \cmd{\setpremisesend}\marg{length} and
% \cmd{\setpremisesspace}\marg{length}. \meta{length} can be given in both
% absolute units like "pt" and "cm" and in relative units like "em" and "ex".
% The default values are: 1$\frac{1}{2}$"em" for "premisesspace",
% $\frac{3}{4}$"em" for "premisesend" and $\frac{1}{2}$"em" for "namespace".
% Note that the lengths \emph{cannot} be altered using the ordinary
% \LaTeX-commands \cmd{\setlength} and \cmd{\addtolength}.
%  
% Besides that, the appearance of inference rules is like fractions in math:
% Among other things the premises will \emph{normally} be at same height
% above the baseline and there is a minimum distance from the line to the
% bottom of the premises.
%
% {\small ^^A This description is only for TeXnichians and it it therefore
%         ^^A written in a smaller font.
% \ifdanger \setparagraphmark{\small\danger} ^^A The dangorous bend is 
%                                            ^^A designed to span two lines
%    \parmark
% \else 
%   \setparagraphmark{\bfseries !!}\parmark\footnote{As your installation
%     lacks the ``dangerous bend'' used in \emph{The \TeX\ book}, we have 
%     used double exclamation marks to  indicate that you do not need to 
%     understand the following paragraphs to use \semantic.}^^A
% \fi
% Fetching the font information from the math font and the evaluation (in
% case they are defined in relative units) of the lengths mentioned above is
% done just before the individual rule is set. This is demonstrated by the
% following construction (which admittedly is not very useful):
%
% \smallskip
% {\hfill
%   \Large^^A
%    \inference[Large]{\normalsize^^A
%      \inference[normalsize]{\footnotesize^^A
%       \inference[footnotesize]{\tiny^^A
%         \inference[tiny]{}{Conclusion}}
%        {Conclusion}}
%      {Conclusion}}
%    {Conclusion}\hfill}
% \smallskip\linebreak
% Note that  from  top to  bottom, the leaves get bigger
% and the names get further from the line below.
% 
% \subsection{Formatting the Entries}
% \parmark
% \DescribeMacro{\predicate} 
% To set up a single predicate (a premise or conclusion) the single-argument
% command \cmd{\predicate} is used. This allows a finer control of the
% formatting. As an example, all premises and conclusions can be set in
% mathematics mode by the command:
% \begin{code}
%   "\renewcommand{\prediate}[1]{$ #1 $}"
% \end{code}
%
% \parmark
% \semantic\ uses \cmd{\predicate} on a premise only when the premise does not
% contain a nested \cmd{\inference}.\footnote{What \semantic\ precisely does is
%   to append the tokens \cs{inference} \cs{end} to the code of a
%   premise, when it has isolated it. \semantic\ then uses \TeX's pattern
%   matching to search this new list of tokens for an appearance of the token
%   \cs{inference}. When this is found the following token is examened,
%   and if it is \cs{end}, \semantic\ concludes that the premise does not
%   contain a nested inference rule} So even if the declaration above has been
% given, \cmd{\inference} is \emph{never} be executed in math mode. Neither is
% it used on the premises if you write:
% \begin{code}
%   "\inference{\inference"\lttdots"}{"\lttdots"}"
% \end{code}
% 
% \parmark
% \DescribeMacro{\predicatebegin} 
% \DescribeMacro{\predicateend}
% \label{ref:changePredicateBegin}
% The default definition of \cmd{\predicate} is "\predicatebegin #1\predicateend",
% where \cmd{\predicatebegin} and \cmd{\predicateend} are defined to `"$"'. In this
% way the premises and conlusions are set in math
%
% \parmark 
% The motivation for introducing \cmd{\predicatebegin} and \cmd{\predicateend}
% was, however, to use \TeX's pattern matching on macro arguments to do even
% more sophisticated formatting by redefining \cmd{\predicatebegin}. 
% \label{pattern matching}
% If for example, \emph{every} \textsl{expression} is to be evaluated in an
% \textsl{environment} giving a \textsl{value}, and you would like to set
% \emph{all} the \textsl{environment's} \textsl{values} in mathematics and the
% \textsl{expressions} in \texttt{typewriter}-font, then this could be
% facilitated by the definition:
% \begin{code}
%   "\def\predicatebegin#1|-#2=>#3#4\predicateend{%" \\
%   "  $#1 \vdash$\texttt{#2}$\stackrel{#3}{\Rightarrow}_S #4$}"
% \end{code}\hangindent=0pt
% Then the inference (borrowed from \textsc{M. Hennessy}, \emph{The 
% Semantics of Programming Languages})
% {\def\predicatebegin#1|-#2=>#3#4\predicateend{$#1 \vdash$\texttt{#2}$\stackrel{#3}{\Rightarrow}_S #4$}
% \[
%   \inference[TlR]{D |- $s$ =>{v} s' & D |- $s$ =>{v'} s''}
%     {D |- Tl($s$) =>{v'} s''}
% \]}^^A
% can be accomplished by
% \begin{code}
%   "\inference[TlR]{D |- $s$ =>{v} s' & D |- $s$ =>{v'} s''}" \\
%   "  {D |- Tl($s$) =>{v'} s''}"
% \end{code} 
% Please note that the "ligatures" option \emph{has not} been used
% above. } 
% ^^A TeXnichian mode OFF
%
% \section{T-diagrams}
%
% \DescribeMacro\compiler
% \DescribeMacro\interpreter
% \DescribeMacro\program
% \DescribeMacro\machine
% To draw T-diagrams describing the result of using one or more
% compilers, interpreters etc., \semantic\ has commands for the diagram:
% \begin{center}
%   \begin{picture}(280,40)
%     \put(10,0) {\program{P,L}}
%     \put(70,0){\interpreter{S,L}}
%     \put(160,0){\compiler{S,M,T}}
%     \put(250,11.45){\machine{M}}
%   \end{picture}
% \end{center}
% These commands should only be used in a "picture" environement and are
% \begin{code}
%   \cmd{\program}"{"\meta{program}","\meta{implementation language}"}" \\
%   \cmd{\interpreter}"{"\meta{source}","\meta{implemenation language}"}" \\
%   \cmd{\compiler}"{"\meta{source}","\meta{machine}","\meta{target}"}" \\
%   \cmd{\machine}\marg{machine}
% \end{code}
% The arguments can be a either a string describing the language (please do
% not begin the string with a  macro name), or one of the four commands.
% However, combinations taht make no sense---like implementing an
% interpreter on a program---are excluded, yielding an error message like:
% \begin{code}
% \begin{verbatim}
% ! Package semantic Error: A program cannot be at the bottom .
% 
% See the semantic package documentation for explanation.
% Type  H <return>  for immediate help.
%  ...                                      
% \end{verbatim}
% \end{code}
% 
% When you are use a command as an argument \semantic, will copy the
% language from the nested command and automaticly place the two figures in
% proportion to each other. In this way, big T- diagrams can easily be
% drawn. The hole construction should be placed using af \cmd{\put} command,
% where the \emph{reference point} is the center of the bottom of the figure
% corresponding to the outermost command. An example (with the
% reference point marked by
% \raisebox{.5ex}[0pt][0pt]{\begin{picture}(6,0)(-3,0)\put(0,0){\circle*{3}}\end{picture}})
% will clarify some of these point.  The figure
% \begin{center}
%   \begin{picture}(220,75)(0,-35)
%      \put(10,0){\interpreter{S,L'}}
%      \put(10,0){\circle*{3}}
%      \put(110,0){\program{P,\compiler{C,\machine{M},\program{P,M}}}}
%      \put(110,0){\circle*{3}}
%   \end{picture}
% \end{center}
% is obtained by the commands
% \begin{code}
%   "\begin{picture}(220,75)(0,-35)" \\
%   " \put(10,0){\interpreter{S,L'}}" \\
%   " \put(110,0){\program{P,\compiler{C,\machine{M},\program{P,M}}}}" \\
%   "\end{picture}"
% \end{code}
% Note from the second example that when \cmd{\compiler} is used as
% ``implementation language''-argument it is by convention attributed to the
% right of the figure. It is also worth mentioning that there is no strict
% demand on which command you should choose as the outermost, \emph{ie} the 
% second example could also be written (with a change of the parameters of 
% \cmd{\put} due to the new reference point) as
% \begin{code}
%   "\put(160,-20){\compiler{\program{P,C},\machine{M},\program{P,M}}}"
% \end{code}
% starting off in the middle instead of using a
% ``left-to-right''-approach.  In fact,  it is  often easier to start in
% the middle, since this is where you get the least levels of nesting.
% 
% Even though most situations may be handled by means of nesting, it is in
% some rare cases adequate to use different 
% language symbols on the two sides of the line of touch.
% When \emph{eg} describing bootstrappring the poor U-code
% implementation can be symbolized by \texttt{U$^{-}$}, indicating that the
% poor implementation is still executed on a  \texttt{U}-machine. This can
% be done by providing the symbol-command 
% with an optional argument immediately after the command name. Thus
% the bootstrapping
% \begin{center}
%   \begin{picture}(230,100)(-90,-20)
%     \put(0,0){\compiler{\compiler{ML,ML,U},\machine[U$^{-}$]{U},\compiler{\compiler{ML,ML,U},\machine[U$^{-}$]{U},\compiler{ML,U,U}}}}
%   \end{picture}
% \end{center}
% is typed 
% \begin{code}
%  "\compiler{\compiler{ML,ML,U},\machine[U$^-$]{U},\compiler{"\\
%  "     \compiler{ML,ML,U},\machine[U$^-$]{U},\compiler{ML,U,U}}}"
% \end{code}
%
% For calculating the dimensions of the "picture"-environment, one needs the
% dimensions of the individual figures.  In  units of  
% \cmd{\unitlength} they are the following:
%
% \ifmulticols
%   \begin{multicols}{2}
% \fi \noindent
%   compiler: 80*40 \\
%   interpreter: 20*40 \\
%   machine: 20*17.1 \\
%   program: 20*40
% \ifmulticols
%   \end{multicols}
% \fi
%
% \section{Reserved Words}
% \label{sec:Reserved Words}
%
% ^^A \tracingmacros=1 \tracingonline=1
% \reservestyle{\command}{\mathbf}     \command{let,in}
% \reservestyle{\punctuation}{\mathtt} \punctuation{=}
% \tracingmacros=0
%
% When describing computer languages, one often wants to typeset commands in
% one style, expressions in another style, and punctuation characters in
% yet another style, for instance
% \[
%   \<let> \; x \;\<=>\; e \;\<in>\; e
% \]
%
% \DescribeMacro{\reservestyle}
% The \semantic\ package supports this by allowing you to reserve a certain
% \emph{style} for certain language constructs.  The fundamental command is
% \begin{code}
%   \cmd{\reservestyle}\marg{\cs{stylename}}\marg{formatting}
% \end{code}
% \cmd{\reservestyle} reserves \cs{\meta{stylename}} as the macro to define
% the language constructs.  The language constructs will be set using
% \meta{formatting}. 
% 
% The reserved macro \cs{\meta{stylename}} should be given a comma
% separated list of words to reserve.  For instance to reserve the words
% $\<let>$ and $\<in>$ as  
% commands, which all are set using a bold font, you can put
% \begin{code}
%   "\reservestyle{\command}{\textbf}" \\
%   "\command{let,in}"
% \end{code}
% in the preamble of your document.  Note that there must not any
% superfloues space in the comma separated list.
% Thus for instance \verb*+\command{let , in}+
% would reserve $\setcommand{let\ExplicitSpace}$ resp.\
% $\setcommand{\ExplicitSpace in}$ instead of $\<let>$ resp. $\<in>$!
% You can of course reserve several styles
% and reserve several words within each of the styles.
%  
% \DescribeMacro{\<}
% To refer to a \emph{reserved word} in the text you use the command
% "\<"\meta{reserved word}">", \eg "\<let>".  If you have reserved several
% styles, \semantic will find the style that was used to reserve
% \meta{reserved word} and use the appropriate formatting commands.
% 
% The "\<"$\cdots$">" can be used in both plain text and in math mode.  You
% should, however, decide in the preamble if a given style should be used in
% math mode or in plain text, as the formatting commands will be different.
%  
% \DescribeMacro{\set\protect\meta{style}}
% If you only want to type  a reserved word a single time, it can seem tedious
% first to reserve the word  and then refer to it once using "\<"$\cdots$">".
% Instead you can use the command \cs{set\meta{style}} that is defined for each
% style you reserve.
%  
% \subsection{Bells and Whistles: Spacing in Math Mode}
% 
% In many situations it seems best to use \emph{reserved words} in math
% mode---after all you get typesetting of expressions for free.  The drawback
% is that it becomes more difficult to get the space correct.  One can of
% course allways insert the space by hand, \eg "$\<let>\; x=e \;\<in>\; e'$",
% However, this soon becomes tedious and \semantic have several ways to try to
% work around this.
% 
% The first option is to provide \cmd{\reservestyle} with an optional spacing
% command, \eg \cmd{\mathinner}.  For instance
% \begin{code}
%   "\reservestyle[\mathinner]{\command}{\mathbf}"
% \end{code}
% will force all \emph{commands} to be typeset with spacing of math inner
% symbols.
% 
% You can also provide an optional space command to each reservation of 
% words.  For instance 
% \begin{code}
%   "\command[\mathrel]{in}"
% \end{code}
% will make $\<in>$ use the spacing of the relational symbols.  The space
% command is applied to all the words in the reservation.  Thus if you would
% like $\<in>$ and $\<let>$ to have different space commands, you must
% specify them in two different \cmd{\command}.
% 
% The drawback of using the math spacing is that in the rare cases where you
% use the reserved words in super- or subscripts, most of the spacing will
% disappear.  This can be avoided by defining the replacement text to be the
% word plus a space, \eg "\;in\;".  For this end a reservation of a word can
% be followed by an explicit replacement text in brackets, \eg
% \begin{code}
%   "\command{let[let\;], in[\;in\;]}"
% \end{code}
% The formatting of \cmd{\command} (with the setting above: \cmd{\mathbf}) will still
% be used so it is only necessary to provide the replacement text.  Note
% that each word in the reservation can have its own optional replacement
% text.
%
% The drawback of this method is, that the you also get the space, if you use
% the reserved word ``out of context'', for instance refering to the
% $\;\<in>\;$-token!  In these cases you can cancel the space by hand using
% "\!".  
%
% This option is also usefull, if you want to typeset the same word in two
% different styles.  If you for instance sometimes want `let' to be typeset
% as a command and sometimes as data, you can define
% \begin{code}
%   "\command{let}" \\
%   "\data{Let[let]}"  
% \end{code}
% Then "\<let>" will typeset the word `let' as a command, while "\<Let>" will
% typeset it as data.  Note that in both cases the word appears in
% lower case.
% 
% Unfortunately there is no way to get the right spacing everytime, so you
% will have to choose which of the two methods serves you the best.
%
% \section{Often Needed Short Hands}
% 
% Within the field of semantics there are a tradition for using some special.
% symbols.  These are provided as default as short hand in the \semantic\
% package.  Most of the following symbols are defined as ligatures, and
% hence the "ligature" option is always implied when the "shorthand" option
% is provided.
%
% \makeatletter
% \subsection{The Meaning of: \@bblb\ and \@bbrb}
% \marginpar{\raggedleft\strut\@bblb}
% \marginpar{\raggedleft\strut\@bbrb}
%
% The symbols for denoting the meaning of an expression, 
% \@bblb\ and \@bbrb\ are provided as short
% hands in math with the ligatures "|[" and "|]".
% \makeatother 
%
% \subsection{Often Needed Symbols}
% 
% The following ligatures are defined for often needed symbols
%
% \begin{tabular}[c]{cl@{\qquad\qquad}cl}
%   $\vdash$   & "|-"   & $\mathligsoff\models$  & "|="   \\
%   $<->$  &  "<->"     & $<=>$  &  "<=>" \\
%   $->$   & "->"       & $-->$  &  "-->" \\
%   $=>$   & "=>"       & $==>$  &  "==>" \\
%   $<-$   & "<-"       & $<--$  &  "<--" \\
%   $<=$   & "<="       & $<==$  &  "<==" \\
% \end{tabular}
%
% All the single directed arrows also comes in a starred and plussed form, \eg\
% "*<=" gives $*<=$ and "-->+" gives $-->+$.
%
% \DescribeMacro{\eval} 
% \DescribeMacro{\comp} 
% To support writing denotational, semantics the commands \cmd{\comp} and \cmd{\eval}
% are provided to describe the evaluation of programs respectively
% expressions. They have the same syntax:
% \cmd{\comp}\marg{command}\marg{environment}, which yields
% \comp{\meta{command}}{\meta{environment}}.  If you need to describe more
% than one kind of evaluations, e.g.\ both \evalsymbol\ and \evalsymbol[*],
% you can provide an optional argument immediately after \cmd{\comp} or
% \cmd{\eval}, respectively. As an example a denotational rule for a
% sequencing two commands
% \[
% \comp{C1 ; C2}{d} = \mathtt{d'} \quad \texttt{if $\comp{C1}{d} = \mathtt{d''}$ and $\comp{C2}{d''} = \mathtt{d'}$}
% \]
% can be typed
% \begin{code}
%   "\["\\
%   "  \comp{C1 ; C2}{d} = \mathtt{d'} \quad "\\
%   "   \texttt{if $\comp{C1}{d} = \mathtt{d''}$ and"\\
%   "              $\comp{C2}{d''} = \mathtt{d'}$}"\\
%   "\]"
% \end{code}
% 
% \DescribeMacro{\evalsymbol}
% \DescribeMacro{\compsymbol}
% As shown above, you can get the evaluation symbol in itself. This is done by
% \cmd{\compsymbol} or  \cmd{\evalsymbol}, respectively. These commands can also be
% supplied with an optional argument, e.g.\ "\evalsymbol[*]" to get
% \evalsymbol[*].
% 
% \DescribeMacro{\exe} The result of executing a program on a machine
% with som data can be described using \cmd{\exe}, which has the syntax
% \cmd{\exe}\marg{program}\oarg{machine}\marg{data}. The third Futumara projection
% $\mathtt{cogen} = \exe{spec}{spec.spec}$ can be written
% "$\mathtt{cogen} = \exe{spec}{spec.spec}$". As an alternative, you
% can also give the machine \texttt{L} explicit:
% \begin{code} 
%   "$\mathtt{cogen} = \exe{spec}[L]{spec.spec}$"
% \end{code}
%  This will result in:
% $\mathtt{cogen} = \exe{spec}[L]{spec.spec}$
%
% \section{Some Notes about the Files}
% 
% \semantic\ is distributed in two files, "semantic.dtx" and
% "semantic.ins".  Of these two files, "semantic.dtx" is the most
% important, as it contains all the essentials---users guide, code and
% documentation of the code.  "semantic.ins" is used only to guide
% \package{docstrip} in generating "semantic.sty" from "semantic.dtx".
% 
% {\makeatletter To get \@bblb\ and \@bbrb, used in \cmd{\comp}, \cmd{\eval} and \cmd{\exe}
%   \semantic, tries to load the package \package{bbold} written by 
%   \textsc{A. Jeffrey}. If this is not installed on your system, the symbols
%   are simulated by drawing together two sharps. However, we  recommend 
%   that you get \package{bbold} from your nearest CTAN-archive. 
% \makeatother}
% 
% In addition to the users guide, you can also get the fully documented code.
% You need this, however, if you want to see how the macros are implemented
% the macros or if you want to change some part of the package. You should
% start by editing "semantic.dtx" and remove the percentage signs from the
% four lines starting at Line~\ref{lin:AlsoImplementation}
% \begin{verbatim}
% % \AlsoImplementation
% % \EnableCrossrefs
% % \CodelineIndex
% % \RecordChanges
% \end{verbatim} 
% After saving the changes, you should run \LaTeX\ twice on the edited
% file to get a correct table of contents. Then you generate the index
% and change history, using "makeindex":
% \begin{code}
%   "makeindex -s gind.ist semantic" \\
%   "makeindex -s gglo.ist -o semantic.gls semantic.glo"
% \end{code}
% After another run of \LaTeX, then the documentation is ready for printing.
% 
% \medskip
% \parmark[\copyright]^^A
% At last the boring formal stuff: The package is protected by the The
% \LaTeX\ Project Public License (lppl). You are encouraged to copy, use, delete
% etc.\ the package ("semantic.dtx" and "semantic.ins") as much as
% your heart, but if you modify the code (even locally), you should
% change the name to avoid confusion.  Under all circumstances, the
% package is still: {\small \copyright 1995--2000 Peter Møller Neergaard
% and Arne John Glenstrup.}
% 
% \StopEventually{
%  \ifmulticols
%    \addtocontents{toc}{\protect\end{multicols}}
%  \fi
% }
%
% \section{Documentation of the Package Code}
%
% \ifmulticols
%   \begin{multicols}{2}[\subsection{To Be Done (in Priority)}]
% \else
%   \subsection{To Be Done (in Priority)}
% \fi
% \changes{1.0}{1995/10/18}{Introduced a list of things to be done}
% \begin{columnItemize}
% \item Add a grammar option if needed.
% \item If at all possible, add a check for the existence of "manfnt.tfm".
% \item Use \cmd{\hrule} and \cmd{\vrule} instead of \cmd{\line} (cf.\ \package{Epic}) as
%   much as possible to build the translation diagrams , since this will
%   improve performance.
% \item Develop example macros that set an example and give the source text
%   for the example.
% \item Analyze my use of registers to see if I can reduce the
%   number of permanently reserved registers.
% \end{columnItemize}
% 
% \ifmulticols
%   \end{multicols}
% \fi
% 
% \subsection{Stub for Users Guide and Documentation}
%
% First comes a little hack that makes \LaTeX\ think it is loading the
% package \texttt{semantic.sty}.  In this way, the commands in the package can
% be for printing the documentation:
%    \begin{macrocode}
%<*documentation>
\makeatletter \def\@currname{semantic} \def\@currext{sty}
%</documentation>
%    \end{macrocode}
% \cmd{\@currname} and \cmd{\@currext} are internal \LaTeX-macros containg the name
% and extension of the package currently being loaded.  The code is
% encapsulated in "<*documentation>"\lttdots"</documentation>".  Thus it is
% not included in the style file, when the package is installed.
%
% \changes{2.0}{1995/05/24}{Added code for loader of different package options}
%
% \subsection{Package Identification and Option Loading}
%
% The package code starts by identifying the file as a \LaTeXe\ package:
%    \begin{macrocode}
%<*general>
\NeedsTeXFormat{LaTeX2e}
%    \end{macrocode}
% \begin{macro}{\semanticVersion}
% \begin{macro}{\semanticDate}
%   Constants definining the package release.
%    \begin{macrocode}
\newcommand{\semanticVersion}{2.0(epsilon)}
\newcommand{\semanticDate}{2003/10/28}
%    \end{macrocode}
%   \changes{2.0$\delta$}{2002/07/11}{Added.}
% \end{macro}^^A \semanticDate
%   \changes{2.0$\delta$}{2002/07/11}{Added.}
% \end{macro}^^A \semanticVersion
%    \begin{macrocode}
\ProvidesPackage{semantic}
  [\semanticDate\space v\semanticVersion\space]
\typeout{Semantic Package v\semanticVersion\space [\semanticDate]}
\typeout{CVSId: $Id: semantic.dtx,v 1.11 2003/10/28 13:45:57 turtle Exp $}
%</general>
%    \end{macrocode}
% \changes{2.0$\delta$}{2002/07/11}{Using \cs{typeout} to print (now) extended information to user.}
%
% \subsubsection{Avoid Naming Conflicts}
% 
% The following code is used to test that all names used by the
% \semantic-package are not used by other packages.
%
% \begin{macro}{\@semanticNotDefinable}
%   \changes{2.0$\alpha$}{1996/05/18}{Added redefinition of
%     \cs{@notdefinable} during package loading}
%   This replaces the internal \LaTeX\ command \cmd{\@notdefinable}, which is
%   used to issue an error message when a command cannot be defined, during
%   loading of \semantic.  The name of the command that could not be defined
%   is saved by \LaTeX\ in \cmd{\reserved@a}.
%    \begin{macrocode}
%<*general>
\newcounter{@@conflict}
\newcommand{\@semanticNotDefinable}{%
  \typeout{Command \@backslashchar\reserved@a\space already defined}
  \stepcounter{@@conflict}} 
\newcommand{\@oldNotDefinable}{}
\let\@oldNotDefinable=\@notdefinable
\let\@notdefinable=\@semanticNotDefinable
%    \end{macrocode}
%   The macro types the name of the confliction macro to the user and then 
%   marks that there has been a conflict by increasing the numbers of
%   conflicts encountered.  \cmd{\@notdefinable} is an internal \LaTeX\
%   command used to write an error message when a command cannot be
%   defined.  It is temporarily saved for later restoring.
% \end{macro}
%
% \begin{macro}{\TestForConflict}
%   \changes{2.0$\alpha$}{1996/05/18}{Added macro for testing for conlict
%     instead of using \cs{newcommand}}
%   \cmd{\@testconflict} takes a list of macros (separated by comma) and testes
%   that they are all undefined. If one of them is not undefined an error
%   message will be issued.  The syntax is choosen like \cmd{\DoNotIndex} from
%   \package{ltxdoc}.
%    \begin{macrocode}
\newcommand{\TestForConflict}{}
\def\TestForConflict#1{\sem@test #1,,}
%    \end{macrocode}
%   The macro initialises the testing and then uses \cmd{\@test} to test the
%   indiviual commands in the list.  
% \end{macro}
%
% \begin{macro}{\sem@test}
%   This is the command for doing the test of a single macro
%    \begin{macrocode}
\newcommand{\sem@test}{} 
\newcommand{\sem@tmp}{} 
\newcommand{\@@next}{}
\def\sem@test#1,{%
  \def\sem@tmp{#1}%
  \ifx \sem@tmp\empty \let\@@next=\relax \else 
    \@ifdefinable{#1}{} \let\@@next=\sem@test \fi
  \@@next}
%</general>
%    \end{macrocode}
%   The macro takes a single argument. If its not empty, \ie\ the list has
%   not been read to the end, the internal \LaTeX\ command \cmd{\@ifdefinable}
%   is used to test if the command can be defined (\see\
%   \cite[p.~192]{LaTeXbook}). 
% 
%   To avoid to many unclosed "\if" the macro is made tail recursive by
%   saving the next macro in \cmd{\@@next}.
%   \changes{2.0$\delta$}{2002/06/19}{Renamed \cs{@temp} \cs{sem@tmp}.}
% \end{macro}
%
% \subsubsection{Hack for the documentation}
%
% The following is a hack inserted to make the processing of the
% documentation, skip all the options loading and just incorporate the
% package code. 
%    \begin{macrocode}
%<*documentation>
\iftrue\iffalse
%</documentation>
%    \end{macrocode}
% The "\iftrue" matches the "\fi" in the bottom of the code, while the
% "\iffalse" is skipping the code controlling loading of the options.
%
% \subsubsection{Loading of Options}
%
% The code to load the different options is defined.  By ``erasing'' the
% definitions after loading the parts, the code ensures that no part is
% loaded more than once.
%    \begin{macrocode}
%<*general>
\TestForConflict{\@inputLigature,\@inputInference,\@inputTdiagram}
\TestForConflict{\@inputReservedWords,\@inputShorthand}
\TestForConflict{\@ddInput,\sem@nticsLoader,\lo@d}
\def\@inputLigature{\input{ligature.sty}\message{ math mode ligatures,}%
                     \let\@inputLigature\relax}
\def\@inputInference{\input{infernce.sty}\message{ inference rules,}%
                     \let\@inputInference\relax}
\def\@inputTdiagram{\input{tdiagram.sty}\message{ T diagrams,}%
                     \let\@inputTdiagram\relax}
\def\@inputReservedWords{\input{reserved.sty}\message{ reserved words,}%
                     \let\@inputReservedWords\relax}
\def\@inputShorthand{\input{shrthand.sty}\message{ short hands,}%
                     \let\@inputShorthand\relax}
%    \end{macrocode}
% Token register~1 is used for keeping the commands to load the package.
% An empty register will mark that all options should be loaded:
%    \begin{macrocode}
\toks1={}
%    \end{macrocode}
% \begin{macro}{\@ddInput}
%   \cmd{\@ddInput} adds its argument to the list of commands used for loading:
%    \begin{macrocode}
\newcommand{\@ddInput}[1]{%
  \toks1=\expandafter{\the\toks1\noexpand#1}}
%    \end{macrocode}
%   The \cmd{\expandafter} makes \cmd{\the} expand the tokens register~0 one level,
%   thus listing all the loading instructions.
% \end{macro}
%
% Each option add the code to load the option to token register~0.
%    \begin{macrocode}
\DeclareOption{ligature}{\@ddInput\@inputLigature}
\DeclareOption{inference}{\@ddInput\@inputInference}
\DeclareOption{tdiagram}{\@ddInput\@inputTdiagram}
\DeclareOption{reserved}{\@ddInput\@inputReservedWords}
\DeclareOption{shorthand}{\@ddInput\@inputLigature 
   \@ddInput\@inputShorthand}
%    \end{macrocode}
%
% The options are processed
%    \begin{macrocode}
\ProcessOptions*
%    \end{macrocode}
%
% and the specified options are loaded (if no options are specifieed, then
% all options are loaded) 
%    \begin{macrocode}
\typeout{Loading features: }
\def\sem@nticsLoader{}
\edef\lo@d{\the\toks1}
\ifx\lo@d\empty
  \@inputLigature
  \@inputInference
  \@inputTdiagram
  \@inputReservedWords
  \@inputShorthand
\else
  \lo@d
\fi
\typeout{and general definitions.^^J}
%    \end{macrocode}
% \cmd{\sem@nticsLoader} is flag used for testing in the options file to check
% that the files are loaeded from the package.
%
% After loading the options the name space is cleaned up.
%    \begin{macrocode}
\let\@ddInput\relax
\let\@inputInference\relax
\let\@inputLigature\relax
\let\@inputTdiagram\relax
\let\@inputReservedWords\relax
\let\@inputShorthand\relax
\let\sem@nticsLoader\realx
\let\lo@d\relax
%</general>
%    \end{macrocode}
% 
% \subsubsection{Options' Test that They Are Loaded by \semantic}
%
% \label{page:testForSemanticsLoader}
% The following does a test in all the options files to see whether they are
% loaded from the \semantic\ package.  If not, no commands are defined.  See
% also the bottom of the code part, where the mathcing "\fi" is provided.
%    \begin{macrocode}
%<*allOptions>
\expandafter\ifx\csname sem@nticsLoader\endcsname\relax
%    \end{macrocode}
%  A feature of \cmd{\csname}\meta{name}\cmd{\endcsname} is that the command
%  sequence would be taken to be \cmd{\relax} if \cs{\meta{name}} is not
%  defined.
%    \begin{macrocode}
  \PackageError{semantic}{%
    This file should not be loaded directly}
    {%
      This file is an option of the semantic package.  It should not be
        loaded directly\MessageBreak 
      but by using \protect\usepackage{semantic} in your document 
        preamble.\MessageBreak
      No commands are defined.\MessageBreak
     Type <return> to proceed.
    }%
\else
%</allOptions>
%    \end{macrocode}
% This is the end of the part, which should not be processed when processing
% the documentation
%    \begin{macrocode}
%<*documentation>
\fi\fi
%</documentation>
%    \end{macrocode}
%
% \subsubsection{Auxiliary Macros}
%
%    \begin{macrocode}
%<*general>
\TestForConflict{\@dropnext,\@ifnext,\@ifn,\@ifNextMacro,\@ifnMacro}
\TestForConflict{\@@maxwidth,\@@pLineBox,\if@@Nested,\@@cBox}
\TestForConflict{\if@@moreLines,\@@pBox}
%    \end{macrocode}
%
% \begin{macro}{\@ifnext}
%   This macro compares the next token with a given token (\#1), and if they
%   are identical, 
%   the first choice (\#2) is expanded, else the second choice(\#3).
%   This is a loan of \cmd{\@ifnextchar} from the \LaTeXe-base and it therefore
%   uses the interal variables \cmd{\reserved@a}\lttdots\cmd{\reserved@d}. The only
%   change from \cmd{\@ifnextchar} is that spaces are not ignoree.  This is
%  appropriate for defining 
%   the ligatures (eg.\ I do not want \verb*"- >" to be converted to 
%   $\rightarrow$).
%    \begin{macrocode}
\def\@ifnext#1#2#3{%
  \let\reserved@e=#1\def\reserved@a{#2}\def\reserved@b{#3}\futurelet%
  \reserved@c\@ifn} 
\def\@ifn{%
      \ifx \reserved@c \reserved@e\let\reserved@d\reserved@a\else%
          \let\reserved@d\reserved@b\fi \reserved@d}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@ifNextMacro}
%   This macro examines the next token, and if it is a macro, the first
%   option (\#1) is executed, else the second option (\#2). Like
%   \cmd{\@ifnext}, the code is mainly ``borrowed'' from the \LaTeX-source.
%    \begin{macrocode}
\def\@ifNextMacro#1#2{%
  \def\reserved@a{#1}\def\reserved@b{#2}%
    \futurelet\reserved@c\@ifnMacro} 
\def\@ifnMacro{%
  \ifcat\noexpand\reserved@c\noexpand\@ifnMacro 
    \let\reserved@d\reserved@a
  \else \let\reserved@d\reserved@b\fi \reserved@d}
%    \end{macrocode}
%   The test of whether it is a macro, is done in \cmd{\@ifnMacro} by comparing the 
%   catcodes of the token and a macro, \cmd{\@ifnMacro} (any other
%   macro could have been used as well). The \cmd{\noexpand} secures that I compare 
%   the token and not its expansion. If \emph{eg} \cmd{\@noexpand} were left out and 
%   the token were a macro, then it would be expanded and the first token in 
%   the macro be compared to the first token in \cmd{\@ifnMacro}.
% \end{macro}
%
% \begin{macro}{\@dropnext}
%   This macro  processes the next token  and ignores its successor
%   (it is not processed at all). 
%    \begin{macrocode}
\newcommand{\@dropnext}[2]{#1}
%</general>
%    \end{macrocode}
%  \end{macro}
%
% \subsubsection{Testing for  Name Conflict  During Loading}
%
% At the end of the loading it is tested if an error has occurred.  In that
% case an error message is issued.  Then the testing commands is disabled.
%
% \medskip\noindent But first  yet another documentation hack$\ldots$
%    \begin{macrocode}
%<*documentation>
\iffalse
%</documentation>
%<*general>
\ifnum \value{@@conflict} > 0
   \PackageError{Semantic}
     {The \the@@conflict\space command(s) listed above have been
      redefined.\MessageBreak
      Please report this to turtle@bu.edu}
     {Some of the commands defined in semantic was already defined %
      and has\MessageBreak now be redefined. There is a risk that %
      these commands will be used\MessageBreak by other packages %
      leading to spurious errors.\MessageBreak
      \space\space Type <return> and cross your fingers%
}\fi
\let\@notdefinable=\@oldNotDefinable
\let\@semanticNotDefinable=\relax
\let\@oldNotDefinable=\relax
\let\TestForConflict=\relax
\let\@endmark=\relax
\let\sem@test=\relax
%</general>
%    \end{macrocode}
%
% \medskip\noindent The end of yet another documentation hack
%    \begin{macrocode}
%<*documentation>
\fi
%</documentation>
%    \end{macrocode}
%
% \subsection{Math Ligatures}
%
%    \begin{macrocode}
%<*ligature>
\TestForConflict{\@addligto,\@addligtofollowlist,\@def@ligstep}
\TestForConflict{\@@trymathlig,\@defactive,\@defligstep}
\TestForConflict{\@definemathlig,\@domathligfirsts,\@domathligfollows}
\TestForConflict{\@exitmathlig,\@firstmathligs,\@ifactive,\@ifcharacter}
\TestForConflict{\@ifinlist,\@lastvalidmathlig,\@mathliglink}
\TestForConflict{\@mathligredefactive,\@mathligsoff,\@mathligson}
\TestForConflict{\@seentoks,\@setupfirstligchar,\@try@mathlig}
\TestForConflict{\@trymathlig,\if@mathligon,\mathlig,\mathligprotect}
\TestForConflict{\mathligsoff,\mathligson,\@startmathlig,\@pushedtoks}
%    \end{macrocode}
%
% \subsubsection{User Interface}
% \label{sec:UserInterface}
%
% \begin{macro}{\if@mathligon}
%   First we define a new "\if" flag that indicates whether the user has
%   requested math ligatures to be active or not:
%    \begin{macrocode}
\newif\if@mathligon
%    \end{macrocode}
% \end{macro}
% \begin{macro}{\mathlig}
%   Now, for the definition of \cmd{\mathlig}\marg{character
%   sequence}\marg{ligature commands}, we first add the ligature
%   character sequence $c_1c_2\cdots c_n$ to the internal ligature
%   character lists, and then 
%   we set up the macros "\@mathlig"$c_1c_2\cdots$ by calling
%   \cmd{\@defligstep}:
%    \begin{macrocode}
\DeclareRobustCommand\mathlig[1]{\@addligtolists#1\@@
  \if@mathligon\mathligson\fi
  \@setupfirstligchar#1\@@
  \@defligstep{}#1\@@}
%    \end{macrocode}
%   \changes{2.0$\beta$}{2000/08/02}{Corrected typo in \cs{mathligson}.}
% \end{macro}
% \DescribeMacro{\@mathligson}\DescribeMacro{\@mathligsoff}
% We define macros \cmd{\@mathligson} and \cmd{\@mathligsoff} for turning math
% ligatures on and off internally without changing the status of the
% "\if@mathligon" flag:
%    \begin{macrocode}
\def\@mathligson{\if@mathligon\mathligson\fi}
\def\@mathligsoff{\if@mathligon\mathligsoff\@mathligontrue\fi}
%    \end{macrocode}
% \begin{macro}{\mathligprotect}
% \cmd{\mathligprotect}\marg{command} defines \meta{command} to be a macro
% expanding into \cmd{\@mathligsoff}\emph{expansion
% of}\meta{command}\cmd{\@mathligson}:
%    \begin{macrocode}
\DeclareRobustCommand\mathligprotect[1]{\expandafter
  \def\expandafter#1\expandafter{%
    \expandafter\@mathligsoff#1\@mathligson}}
%    \end{macrocode}
% \end{macro}
% \begin{macro}{\mathligson}
% \cmd{\mathligson} changes the math code of all the characters that can occur
% as the first character of a ligature character sequence to be active, and
% sets the "\if@mathligon" flag:
%    \begin{macrocode}
\DeclareRobustCommand\mathligson{\def\do##1##2##3{\mathcode`##1="8000}%
  \@domathligfirsts\@mathligontrue}
%    \end{macrocode}
%  and turn on math ligatures automatically.
%    \begin{macrocode}
\AtBeginDocument{\mathligson}
%    \end{macrocode}
%   \changes{2.0$\beta$}{2000/08/02}{Ligature turned on when ligatures are loaded (moved from \texttt{shorthand} option).}
% \end{macro}
% \begin{macro}{\mathligsoff}
% \cmd{\mathligsoff} does the reverse actions: resetting math codes to their
% values as recorded at ligature definition time (stored in the
% \cmd{\@domathligfirsts} data structure).
%    \begin{macrocode}
\DeclareRobustCommand\mathligsoff{\def\do##1##2##3{\mathcode`##1=##2}%
  \@domathligfirsts\@mathligonfalse}
%    \end{macrocode}
% \end{macro}
%
% \subsubsection{Utilities}
% \label{sec:Utilities}
%
% \DescribeMacro{\@mathliglink} \cmd{\@mathliglink} is a dummy macro that
% should never be expanded, so we issue an error if it is:
%    \begin{macrocode}
\edef\@mathliglink{Error: \noexpand\verb|\string\@mathliglink| expanded}
%    \end{macrocode}
% \DescribeMacro{\@ifcharacter}\DescribeMacro{\@ifactive}
% \cmd{\@ifcharacter}\meta{character}\marg{truebranch}\marg{falsebranch} 
% is used to test whether \meta{character} is in fact a character and chooses the
% appropriate branch. \cmd{\@ifactive} is analogous.
%    \begin{macrocode}
{\catcode`\A=11\catcode`\1=12\catcode`\~=13 % Letter, Other and Active
\gdef\@ifcharacter#1{\ifcat A\noexpand#1\let\next\@firstoftwo
                \else\ifcat 1\noexpand#1\let\next\@firstoftwo
                \else\ifcat \noexpand~\noexpand#1\let\next\@firstoftwo
                \else\let\next\@secondoftwo\fi\fi\fi\next}%
\gdef\@ifactive#1{\ifcat \noexpand~\noexpand#1\let\next\@firstoftwo
                  \else\let\next\@secondoftwo\fi\next}}
%    \end{macrocode}
%
% \subsubsection{Data Structures}
% \label{sec:DataStructures}
%
% For each math ligature character sequence $c_1c_2\cdots c_n$ the macros
% "\@mathlig"$c_1$, "\@mathlig"$c_1c_2$, \ldots, "\@mathlig"$c_1c_2\cdots
% c_n$ are defined, and "\@mathlig"$c_1c_2\cdots c_n$ expands to the
% commands that typeset the ligature. For $1<i<n$, if $c_1c_2\cdots c_i$ is
% not also a ligature character sequence, it is defined as the (dummy)
% macro \cmd{\@mathliglink}\DescribeMacro{\@mathliglink}.
%
% E.g.: if `"-><-"' has been defined to typeset as
% "\rightarrow\leftarrow" and `"-->"' has been defined to typeset as
% \cmd{\longrightarrow}, the following macros will be defined:
% \begin{center}
% \begin{tabular}{ll}
% \textbf{Macro} & \textbf{is defined as} \\
% "\@mathlig-"     & "-"                     \\
% "\@mathlig--"    & \cmd{\@mathliglink}         \\
% "\@mathlig-->"   & \cmd{\longrightarrow}       \\
% "\@mathlig->"    & \cmd{\@mathliglink}         \\
% "\@mathlig-><"   & \cmd{\@mathliglink}         \\
% "\@mathlig-><-"  & "\rightarrow\leftarrow" \\
% \end{tabular}
% \end{center}
% As it can be seen, "\@mathlig"$c$ expands to $c$, so that the original
% meaning of a single character $c$ can be used.
%
% The macro \cmd{\@domathligfirsts}\DescribeMacro{\@domathligfirsts} holds a
% list of characters, which occur as a
% first character in a ligature character sequence, with their 
% "mathcode"s and "catcode"s as defined when the ligature is defined. E.g.:
% if ligatures have been defined for `"-><-"' and `"<--"', then
% \cmd{\@domathligfirsts} will expand into a token sequence containing the
% sequence
% \begin{center}
% "\do \-{8704}{12}\do \<{12604}{12}"
% \end{center}
% Thus, defining command "\do#1#2#3{"\emph{manipulate character}"#1}" and
% executing \cmd{\@domathligfirsts} manipulates all the first characters of
% ligature character sequences.
%
% The macro \cmd{\@domathligfollows}\DescribeMacro{\@domathligfollows} is
% analogous for characters that occur after the first character in a
% ligature character sequence. \cmd{\@makemathligsactive} and
% \cmd{\@makemathligsnormal} change the catcodes of these characters.
%    \begin{macrocode}
\def\@domathligfollows{}\def\@domathligfirsts{}
\def\@makemathligsactive{\mathligson
  \def\do##1##2##3{\catcode`##1=12}\@domathligfollows}
\def\@makemathligsnormal{\mathligsoff
  \def\do##1##2##3{\catcode`##1=##3}\@domathligfollows}
%    \end{macrocode}
% \begin{macro}{\@ifinlist}
%   \cmd{\@ifinlist}\marg{character/mathcode/catcode list}\discretionary{}{}{}^^A
%              \marg{character}\discretionary{}{}{}^^A
%              \marg{true\-branch}\discretionary{}{}{}^^A
%              \marg{false\-branch}
%   checks whether \meta{character} is in \meta{character/mathcode/catcode
%   list} and chooses the appropriate branch.
%    \begin{macrocode}
\def\@ifinlist#1#2{\@tempswafalse
  \def\do##1##2##3{\ifnum`##1=`#2\relax\@tempswatrue\fi}#1%
  \if@tempswa\let\next\@firstoftwo\else\let\next\@secondoftwo\fi\next}
%    \end{macrocode}
% \end{macro}
%
% \subsubsection{Setting up the Data Structures}
% \label{sec:SettingUpTheDataStructures}
%
% \begin{macro}{\@addligto}
% \cmd{\@addligto}\marg{character/mathcode/catcode
%   list}\marg{character} inserts (replaces) or adds the "mathcode"
%   and "catcode" information into the \meta{character/mathcode/catcode
%   list}:
%    \begin{macrocode}
\def\@addligto#1#2{%
  \@ifinlist#1#2{\def\do##1##2##3{\noexpand\do\noexpand##1%
      \ifnum`##1=`#2 {\the\mathcode`#2}{\the\catcode`#2}%
      \else{##2}{##3}\fi}%
    \edef#1{#1}}%
  {\def\do##1##2##3{\noexpand\do\noexpand##1%
      \ifnum`##1=`#2 {\the\mathcode`#2}{\the\catcode`#2}%
      \else{##2}{##3}\fi}%
    \edef#1{#1\do#2{\the\mathcode`#2}{\the\catcode`#2}}}}
%    \end{macrocode}
% \end{macro}
% \begin{macro}{\@addligtolists}
% \begin{macro}{\@addligtofollowlist}
% \errorcontextlines=10
% \cmd{\@addligtolists}\marg{$c_1c_2\cdots{}c_n$} adds $c_1$ to the
% \cmd{\@domathligfirsts} list and the remaining to the \cmd{\@domathligfollows}
% list by only eating the first character and passing the remaining to
% \cmd{\@addligtofollowlist}:
%    \begin{macrocode}
\def\@addligtolists#1{\expandafter\@addligto
  \expandafter\@domathligfirsts
  \csname\string#1\endcsname\@addligtofollowlist}
\def\@addligtofollowlist#1{\ifx#1\@@\let\next\relax\else
  \def\next{\expandafter\@addligto
    \expandafter\@domathligfollows
    \csname\string#1\endcsname
    \@addligtofollowlist}\fi\next}
%    \end{macrocode}
% \end{macro}
% \end{macro}
% \begin{macro}{\@defligstep}
% \begin{macro}{\@def@ligstep}
% \cmd{\@defligstep}\marg{$c_1\cdots{}c_{i-1}$}\marg{$c_i$} defines one
% step in the parsing of a ligature character sequence: the
% "\@mathlig"$c_1\cdots c_i$ macro. The (possibly active) characters are
% turned into letters by applying \cmd{\string} until the end of the sequence
% is reached:
%    \begin{macrocode}
\def\@defligstep#1#2{\def\@tempa##1{\ifx##1\endcsname
    \expandafter\endcsname\else
    \string##1\expandafter\@tempa\fi}%
  \expandafter\@def@ligstep\csname @mathlig\@tempa#1#2\endcsname{#1#2}}
%    \end{macrocode}
% when the end of ALL the characters of the sequence (i.e.{} $c_1c_2\cdots
% c_n$) is reached---signalled by the \cmd{\@@} control
% sequence inserted by \cmd{\mathlig}---\cmd{\@def@ligstep} can define the macro
% "\@mathlig"$c_1c_2\cdots
% c_n$ (note that the following tokens in the input stream are the ones
% following the first parameter of a \cmd{\mathlig} command). Otherwise, the
% process is repeated by calling \cmd{\@defligstep} again.
%    \begin{macrocode}
\def\@def@ligstep#1#2#3{%
  \ifx#3\@@
    \def\next{\def#1}%
  \else
    \ifx#1\relax
      \def\next{\let#1\@mathliglink\@defligstep{#2}#3}%
    \else
      \def\next{\@defligstep{#2}#3}%
    \fi
  \fi\next}
%    \end{macrocode}
% \end{macro}
% \end{macro}
% \begin{macro}{\@setupfirstligchar}
% The first character, $c$, of a ligature sequence must receive special
% treatment: if it is already active, we must redefine it to check whether
% it is used inside or outside of math. When inside, it should expand to
% \cmd{\@startmathlig}$c$\SpecialUsageIndex{\@startmathlig}.
%    \begin{macrocode}
\def\@setupfirstligchar#1#2\@@{%
  \@ifactive{#1}{%
    \expandafter\expandafter\expandafter\@mathligredefactive
    \expandafter\string\expandafter#1\expandafter{#1}{#1}}%
%    \end{macrocode}
% If on the other hand it is not active, we must define \emph{its active
% variant} to expand to \cmd{\@startmathlig}$c$. This cannot be done directly,
% as we cannot change the "catcode"s of characters once they've been read,
% so we call \cmd{\@defactive}:
%    \begin{macrocode}
  {\@defactive#1{\@startmathlig #1}\@namedef{@mathlig#1}{#1}}}
%    \end{macrocode}
% \end{macro}
% \begin{macro}{\@mathligredefactive}
% The use of \cmd{\@mathligredefactive} is tricky: the macro needs three
% versions of the character to be defined: an active (for defining), a
% letter (for \cmd{\@namedef}ining) and an expanded version (for wrapping the
% math mode check stuff around). thus it must be called by
% \cmd{\@mathligredefactive}\marg{letter}\marg{expansion}\marg{active
% character}.
%    \begin{macrocode}
\def\@mathligredefactive#1#2#3{%
  \def#3{{}\ifmmode\def\next{\@startmathlig#1}\else
    \def\next{#2}\fi\next}%
  \@namedef{@mathlig#1}{#2}}
%    \end{macrocode}
% \end{macro}
% \begin{macro}{\@defactive}
% \begin{macro}{\@definemathlig}
% The only way we can get an active version of a character $c$ is by
% storing a list of possible characters, each with catcode 13
% (active). Actually, what we do is to have a list of macros,
% \cmd{\@definemathlig}$c$\marg{expansion text} that will define the
% active character $c$ to expand to \meta{expansion text}.
%    \begin{macrocode}
\def\@defactive#1{\@ifundefined{@definemathlig\string#1}%
  {\@latex@error{Illegal first character in math ligature}
    {You can only use \@firstmathligs\space as the first^^J
      character of a math ligature}}%
  {\csname @definemathlig\string#1\endcsname}}

{\def\@firstmathligs{}\def\do#1{\catcode`#1=\active
    \expandafter\gdef\expandafter\@firstmathligs
    \expandafter{\@firstmathligs\space\string#1}\next}
  \def\next#1{\expandafter\gdef\csname
    @definemathlig\string#1\endcsname{\def#1}}
%    \end{macrocode}
% Well, this is the list of characters I found it reasonable to expect as
% first characters of a ligature sequence. Characters like "$" "&" "^" "_"
% "#" "\" and "%" don't really make sense. All these characters are put
% into a comma separated list,
% \cmd{\@firstmathligs}\DescribeMacro{\@firstmathligs}.
%    \begin{macrocode}
  \do{"}"\do{@}@\do{/}/\do{(}(\do{)})\do{[}[\do{]}]\do{=}=
  \do{?}?\do{!}!\do{`}`\do{'}'\do{|}|\do{~}~\do{<}<\do{>}>
  \do{+}+\do{-}-\do{*}*\do{.}.\do{,},\do{:}:\do{;};}
%    \end{macrocode}
% \end{macro}
% \end{macro}
%
% \subsubsection{Parser Algorithm}
% \label{sec:ParserAlgorithm}
%
% During parsing, 
% \begin{itemize}
%   \item \DescribeMacro{\@seentoks}\cmd{\@seentoks} holds the characters seen
%     so far. 
%   \item \DescribeMacro{\@lastvalidmathlig}\cmd{\@lastvalidmathlig} holds the
%     macro corresponding to the longest 
%     valid math ligature character sequence seen so far
%   \item \DescribeMacro{\@pushedtoks}\cmd{\@pushedtoks} holds the remaining
%     characters seen that are not a 
%     part of the valid ligature character sequence
% \end{itemize}
%    \begin{macrocode}
\newtoks\@pushedtoks
\newtoks\@seentoks
%    \end{macrocode}
%
% The overall algorithm is as follows:
%
% \begin{itemize}
%   \item [1] Let $i=1$. A character $c_i$ in \cmd{\@domathligfirsts} triggers
%     the following steps:
%   \item [2] 
%        \begin{tabbing}
%        \cmd{\@seentoks} := [ ] \\
%        \cmd{\@lastvalidmathlig} := \{\} \\
%        \cmd{\@pushedtoks} := [ ]
%        \end{tabbing}
%   \item [3]
%     \begin{tabbing}\qquad\=\qquad\=\qquad\=\kill
%        if the macro \cmd{\@mathlig}$c_1c_2\cdots c_i$ is defined then \\
%          \>if \cmd{\@mathlig}$c_1c_2\cdots c_i$ is a \cmd{\@mathliglink} then \\
%            \>\>\cmd{\@pushedtoks} := \cmd{\@pushedtoks} ++ [$c_i$] \\
%          \>else \\
%            \>\>\cmd{\@lastvalidmathlig} := \cmd{\@mathlig}$c_1c_2\cdots c_i$ \\
%            \>\>\cmd{\@pushedtoks} := [ ] \\
%          \>\cmd{\@seentoks} := \cmd{\@seentoks} ++ [$c_i$] \\
%        else \\
%          \>disable ligatures \\
%          \>expand \cmd{\@lastvalidmathlig} \\
%          \>enable ligatures \\
%          \>put the \cmd{\@pushedtoks} and $c_i$ on the input stream \\
%          \>go to 1
%     \end{tabbing}
%   \item [4] Let $i=i+1$; read next character $c_i$ and go to 3.
% \end{itemize}
% \begin{macro}{\@startmathlig}
% \begin{macro}{\@trymathlig}
% \begin{macro}{\@@trymathlig}
% \begin{macro}{\@try@mathlig}
% \begin{macro}{\@exitmathlig}
% All this is accomplished by the following macros, starting with
% \cmd{\@startmathlig}: 
%    \begin{macrocode}
\def\@startmathlig{\def\@lastvalidmathlig{}\@pushedtoks{}%
  \@seentoks{}\@trymathlig}
\def\@trymathlig{\futurelet\next\@@trymathlig}
\def\@@trymathlig{\@ifcharacter\next{\@try@mathlig}{\@exitmathlig{}}}
\def\@exitmathlig#1{%
  \expandafter\@makemathligsnormal\@lastvalidmathlig\mathligson
  \the\@pushedtoks#1}
\def\@try@mathlig#1{%\typeout{char: #1 catcode: \the\catcode`#1
%^^A    \space pushed:\the\@pushedtoks
%^^A    \space seen:\the\@seentoks
%^^A    \space last\meaning\@lastvalidmathlig}%
  \@ifundefined{@mathlig\the\@seentoks#1}{\@exitmathlig{#1}}%
  {\expandafter\ifx
                 \csname @mathlig\the\@seentoks#1\endcsname
                 \@mathliglink
      \expandafter\@pushedtoks
        \expandafter=\expandafter{\the\@pushedtoks#1}%
    \else
      \expandafter\let\expandafter\@lastvalidmathlig
      \csname @mathlig\the\@seentoks#1\endcsname
      \@pushedtoks={}%
    \fi
    \expandafter\@seentoks\expandafter=\expandafter%
    {\the\@seentoks#1}\@makemathligsactive\obeyspaces\@trymathlig}}
%    \end{macrocode}
% \end{macro}
% \end{macro}
% \end{macro}
% \end{macro}
% \end{macro}
%
% \subsubsection{Compatibility with \texttt{amsmath} package}
%
% \begin{macro}{\patch@newmcodes@}
%   The \texttt{amsmath} package by AMS uses some non-alphanumeric
%   characters to produce for instance extended arrows.  Consequently
%   the  \cmd{\newmcodes@} in \texttt{amsopn.sty} (2.01) fails with an error message if
%   the hyphen character has mathcode \"8000. So we in provide a patch
%   (suggested by Michael John Downes of AMS<). 
%    \begin{macrocode}
\edef\patch@newmcodes@{%
  \mathcode\number`\'=39
  \mathcode\number`\*=42
  \mathcode\number`\.=\string "613A
  \mathchardef\noexpand\std@minus=\the\mathcode`\-\relax
  \mathcode\number`\-=45
  \mathcode\number`\/=47
  \mathcode\number`\:=\string "603A\relax
}
\AtBeginDocument{\let\newmcodes@=\patch@newmcodes@}
%</ligature>
%    \end{macrocode}
% \changes{2.0$\epsilon$}{2002/06/13}{Provided patch to make \semantic compatible with \texttt{amsmath} v. 2.01}
% \end{macro}
%
% \subsubsection{ToDo}
% \label{sec:ToDo}
% 
% \begin{itemize}
% \item Make removing of math ligatures possible (tricky!)
% \item Make it possible to define a single char as a ligature
%       (redefinition)
% \item Check the use of \cmd{\@makemathligsactive}: is it possible to
%       replace it by \cmd{\mathligson}?
% \end{itemize}
%
% \subsection{Inference Rules}
%
%    \begin{macrocode}
%<*inference>
\TestForConflict{\@@tempa,\@@tempb,\@adjustPremises,\@inference}
\TestForConflict{\@inferenceBack,\@inferenceFront,\@inferenceOrPremis}
\TestForConflict{\@premises,\@processInference,\@processPremiseLine}
\TestForConflict{\@setLengths,\inference,\predicate,\predicatebegin}
\TestForConflict{\predicateend,\setnamespace,\setpremisesend}
\TestForConflict{\setpremisesspace,\@makeLength,\@@space}
\TestForConflict{\@@aLineBox,\if@@shortDivider}
%    \end{macrocode}
% \begin{macro}{\@makeLength}
%   \changes{1.1}{1995/11/12}{Redefined the lengths commands, so that the lengths are evaluated each time}^^A
% \begin{macro}{\@setLengths}
% \changes{1.1$\beta$}{1995/11/21}{Added setting of parameters for line skipping in \cs{@setLengths}}
%   First I define two auxiliary macros to facilitate the use of the lengths
%   controlling the appearance of an inference rule.  My overall aim is to
%   allow the use of relative units ("em" and "ex"). To accomplish this, the
%   lengths have to be evaluated before the setting of every rule. As
%   there are only a few lengths, it could been have been simpler and less
%   general, but I found it inspiring to work out a general solution.
%
%   \cmd{\@makelength}\marg{users name}\marg{internal name}\marg{default
%       value}\marg{stretch} does all the definitions associated with
%   making a new length: defines a new length \cs{@@\meta{internal name}}, makes
%   a command to evaluate it (with the current choice of font)
%   \cs{@set\meta{internal name}} and makes the users command to change the
%   length \cs{set\meta{users name}}.  \meta{default value} is---of course---the
%   normal value used for the length, while \meta{stretch} is the stretch
%   parameter in case the premise should be set wider than its natural width.
%
%   The macro \cmd{\@setLengths} is used to evaluate all the lengths. When a new
%   length is made using \cmd{\@makelength}, the name of its evaluation macro,
%   \cs{@set\meta{internal name}}, is added. 
%    \begin{macrocode}
\newtoks\@@tempa 
\newtoks\@@tempb 
\newcommand{\@makeLength}[4]{
  \@@tempa=\expandafter{\csname @@#2\endcsname}
  \@@tempb=\expandafter{\csname @set#2\endcsname} %
  \expandafter \newlength \the\@@tempa 
  \expandafter \newcommand \the\@@tempb {} 
  \expandafter \newcommand \csname set#1\endcsname[1]{}
  \expandafter \xdef \csname set#1\endcsname##1%
    {{\dimen0=##1}%
      \noexpand\renewcommand{\the\@@tempb}{%
        \noexpand\setlength{\the \@@tempa}{##1 #4}}%
    }%
  \csname set#1\endcsname{#3}
  \@@tempa=\expandafter{\@setLengths} %
  \edef\@setLengths{\the\@@tempa \the\@@tempb} %
  }

\newcommand{\@setLengths}{%
  \setlength{\baselineskip}{1.166em}%
  \setlength{\lineskip}{1pt}%
  \setlength{\lineskiplimit}{1pt}}
%    \end{macrocode}
%   The first lines in \cmd{\@makelength} builds the name of the length in
%   \cmd{\@@tempa} and the macro to evaluate it in \cmd{\@@tempb}---this requires some
%   playing with \cmd{\csname}---and declares the corresponding length and command.
%   Then the users command is builded: It contains a test "{\dimen0 = #1}" to
%   ensure that the given parameter  is, in fact, a length and then it
%   redefines the evaluating command so that the length is the length
%   provided by the user, and a possibly stretch which is defined below and
%   cannot be altered by the user. At last the evaluating command is added to
%   \cmd{\@setLengths}---the inspiration to this code I got from
%   \cite[378]{texbook}.
%
%   The distance between the lines of premises is set by \TeX\ using its normal
%   lineskipping algorithm. As some environments, e.g.\ "tabular", sets all the
%   lineskipping  parameters, \cmd{\baselineskip}, \cmd{\lineskip} and 
%   \cmd{\lineskiplimit}, to zero it is necessary to set them in \cmd{\@setLengths}.
% \end{macro}
% \end{macro}
%
% \begin{macro}{\setpremisesspace}
%   \changes{1.0}{1995/10/18}{Changed from 10"pt" to 15"pt"}^^A
%   \changes{1.2$\alpha$}{1996/01/31}{Changed to 1.5"em"}
% \begin{macro}{\setpremisesend}
%   \changes{1.2$\alpha$}{1996/01/31}{Changed to .75"em"}
% \begin{macro}{\setnamespace}
%   \changes{1.01}{1995/11/07}{Introduced \cs{name\-space}}^^A
%   This is followed by the definition of some auxiliary internal registers:
%   \label{space setting}
%    \begin{macrocode}
\@makeLength{premisesspace}{pSpace}{1.5em}{plus 1fil}
\@makeLength{premisesend}{pEnd}{.75em}{plus 0.5fil}
\@makeLength{namespace}{nSpace}{.5em}{}
%</inference>
%    \end{macrocode}
% \end{macro}
% \end{macro}
% \end{macro}
%
% Then comes some auxiliary internal registers
% \changes{1.1$\delta$}{1995/12/01}{Introduced \cs{@@space} for use in comparisons}
%    \begin{macrocode}
%<*general>
\newdimen\@@maxwidth 
\newbox\@@pLineBox
\newbox\@@cBox 
\newbox\@@pBox 
\newif\if@@moreLines
%</general>
%<*inference>
\newbox\@@aLineBox 
\newif\if@@shortDivider
\newcommand{\@@space}{ }
%    \end{macrocode}
% \begin{tabular}{lp{9.4cm}}
%   \cmd{\@@maxwidth} & The largest width of a premise/ \\
%   \cmd{\@@cBox} & Holds the conclusion when it has been built \\
%   \cmd{\@@pBox} & The premises is built in this register  \\
%   \cmd{\@@pLineBox} & Used to build a single line of the premise \\
%   \cmd{\@@aLineBox} & Contains the line to be adjusted  \\
%   \cmd{\@@moreLines} & Flag telling if there is more lines of premises to process \\
%   \cmd{\@@moreLines} & Flag telling the divider should only be the length of
%   the conclusion \\
%   \cmd{\@@space} & Macro with a single space---used for comparison.
% \end{tabular}
%
% \begin{macro}{\predicate}
% \begin{macro}{\predicatebegin}
% \changes{1.0}{1995/10/18}{Changed the name to avoid conflict with \LaTeX}
% \changes{2.0}{1998/06/05}{Changed the default setting to "$" such that
% the premises are set in math mode.}
% \begin{macro}{\predicateend}
% \changes{1.0}{1995/10/18}{Changed the name to avoid conflict with \LaTeX}
% \changes{2.0}{1998/06/05}{Changed the default setting to "$" such that
% the premises are set in math mode.}
%   \cmd{\predicate} controls the setting of a single predicate cf.\ 
%   p.~\pageref{pattern matching}.
%    \begin{macrocode}
\newcommand{\predicate}[1]{\predicatebegin #1\predicateend}
\newcommand{\predicatebegin}{$}
\newcommand{\predicateend}{$}
%    \end{macrocode}
% \end{macro}
% \end{macro}
% \end{macro}
%
% \subsection{Typesetting Inference Rules}
%
%   These macros typesets inference rules.  The macros are used nested,
%   which means that \TeX{}'s stack is used extensively.  In
%   particular, these put a heavy burden on the paramter stack. To
%   circumvent this the macros are splitted such that each macro only 
%   parses one argument at a time.  Then only the arguments
%   containing the premise are saved.   It is still worth considering 
%   ways to remove more nesting of macros with arguments, for
%   instance one could probaply test if the following token was a
%   begin group and then redefine the meaning of~"&" and~"\\".  The
%   drawback is that it then might be necessary to use active
%   characters.
%
% \begin{macro}{\inference}
% \changes{1.0}{1995/18/10}{Changed some names due to a conflict with \LaTeX's \cs{rule}}
% \changes{1.01}{1995/11/07}{Inserted a space in front of the name using \cs{name\-space}}
% \changes{1.1}{1995/11/15}{Removed \cs{@pInference}}
% \changes{2.0}{1998/05/20}{Added check for starred version}
%  This is the entry macro.  It starts the parameter parsig by testing 
%  for the starred version; this is stored in the value of
%  "\if@@shortDivider".  It starts a group that the full inference
%  with names is saved in.
%    \begin{macrocode}
\def\inference{%
  \@@shortDividerfalse
  \expandafter\hbox\bgroup
  \@ifstar{\@@shortDividertrue\@inferenceFront}%
          \@inferenceFront
}
%    \end{macrocode}
% \end{macro}
% 
% \begin{macro}{\@inferenceFront}
%   This macro testes for an optional argument to the left of the
%   inference. 
%    \begin{macrocode}
\def\@inferenceFront{%
  \@ifnextchar[%
     {\@inferenceFrontName}%
     {\@inferenceMiddle}%
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@inferenceFrontName}
%   This maacro typesets an optional argument with the apropriate
%   space and then passes control to the typesetting of the inference
%    \begin{macrocode}
\def\@inferenceFrontName[#1]{%
  \setbox3=\hbox{\footnotesize #1}%
  \ifdim \wd3 > \z@
    \unhbox3%
    \hskip\@@nSpace
  \fi
  \@inferenceMiddle
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@inferenceMiddle}
%   It typesets the premises in the box~\cmd{\@@pBox}.
%    \begin{macrocode}
\long\def\@inferenceMiddle#1{%
  \@setLengths%
%    \end{macrocode}
%   Initialises the length parameters according to the current font
%   size.
%    \begin{macrocode}
  \setbox\@@pBox=
    \vbox{%
      \@premises{#1}%
      \unvbox\@@pBox
    }%
%    \end{macrocode}
%   This typesets the premises.  It is necessary to have the
%   typesetting in its own group to prevent interferring with a
%   premise being typeset on the outer levels.  We therefore typeset
%   the premises inside a group and moves them one level out by
%   \cmd{\unvbox} inside a~\cmd{\vbox}.
%    \begin{macrocode}
  \@inferenceBack
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@inferenceBack}
%  This macro typesets the conclusion, sets up the premises on top of
%  the conclusion and tests for an additional argument.
%    \begin{macrocode}
\long\def\@inferenceBack#1{%
  \setbox\@@cBox=%
   \hbox{\hskip\@@pEnd \predicate{\ignorespaces#1}\unskip\hskip\@@pEnd}%
%    \end{macrocode}
%  Typeset the conclusion in its own box.  In this way we are able to
%  compare the lengths of the two.
%    \begin{macrocode}
  \setbox1=\hbox{$ $}%
%    \end{macrocode}
%  We then ensure that we have the right math fonts loaded by changing 
%  to math mode.
%    \begin{macrocode}
  \setbox\@@pBox=\vtop{\unvbox\@@pBox
                 \vskip 4\fontdimen8\textfont3}%
  \setbox\@@cBox=\vbox{\vskip 4\fontdimen8\textfont3%
                 \box\@@cBox}%
%    \end{macrocode}
%  Add the space corresponding to a fraction bar in a display below
%  the premises and above the conclusion.  
%    \begin{macrocode}
  \if@@shortDivider
%    \end{macrocode}
%  If the user want a short divider, we typeset the premises and the
%  conclusion in a box with the width of the biggest of the two, but
%  ensures that the divider only gets the width of the
%  conclusion. Anyway, this is not really what we want.  We should
%  somehow know the length of the previous premise, but I have not
%  worked out the algorithm yet.
%    \begin{macrocode}
    \ifdim\wd\@@pBox >\wd\@@cBox%
      \dimen1=\wd\@@pBox%
    \else%
      \dimen1=\wd\@@cBox%
    \fi%
    \dimen0=\wd\@@cBox%
    \hbox to \dimen1{%
      \hss
      $\frac{\hbox to \dimen0{\hss\box\@@pBox\hss}}%
        {\box\@@cBox}$%
      \hss
    }%
  \else
%    \end{macrocode}
%   If plain style, we simply typeset the premise on top of the
%   conclusion. 
%    \begin{macrocode}
    $\frac{\box\@@pBox}%
          {\box\@@cBox}$%
  \fi
  \@ifnextchar[%
     {\@inferenceBackName}%{}%
     {\egroup}
}
%    \end{macrocode}
%  We end the typesetting by testing for an optional argument.  If
%  this is not provided we simply ends the group started by
%  \cmd{\inference}. 
% \end{macro}
%
% \begin{macro}{\@inferenceBackName}
%   Here we typeset an additional argument
%    \begin{macrocode}
\def\@inferenceBackName[#1]{%
  \setbox3=\hbox{\footnotesize #1}%
  \ifdim \wd3 > \z@
    \hskip\@@nSpace
    \unhbox3%
  \fi
%    \end{macrocode}
% and end the group started by \cmd{\inference}.
%    \begin{macrocode}
  \egroup
}
%    \end{macrocode}
% \end{macro}
%
% \subsubsection{Processing of Premises}
%
% Then comes the code that processes a list of premises and set them in
% \cmd{\@@pBox}. I do a lot of gambots adding and deleting extra tokens so that
% \TeX's pattern mathcing on macro arguments can be used to find nestings,
% linebreaks etc.\ as I belive this to be faster than actually reading 
% one token at a time using \TeX\ primitives.
%
% \begin{macro}{\@premises}
%   \changes{1.1}{1995/11/25}{Initially set \cs{@max\-width} equal to the width of the conclusion}
% \changes{1.1$\gamma$}{1995/11/12}{Changed \cs{@premises} so the
% premises can extend over several lines}
%   This initialises the processing of the list of premises line by line. A
%   line is recognised in \cmd{\@processPremises}, which does the processing by
%   matching on its terminating "\\". Since there is not a "\\" after the last
%   premise, I insert \verb*"\\ \end" as an end marker after the list of
%   premises. In this way, \cmd{\@processPremises} can assume that every line is
%   followed by "\\", and if this is followed by \cmd{\end}, it has reached the
%   end.
%    \begin{macrocode}
\newcommand{\@premises}[1]{%
  \setbox\@@pBox=\vbox{}%
  \dimen\@@maxwidth=\wd\@@cBox%
  \@processPremises #1\\\end%
  \@adjustPremises%
}
%    \end{macrocode}
%   In cases where there---as an example---are two narrow premises on one line
%   and a broad one on another line. it would look strange if the distance between
%   the two premises were fixed. I therefore add som strechable glue
%   between the premises and at the end (with half the strechability) 
%   cf.~p.~\pageref{space setting}. To accomplish this, I need to know the 
%   width of the widest line, but this can only be found while processing
%   the premises. It is saved in \cmd{\@@maxwidth} so that \cmd{\@adjustPremises} adjusts
%   all lines to it. By initially setting \cmd{\@@maxwidth} to the width of the
%   conclusion, no line will become narrower than the conclusion. And due to the
%   glue, the premises will appear centered if the conclusion is wider than the
%   premises.
% \end{macro}
%
% \begin{macro}{\@adjustPremises}
%   This macro adjusts  the lines of premises to \cmd{\@@maxwidth}:
%    \begin{macrocode}
\newcommand{\@adjustPremises}{%
  \setbox\@@pBox=\vbox{%
    \@@moreLinestrue %
    \loop %
      \setbox\@@pBox=\vbox{%
        \unvbox\@@pBox %
        \global\setbox\@@aLineBox=\lastbox %
      }%
      \ifvoid\@@aLineBox %
        \@@moreLinesfalse %
      \else %
        \hbox to \dimen\@@maxwidth{\unhbox\@@aLineBox}%
      \fi % 
    \if@@moreLines\repeat%
  }%
}
%    \end{macrocode}
%   The lines set are put in \cmd{\@@pBox} in reverse order. They are taken from
%   \cmd{\@@pBox} one by one by emptying (\cmd{\unvbox}) \cmd{\@@pBox}, setting
%   \cmd{\@@aLineBox} to the last box in the vertical list just emptied and putting
%   the rest back in \cmd{\@@pBox}. I do not expect this to be as bas as it sounds,
%   because presumably the \cmd{\unvbox} is not a actual copying but only some
%   pointer operation, which can be done in constant time (cf.\ the hints on
%   \cite[120]{texbook}).
%   
%   All this is done inside a \cmd{\vbox} so the contents of \cmd{\@@aLineBox} can be
%   added to the list being build simply using "\hbox to "\lttdots\ (doing the
%   adjusting simultaneousnessly). Being inside a \cmd{\vbox} has the additional
%   advantage that \TeX\ is in internal vertical mode so that there
%   is added lineskip automaticly in accordance with \cmd{\baselineskip} etc.\ 
%   (cf.~\cite[80]{texbook}). As the macro is in no sense recursive, it is no
%   problem changing \cmd{\@aLineBox}  globally.
% \end{macro}
% 
% \begin{macro}{\@processPremises}\mbox{}^^A
% \changes{1.1$\beta$}{1995/11/21}{Fixed bug that made an empty premise sometimes contain \cs{pSpace}}
% \changes{1.1$\beta$}{1995/11/21}{Moved the processing of spaces to \cs{@inferenceOrPremis}}
%    \begin{macrocode}
\def\@processPremises#1\\#2\end{%
%    \end{macrocode}
%   This pattern splits the list of premises into the first
%   line (\#1---possibly empty) and the following lines
%   (\#2---possibly containing no lines).   
%    \begin{macrocode}
  \setbox\@@pLineBox=\hbox{}%
  \@processPremiseLine #1&\end%
  \setbox\@@pLineBox=\hbox{\unhbox\@@pLineBox \unskip}% 
%    \end{macrocode}
%   The first line is typesetted in \cmd{\@@pLineBox} and additional space 
%   is removed.  We use \cmd{\@processPremiseLine} that like
%   \cmd{\@processPremises} gets "&\end" added so that it recognizes the
%   end of line. After the line has been set   
%    \begin{macrocode}
  \ifdim \wd\@@pLineBox > \z@ %
%    \end{macrocode}
%   If the premise is not empty, we add it to \cmd{\@@pBox}, that when finished
%   will contain the lines (in reverse order---cf.~\cmd{\@adjustPremises}), and if
%   necessary \cmd{\@@maxwidth} is increased. 
%    \begin{macrocode}
    \setbox\@@pLineBox=%
      \hbox{\hskip\@@pEnd \unhbox\@@pLineBox \hskip\@@pEnd}%
    \ifdim \wd\@@pLineBox > \dimen\@@maxwidth %
      \dimen\@@maxwidth=\wd\@@pLineBox %
    \fi %
    \setbox\@@pBox=\vbox{\box\@@pLineBox\unvbox\@@pBox}%
  \fi %
%    \end{macrocode}
%  If there are more lines we process them.
%    \begin{macrocode}
  \def\sem@tmp{#2}%
  \ifx \sem@tmp\empty \else %
    \@ReturnAfterFi{%
      \@processPremises #2\end %
    }%
%    \end{macrocode}
%  \cmd{\@ReturnAfterFi} is a trick due to Heiko Oberdik to ensure that we 
%  get a tail recursive macro.
%    \begin{macrocode}
  \fi%
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@processPremiseLine}\mbox{}^^A
% \changes{1.1$\delta$}{1995/12/01}{Fixed bug that axioms could not be handled using pattern matching}
%    \begin{macrocode}
\def\@processPremiseLine#1&#2\end{%
%    \end{macrocode}
%   This pattern splits the line into the first premise (\#1---possibly
%   empty) and the following premises (\#2---possibly none). 
%    \begin{macrocode}
  \def\sem@tmp{#1}%
  \ifx \sem@tmp\empty \else%
    \ifx \sem@tmp\@@space \else%
    \setbox\@@pLineBox=%
      \hbox{\unhbox\@@pLineBox%
            \@inferenceOrPremis #1\inference\end%
            \hskip\@@pSpace}%
    \fi%
  \fi%
%    \end{macrocode}
%   If the first premise is non-empty, which in this context means that
%   it is neither empty nor a space (\verb*+& &+ should be regarded as an 
%   empty premise), it is typesetted using
%   \cmd{\@inferenceOrPremis}, and an appropriate spacing to the next premise is
%   added. Note that this space is also added after the last premise but then
%   removed again, when \LaTeX\ has returned to \cmd{\@processPremises}.
%    \begin{macrocode}
  \def\sem@tmp{#2}%
  \ifx \sem@tmp\empty \else%
    \@ReturnAfterFi{%
      \@processPremiseLine#2\end%
    }%
  \fi%
}
%    \end{macrocode}
%  If there are any premises in the
%   \emph{following premises} we use \cmd{\@processPremisesLine} 
%   tail recursively.
% \end{macro}
%
% \begin{macro}{\@inferenceOrPremis}
%   "@inferenceOrPremis" decides wether there is a nested \cmd{\@inference} in a
%   premise. 
%    \begin{macrocode}
\def\@inferenceOrPremis#1\inference{%
  \@ifnext \end
    {\@dropnext{\predicate{\ignorespaces #1}\unskip}}%
    {\@processInference #1\inference}%
}
%    \end{macrocode}
%   The calling macro appends the argument with "\inference \end". We
%   then test whether \cmd{\inference} followd by the token~\cmd{\end}.  If
%   this is the case, we conclude that premise did not originally 
%   contain a nesting (\emph{ie} \cmd{\inference}). In this case, 
%   the \cmd{\end}-token is removed and the premise is set using
%   \cmd{\predicate}. Otherwise, \cmd{\inference}
%   \cmd{\end} is removed and the inference rule is set---all this is done by
%   \cmd{\@processInference}.
% \end{macro}
%
% \begin{macro}{\@processInference}
%   Remove \cmd{\inference} \cmd{\end} from the testing for a nested
%   appearance of an inference rule.  Typesets the inference and
%   adjust its vertical placement  such that the baseline of its
%   conclusion match the baseline of a plain premise.
%    \begin{macrocode}
\def\@processInference#1\inference\end{%
  \ignorespaces #1%
%    \end{macrocode}
%  Typesets the inference rule and returns the full inference rule in
%  a box.
%    \begin{macrocode}
  \setbox3=\lastbox
  \dimen3=\dp3
  \advance\dimen3 by -\fontdimen22\textfont2
  \advance\dimen3 by \fontdimen8\textfont3
  \expandafter\raise\dimen3\box3%  
%    \end{macrocode}
%  We take the previously type setted inference rule and lifts it by
%  its depth modulo the extra depth that it has got from be lowered
%  by a fraction.
%    \begin{macrocode}
}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@ReturnAfterFi}
%   This is a small macro due to Heiko Oberdik.  It ensure that we get 
%   a tail recursive function even inside an "\if"-construction.
%    \begin{macrocode}
\long\def\@ReturnAfterFi#1\fi{\fi#1}
%    \end{macrocode}
%  It finds the commands up till the enclosing "\fi", closes the "\if" 
%  and executes the commands.
% \end{macro}
%
%    \begin{macrocode}
%</inference>
%    \end{macrocode}
%
% \subsubsection{ToDo}
% 
% \begin{itemize}
% \item Find a way to made the conclusion bar as wide as the
%       conclusion of the premises (tricky).
% \item Get it to work correctly with amsmath and mathbbol
% \end{itemize}
%
% \subsection{T-diagrams}
%
%    \begin{macrocode}
%<*Tdiagram>
\TestForConflict{\@getSymbol,\@interpreter,\@parseArg,\@program}
\TestForConflict{\@putSymbol,\@saveBeforeSymbolMacro,\compiler}
\TestForConflict{\interpreter,\machine,\program,\@compiler}
%</Tdiagram>
%    \end{macrocode}
% First some auxilary registers are reserved:
%    \begin{macrocode}
%<*general>
\newif\if@@Nested \@@Nestedfalse 
%</general>
%<*Tdiagram>
\newif\if@@Left 
\newif\if@@Up
\newcount\@@xShift 
\newcount\@@yShift 
\newtoks\@@symbol
\newtoks\@@tempSymbol
%    \end{macrocode}
% \begin{tabular}{lp{9.2cm}}
%   \cmd{\@@Nested} & Flag telling if the current diagram is nested within another \\
%   \cmd{\@@Left}   & Flag telling that a nested diagram should be drawn to the
%                 left---if not set, the nested diagram is drawn to the right \\
%   \cmd{\@@Right}  & Flag telling that a nested diagram should be drawn above 
%                 the current one---if not set, the diagram is drawn below
%                 the current one \\
%   \cmd{\@@xShift} & Horizontal shift from the local origin to the starting
%                 position in units of \cmd{\unitlength}. \\
%   \cmd{\@@yShift} & Vertical shift from the local origin to the starting
%                 position in units of \cmd{\unitlength} \\
%   \cmd{\@@Symbol} & The current machine symbol (i.e.\ the letter designating
%                 the programme/machine) \\
%   \cmd{\@@tempSymbol} & Used as temporary storage for different symbols 
% \end{tabular}
% 
% When \LaTeX's \cmd{\put} command is invoked, it raises a \cmd{\hbox} to
% the given offset, giving it height zero, and puts a \cmd{\hss} in the end
% so that it will end up with zero width too. It expands the "picture" command
% given in "{"\lttdots"}" just before the \cmd{\hss}, so they can be drawn
% from a local origin (given as coordinates to \cmd{\put}). The
% diagram commands are adapted to this scheme. Thus they are all constructed
% according to a common scheme:
% \begin{itemize}
% \item The offset (x in "count1" and y in "count2") from the local
%   origin to the starting position is calculated: If the diagram is
%   \emph{not} nested, the bottom should be centered around the position
%   given by \cmd{\put}. If the diagram  is nested, the bottom should
%   be at the current vertical position, if the diagram is to be drawn
%   \emph{upwards}. Conversely, the top should be at the current vertical
%   position if the diagram is to be drawn \emph{downwards}. If the
%   diagram should go to the \emph{left}, the right side should be at
%   the current horizontal position, and conversely.
% \item A \cmd{\hbox} is shifted to the given offset using \cmd{\hskip} and
%   \cmd{\raise}. Inside the box  the frame of the diagram is drawn first.
%   This is done using the \cmd{\put}, \cmd{\line} and other
%   "picture" commands. This relies on the way the
%   "picture" commands are construtced. It is admittely a little
%   bad style to use the commands in a non-documented ways, but it takes up a
%   little less memory, and I would like later to implement most of the
%   commands using rules, which would be faster.
% 
% \item The parameters are parsed. This is done in a specialized macro, to
%   which the position and orientation (\emph{ie} up and left) of a
%   possible nested diagram, and the coordinates for the symbol in the
%   current diagram are given.  The macro will examine the argument, and if it
%   consists of letters, it is considered a language symbol and is
%   set in the appropriate place. If itis a macro, however, the nested diagram
%   will be drawn, returning the language symbol using the global register
%   \cmd{\@@symbol}, which afterwards is set inside the diagram.
% 
% \item If the diagram is nested, it is finally ensure, that \cmd{\@@symbol}
%   is set globally accordingly to the orientation. Thus it returns
%   the symbol to the ``calling'' diagram.
% \end{itemize}
% 
% Most of the translation diagrams are coded with a small stup, that
% packs the arguments (that are separated by commas) followed by an \cmd{\end},
% so that \TeX's pattern matching can separate them.
% 
% \begin{macro}{\compiler}
% \begin{macro}{\@compiler}\mbox{}
% \changes{1.2$\alpha$}{1996/27/01}{Rewritten to fit with a "picture"-environment and nesting of diagrams}
%    \begin{macrocode}
\newcommand{\compiler}[1]{\@compiler#1\end}
\def\@compiler#1,#2,#3\end{%
  \if@@Nested %
    \if@@Up %
    \@@yShift=40 \if@@Left \@@xShift=-50 \else \@@xShift=-30 \fi
    \else%
      \@@yShift=20 \@@xShift =0 %
    \fi%
  \else%
    \@@yShift=40 \@@xShift=-40%
    \fi
  \hskip\@@xShift\unitlength\raise \@@yShift\unitlength\hbox{%
    \put(0,0){\line(1,0){80}}%
    \put(0,-20){\line(1,0){30}}%
    \put(50,-20){\line(1,0){30}}%
    \put(30,-40){\line(1,0){20}}%
    \put(0,0){\line(0,-1){20}}%
    \put(80,0){\line(0,-1){20}}%
    \put(30,-20){\line(0,-1){20}}%
    \put(50,-20){\line(0,-1){20}}%
    \put(30,-20){\makebox(20,20){$\rightarrow$}} %
   {\@@Uptrue \@@Lefttrue \@parseArg(0,-20)(5,-20)#1\end}%
   \if@@Up \else \@@tempSymbol=\expandafter{\the\@@symbol}\fi
   {\@@Uptrue \@@Leftfalse \@parseArg(80,-20)(55,-20)#3\end}%
   {\@@Upfalse \@@Lefttrue \@parseArg(50,-40)(30,-40)#2\end}%
   \if@@Up \@@tempSymbol=\expandafter{\the\@@symbol}\fi
    \if@@Nested \global\@@symbol=\expandafter{\the\@@tempSymbol} \fi%
  }%
}
%    \end{macrocode}
% \end{macro} 
% \end{macro} 
%
% \begin{macro}{\interpreter}
% \begin{macro}{\@interpreter}\mbox{}
% \changes{1.0}{1995/18/10}{Translated command names from danish to english}
% \changes{1.2$\alpha$}{1996/27/01}{Rewritten to fit with a "picture"-environment and nesting of diagrams}
%    \begin{macrocode}
\newcommand{\interpreter}[1]{\@interpreter#1\end}
\def\@interpreter#1,#2\end{%
  \if@@Nested %
    \if@@Up %
    \@@yShift=40 \if@@Left \@@xShift=0 \else \@@xShift=20 \fi
    \else%
      \@@yShift=0 \@@xShift =0 %
    \fi%
  \else%
    \@@yShift=40 \@@xShift=10%
    \fi
  \hskip\@@xShift\unitlength\raise \@@yShift\unitlength\hbox{%
    \put(0,0){\line(-1,0){20}}%
    \put(0,-40){\line(-1,0){20}}%
    \put(0,0){\line(0,-1){40}}%
    \put(-20,0){\line(0,-1){40}}%
   {\@@Uptrue \@@Lefttrue \@parseArg(0,0)(-20,-20)#1\end}%
   \if@@Up \else \@@tempSymbol=\expandafter{\the\@@symbol}\fi
   {\@@Upfalse \@@Lefttrue \@parseArg(0,-40)(-20,-40)#2\end}%
   \if@@Up \@@tempSymbol=\expandafter{\the\@@symbol}\fi
    \if@@Nested \global\@@symbol=\expandafter{\the\@@tempSymbol} \fi%
  }%
}
%    \end{macrocode}
% \end{macro} 
% \end{macro} 
% 
% \begin{macro}{\program}
% \begin{macro}{\@program}\mbox{}
% \changes{1.2$\alpha$}{1996/27/01}{Command added}
%    \begin{macrocode}
\newcommand{\program}[1]{\@program#1\end}
\def\@program#1,#2\end{%
  \if@@Nested %
    \if@@Up %
    \@@yShift=0 \if@@Left \@@xShift=0 \else \@@xShift=20 \fi
    \else%
      \PackageError{semantic}{%
        A program cannot be at the bottom}
        {%
          You have tried to use a \protect\program\space as the
          bottom\MessageBreak parameter to \protect\compiler,
          \protect\interpreter\space or \protect\program.\MessageBreak
         Type <return> to proceed --- Output can be distorted.}%
    \fi%
  \else%
    \@@yShift=0 \@@xShift=10%
    \fi
  \hskip\@@xShift\unitlength\raise \@@yShift\unitlength\hbox{%
    \put(0,0){\line(-1,0){20}}%
    \put(0,0){\line(0,1){30}}%
    \put(-20,0){\line(0,1){30}}%
    \put(-10,30){\oval(20,20)[t]}%
    \@putSymbol[#1]{-20,20}%
   {\@@Upfalse \@@Lefttrue \@parseArg(0,0)(-20,0)#2\end}%
  }%
}
%    \end{macrocode}
% Note that a little code that reports errors if the
% command is used wrongly, is incorporated.
% \end{macro} 
% \end{macro} 
% 
% \begin{macro}{\machine}\mbox{}
% \changes{1.2$\alpha$}{1996/27/01}{Command added}
%    \begin{macrocode}
\newcommand{\machine}[1]{%
  \if@@Nested %
    \if@@Up %
      \PackageError{semantic}{%
        A machine cannot be at the top}
        {%
          You have tried to use a \protect\machine\space as a
          top\MessageBreak parameter to \protect\compiler or
          \protect\interpreter.\MessageBreak
         Type <return> to proceed --- Output can be distorted.}%
       \else \@@yShift=0 \@@xShift=0
    \fi%
  \else%
    \@@yShift=20 \@@xShift=10%
    \fi
  \hskip\@@xShift\unitlength\raise \@@yShift\unitlength\hbox{%
    \put(0,0){\line(-1,0){20}} \put(-20,0){\line(3,-5){10}}
    \put(0,0){\line(-3,-5){10}}%
   {\@@Uptrue \@@Lefttrue \@parseArg(0,0)(-20,-15)#1\end}%
  }%
}
%    \end{macrocode}
% Note that a little code that reports errors if the
% command is used wrongly, is incorporated.
% \end{macro} 
%
% \begin{macro}{\@parseArg}
% \begin{macro}{\@getSymbol}
% \begin{macro}{\@doSymbolMacro}
% \begin{macro}{\@saveBeforeSymbolMacro}
%   These macros parse a single argument. As there is some testing of
%   the following token, it is splitted into four macros, the main one being
%   \cmd{\@parseArg}. It is given the offset to a possibly nested diagram and the
%   position of the symbol within the current diagram. All it does is
%   testing wether the argument is a command (\cmd{\@doSymbolMacro}) or some
%   text string ("@\getSymbol"), and then passing the parameters on to the
%   appropriate macro.
%    \begin{macrocode}
\def\@parseArg(#1)(#2){%
  \@ifNextMacro{\@doSymbolMacro(#1)(#2)}{\@getSymbol(#2)}}
%    \end{macrocode}
%   \cmd{\@getSymbol} is used when the argument is ``plain'' text. It simply
%   passes the parameters to \cmd{\@putSymbol}, which does the setting up.
%    \begin{macrocode}
\def\@getSymbol(#1)#2\end{\@putSymbol[#2]{#1}}
%    \end{macrocode}
%   \cmd{\@doSymbolMacro} is used when the argument has been identified as a
%   macro. It tests if there is an optional argument, which is then saved
%   in \cmd{\@@symbol} using \cmd{\@saveBeforeSymbolMacro} and \cmd{\@@tempSymbol}.
%   Then the macro is expanded.
%    \begin{macrocode}
\def\@doSymbolMacro(#1)(#2)#3{%
  \@ifnextchar[{\@saveBeforeSymbolMacro(#1)(#2)#3}%
               {\@symbolMacro(#1)(#2)#3}}
%    \end{macrocode}
%    \begin{macrocode}
\def\@saveBeforeSymbolMacro(#1)(#2)#3[#4]#5\end{%
  \@@tempSymbol={#4}%
  \@@Nestedtrue\put(#1){#3#5}%
  \@putSymbol[\the\@@tempSymbol]{#2}}
%    \end{macrocode}
%    \begin{macrocode}
\def\@symbolMacro(#1)(#2)#3\end{%
  \@@Nestedtrue\put(#1){#3}%
  \@putSymbol{#2}}
%    \end{macrocode}
% \end{macro}
% \end{macro}
% \end{macro}
% \end{macro}
%
% \begin{macro}{\@putSymbol}
%   This is an auxiliary macro that sets as default set the text of register
%   \cmd{\@@symbol} on the given position. If, however, a parameter is given,
%   \cmd{\@@symbol} is set to this parameter before \cmd{\@@symbol} is set. The
%   macro is used by all the diagrams to set the symbols when they have
%   been determined.
%    \begin{macrocode}
\newcommand{\@putSymbol}[2][\the\@@symbol]{%
  \global\@@symbol=\expandafter{#1}%
  \put(#2){\makebox(20,20){\texttt{\the\@@symbol}}}}
%</Tdiagram>
%    \end{macrocode}
% \end{macro}
%
% \MakeShortVerb{\|} ^^A Usefull as " is used by the grammar
% \subsection{Reserved words}
%
%    \begin{macrocode}
%<*reservedWords>
\TestForConflict{\reservestyle,\@reservestyle,\setreserved,\<}
\TestForConflict{\@parseDefineReserved,\@xparseDefineReserved}
\TestForConflict{\@defineReserved,\@xdefineReserved}
%    \end{macrocode}
%
% \begin{macro}{\reservestyle}
%   \changes{2.0$\alpha$}{1996/05/18}{Added commands for setting reserved
%     words: \cs{reservestyle} and \cs{<}}
%   \cmd{\reservestyle} defines the typesetting style for a class of reserved
%   words by defining a command for defining reserved words
%   from this class
%    \begin{macrocode}
\newcommand{\reservestyle}[3][]{
  \newcommand{#2}{\@parseDefineReserved{#1}{#3}}
%    \end{macrocode}
%   \cmd{\reservestyle} takes an optional command to control the spacing, \eg
%   \cmd{\mathinner}, a command \cs{\meta{name}} and a formatting
%   macro.  The commandname is defined to call an internal parsing function,
%   \cmd{\@parseDefineReserved} which will reserve the concrete words.
%    \begin{macrocode}
   \expandafter\expandafter\expandafter\def
     \expandafter\csname set\expandafter\@gobble\string#2\endcsname##1%
   {#1{#3{##1}}}}
%    \end{macrocode}
%  Defines the command \cs{set\meta{name}} as a shortcut to get the
%  specified style.  For an explanation of the expansion of
%  \cs{set\meta{name}}, see the definition of "@xdefineReserved" on
%     p.~\pageref{page:styleExpansion}. 
% \end{macro} ^^A \reservestyle
%
% \begin{macro}{\@parseDefineReserved}^^A 
% \begin{macro}{\@xparseDefineReserved}^^A
%   \cmd{\@parseDefineReserved} parses the parameters and set up the following
%   two internal registers, which are used when defining each word.
%    \begin{macrocode}
\newtoks\@@spacing
\newtoks\@@formating
\def\@parseDefineReserved#1#2{%
  \@ifnextchar[{\@xparseDefineReserved{#2}}%
     {\@xparseDefineReserved{#2}[#1]}}
%    \end{macrocode}
% If no spacing command is provided to the definition, the default ("#1")
% for the style is used. 
%    \begin{macrocode}
\def\@xparseDefineReserved#1[#2]#3{%
  \@@formating{#1}%
  \@@spacing{#2}%
  \expandafter\@defineReserved#3,\end
}
%    \end{macrocode}
%   The formatting and the spacing information is saved and then the
%   comma separated list of words to be reserved are processed.  The
%   sequence ",\end" gives and end marker.
% \end{macro} ^^A \@parseDefineReserved
% \end{macro} ^^A \@xparseDefineReserved
%
% \begin{macro}{\@defineReserved}^^A
% \begin{macro}{\@xdefineReserved}
%   The two commands define a reserved word: \cmd{\@defineReserved} testes if
%   it is the last argument and makes it possible for \cmd{\@xdefineReserved} to
%   test if an alternative text is provided. \cmd{\@xdefineReserved} also
%   defines the reserved word. 
%    \begin{macrocode}
\def\@defineReserved#1,{%
  \@ifnextchar\end
%    \end{macrocode}
%   Testes if this is the last word (\cmd{\end} is following the comma) to
%   decide if another iteration should be done after defining the word in
%   "#1".  
%    \begin{macrocode}
  {\@xdefineReserved #1[]\END\@gobble}%
%    \end{macrocode}
%   If is was the last then remove the endmarker \cmd{\end}.
%    \begin{macrocode}
  {\@xdefineReserved#1[]\END\@defineReserved}}
%    \end{macrocode}
%   "[]" is inserted to ensure \cmd{\@xdefineReserved} that all
%   definitions have a pair of and \cmd{\END} makes it possible to remove an
%   extra set of brackets, if there was already a pair of brackets in "#1".
%    \begin{macrocode}
\def\@xdefineReserved#1[#2]#3\END{%
  \def\reserved@a{#2}%
  \ifx \reserved@a\empty \toks0{#1}\else \toks0{#2} \fi
%    \end{macrocode}
%   If the optional text is empty the word is used as text (saved in token
%   register 0).
%    \begin{macrocode}
    \expandafter\edef\csname\expandafter<#1>\endcsname
    {\the\@@formating{\the\@@spacing{\the\toks0}}}}
%    \end{macrocode}
%   \label{page:styleExpansion}
%   This defines the reserved word given in "#1" to the text given in
%   "#2". Saving "#2" in token register 0 is done to avoid having \cmd{\edef}
%   expanding any commands in the text (\see \cite[p.~216]{texbook}).
%
%   The reserved words are saved as macros with the names enclosed in angle
%   brackets. They can thus only be expanded using
%   \cmd{\csname}\lttdots\cmd{\endcsname}.  The typesetting ("{#1{#3}}") is done 
%   inside a group so it is possible to use style changing commands like
%   \cmd{\scriptstyle} (though it would admittedly be strange).  By enclosing 
%   the text "#2" in brackets one argument commands like \cmd{\textbf} are also
%    possible.   
% 
%   Be aware that the use of \cmd{\def} to
%   define the command, allows redefinition of a already reserved words an
%   even other macros.
% \end{macro} ^^A \@xdefineReserved
% \end{macro} ^^A \@DefineReserved
%
% \begin{macro}{\setreserved}
% \begin{macro}{\<}
%   \cmd{\setreserved} is a command for internal use (however provided for the
%   user if necessary to avoid conflict on "\<") to typeset a reserved word.
%   \cmd{\setreserved} is used by "\<",
%   the command to typeset reserved words, and the argument is thus
%   delimited by a ">" (the use being \cs{<\meta{name}>}).
%    \begin{macrocode}
\def\setreserved#1>{%
  \expandafter\let\expandafter\reserved@a\csname<#1>\endcsname
  \@ifundefined{reserved@a}{\PackageError{Semantic}
      {``#1'' is not defined as a reserved word}%
      {Before referring to a name as a reserved word, it % 
      should be defined\MessageBreak using an appropriate style 
      definer.  A style definer is defined \MessageBreak 
      using \protect\reservestyle.\MessageBreak%
      Type <return> to proceed --- nothing will be set.}}%
  {\reserved@a}}
\let\<=\setreserved
%</reservedWords>
%    \end{macrocode}
%   Typesetting of the reserved word is done by expanding the macro defined
%   for the name.  The macro name is first build in the internal \LaTeX\
%   register \cmd{\reserved@a} so it can be tested if the name is defined. 
% \end{macro}
% \end{macro}
%
% \subsection{The Short Hands Part}
% \changes{2.0}{1998/05/24}{Made the short hand options part}
% At last  come all the commands for symbols facilitating the notation of
% semantics. They are all fairly simple, taking some arguments and setting
% them in an  pproriate font intermixed with some filling symbols.
%
% \subsubsection{The Symbols \@bblb and \@bbrb}
% \begin{macro}{\@bblb}
% \begin{macro}{\@bbrb}
% \begin{macro}{\@mbblb}
% \begin{macro}{\@mbbrb}
% \changes{1.0}{1995/10/20}{I have defined ``fake''-black\-board\-bold for
% the benefit of  people who do not have \package{bbold}}
% \changes{1.2$\alpha$}{1996/01/31}{Changed the names}
% \changes{1.2$\alpha$}{1996/01/31}{Added permanent use of document main font}
% \makeatletter\changes{2.0}{1998/05/24}{Moved to the new "shorthand" options part and made ligatures for $\@bblb$ and $\@bbrb$.}\makeatother
% \changes{2.0}{1998/05/24}{Introduced the math mode commands \cs{@mbblb} and \cs{@mbbrb}.}
% \makeatletter
% If \package{bbold}, is installed it is used to make \@bblb\ og \@bbrb.
% Otherwise two brackets are drawn together. To make this transparent to the
% rest of the package, two commands \cmd{\@bblb} (\textbf{b}lackboard
% \textbf{b}old \textbf{l}eft \textbf{b}racket) and \cmd{\bbrb}
% (\textbf{b}lackboard \textbf{b}old \textbf{r}ight \textbf{b}racket) are
% defined , which in both cases gives \@bblb\ or \@bbrb, respectively.
%    \begin{macrocode}
%<*shorthand>
\IfFileExists{DONOTUSEmathbbol.sty}{%
  \RequirePackage{mathbbol} 
  \newcommand{\@bblb}{\textbb{[}}
  \newcommand{\@bbrb}{\textbb{]}}
  \newcommand{\@mbblb}{\mathopen{\mbox{\textbb{[}}}}
  \newcommand{\@mbbrb}{\mathclose{\mbox{\textbb{]}}}}
} 
{ \newcommand{\@bblb}{\textnormal{[\kern-.15em[}}
  \newcommand{\@bbrb}{\textnormal{]\kern-.15em]}}
  \newcommand{\@mbblb}{\mathopen{[\mkern-2.67mu[}}
  \newcommand{\@mbbrb}{\mathclose{]\mkern-2.67mu]}}
}
%    \end{macrocode}
% \makeatother
% \end{macro}
% \end{macro}
% \end{macro}
% \end{macro}
%
% \subsubsection{Short Hands for the Often Needed Symbols}
%
% This defines the often needed symbols.  Note that by specifying the option
%  "shorthand" math ligatures are automatically loaded.
%    \begin{macrocode}
\mathlig{|-}{\vdash}
\mathlig{|=}{\models}
\mathlig{->}{\rightarrow}
\mathlig{->*}{\mathrel{\rightarrow^*}}
\mathlig{->+}{\mathrel{\rightarrow^+}}
\mathlig{-->}{\longrightarrow}
\mathlig{-->*}{\mathrel{\longrightarrow^*}}
\mathlig{-->+}{\mathrel{\longrightarrow^+}}
\mathlig{=>}{\Rightarrow}
\mathlig{=>*}{\mathrel{\Rightarrow^*}}
\mathlig{=>+}{\mathrel{\Rightarrow^+}}
\mathlig{==>}{\Longrightarrow}
\mathlig{==>*}{\mathrel{\Longrightarrow^*}}
\mathlig{==>+}{\mathrel{\Longrightarrow^+}}
\mathlig{<-}{\leftarrow}
\mathlig{*<-}{\mathrel{{}^*\mkern-1mu\mathord\leftarrow}}
\mathlig{+<-}{\mathrel{{}^+\mkern-1mu\mathord\leftarrow}}
\mathlig{<--}{\longleftarrow}
\mathlig{*<--}{\mathrel{{}^*\mkern-1mu\mathord{\longleftarrow}}}
\mathlig{+<--}{\mathrel{{}^+\mkern-1mu\mathord{\longleftarrow}}}
\mathlig{<=}{\Leftarrow}
\mathlig{*<=}{\mathrel{{}^*\mkern-1mu\mathord\Leftarrow}}
\mathlig{+<=}{\mathrel{{}^+\mkern-1mu\mathord\Leftarrow}}
\mathlig{<==}{\Longleftarrow}
\mathlig{*<==}{\mathrel{{}^*\mkern-1mu\mathord{\Longleftarrow}}}
\mathlig{+<==}{\mathrel{{}^+\mkern-1mu\mathord{\Longleftarrow}}}
\mathlig{<->}{\longleftrightarrow}
\mathlig{<=>}{\Longleftrightarrow}
\mathlig{|[}{\@mbblb}
\mathlig{|]}{\@mbbrb}
%    \end{macrocode}
% 
% \subsubsection{Denotational Semantics}
% I have given a lot of thoughts to the problem of choosing a good syntax.
% The most essential requirement was that syntax should be consistent and
% simple/intuitive, close to that used in \emph{Introduction to the Semantics
%   of Programming Languages}. To a semantics person, the most natural way to get
%   \eval{\lttdots}{x} would probably be  "\eval["\lttdots"]x"
% and indeed "\eval**["\lttdots"]x" rather than "\eval[**]{"\lttdots"}{x}".
% This is however a departure from the standard syntax of \LaTeX. And even
% more decisively, one cannot make an analogoues syntax for
% \cmd{\evalsymbol} since it is undecidable whether it is followed by a
% symbol: Does \emph{eg} "\evalsymbol test" mean ``\evalsymbol[t]est'' or
% ``\evalsymbol test''? This makes it necessary to use brackets in connection
% with \cmd{\evalsymbol} and in order to have a consistent syntax,  I have made
% the same decission for \cmd{\eval}.
%\begin{macro}{\evalsymbol}
%\begin{macro}{\compsymbol}\mbox{}
% \changes{1.0}{1995/10/18}{Settled on a syntax and described my considerations} 
% \changes{1.0}{1995/10/18}{Made som ``cleanup'' based on the decided syntax}
%    \begin{macrocode}
\newcommand{\evalsymbol}[1][]{\ensuremath{\mathcal{E}^{#1}}}
\newcommand{\compsymbol}[1][]{\ensuremath{\mathcal{C}^{#1}}}
%    \end{macrocode}
%   These lines define commands that take  an optional argument. If this
%   argument is \emph{not} present, the default value given in the second
%   pair of  brackets is used ie.\ nothing.
% \end{macro}
% \end{macro}
%
%\begin{macro}{\eval}
%\begin{macro}{\comp}\mbox{}
% \changes{1.0}{1995/10/18}{Erased several previous commands as they were
% just  special cases of the other commands (with the decided
% syntax). Furthermore the names were  translated from danish into english}
% \changes{1.2$\alpha$}{1996/01/30}{Made a brand new definition to avoid an
% error when using \cs{comp} and \cs{eval} with displaymath}
%    \begin{macrocode} 
\newcommand{\eval}[3][]%
  {\mbox{$\mathcal{E}^{#1}$\@bblb \texttt{#2}\@bbrb}%
   \ensuremath{\mathtt{#3}}}
\newcommand{\comp}[3][]%
  {\mbox{$\mathcal{C}^{#1}$\@bblb \texttt{#2}\@bbrb}%
   \ensuremath{\mathtt{#3}}}
%    \end{macrocode}
%  This definition should allow a linebreak after the last bracket
% \end{macro}
% \end{macro}
%
% \begin{macro}{\exe} \mbox{}
% \changes{1.0}{1995/10/18}{Translated the name to english}
%    \begin{macrocode}
\newcommand{\@exe}[3]{}
\newcommand{\exe}[1]{\@ifnextchar[{\@exe{#1}}{\@exe{#1}[]}}
\def\@exe#1[#2]#3{%
  \mbox{\@bblb\texttt{#1}\@bbrb$^\mathtt{#2}\mathtt{(#3)}$}}
%</shorthand>
%    \end{macrocode}
%   The command \cmd{\exe} is a stub that checks if the second argument begins 
%   with an optional sharp by looking at the token following the first
%   argument. If  a bracket  is not provided, an empty second argument is
%   added before the control is given to \cmd{\@exe}, which does the setting.
%   There is no place to do an expedient linebreak, so everything is
%   encapsulated in a \cmd{\mbox}.
% \end{macro}
%
% \subsection{End of All Options Files}
%  
% All the options files are ended with the following code to match the test
% whether the file is loaded from the semantics package
% (\emph{see}~\pageref{page:testForSemanticsLoader}):
%    \begin{macrocode}
%<*allOptions>
\fi
%</allOptions>
%    \end{macrocode}
%
% \subsection{Preamble of Users Guide and Documentation}
% \changes{1.0}{1995/10/16}{Made "semantic.sty" into a ".dtx"-file with a stub for generating the users guide and documentation}
% \changes{1.0}{1995/10/16}{Added control that the requested files is in fact  installed}
% \changes{1.2$\alpha$}{1996/01/28}{Put the document header at the bottom, and introduced a hack making \LaTeX\ think it is loading \texttt{semantic.sty} when processing \texttt{semantic.dtx}}
%
% The document preamble and the code to generate code is placed at the end,
% so that the documentation may  be printed before \semantic\ is installed. 
% For the use of \package{docstrip}, the code is marked as conditional
% code, so that it is not included in "semantic.sty" when installing the
% package.
%    \begin{macrocode}
%<*documentation>
\documentclass{ltxdoc} 
\usepackage[latin1]{inputenc}
%    \end{macrocode}
% We test whether multiple columns are supported (the package is
% loaded by \package{ltxdoc}):
%    \begin{macrocode}
\newif\ifmulticols 
\IfFileExists{multicol.sty}{\multicolstrue}{}
%    \end{macrocode}
% We make a command \cmd{\command} for the dangerous bend sign (used in the
% \TeX-book).  If the font "manfnt.tfm" is not installed on your
% system, you should turn the second line, \cmd{\dangertrue} into a
% comment:
%    \begin{macrocode}
\newif\ifdanger 
\dangertrue
\DeclareFontFamily{U}{manual}{} 
\DeclareFontShape{U}{manual}{m}{n}{<->  manfnt }{} 
\newcommand{\danger}
  {{\fontencoding{U}\fontfamily{manual}\selectfont\symbol{127}}}
%    \end{macrocode}
% We define some abbreviations used in the text,
%    \begin{macrocode}
\usepackage{xspace}
\newcommand{\ie}{\emph{ie}\xspace}
\newcommand{\eg}{\emph{eg}\xspace}
\newcommand{\see}{\emph{see}\xspace}
\newcommand{\semantic}{\texttt{semantic}\xspace}
\newcommand{\lttdots}{\ensuremath{\mathtt{\ldots}}}
\newcommand{\ExplicitSpace}{\texttt{\char'040}}
%    \end{macrocode}
% a command for typesetting the names of other packages.
%    \begin{macrocode}
\newcommand{\package}[1]{\textsf{#1}}
%    \end{macrocode}
% and a command for printing CVS tags. 
%    \begin{macrocode}
\def\RCS$#1: #2 ${\@namedef{RCS#1}{#2}}
%    \end{macrocode}
% \changes{2.0(delta)}{2002/06/19}{Included the RCS revision in the file information}
%
% We make a command \cmd{\labelnextline} for labelling the following line
%    \begin{macrocode}
\newcommand{\labelnextline}[1]{{%
  \count8\inputlineno \advance\count8\@ne
  \@bsphack
  \protected@write\@auxout{}%
    {\string\newlabel{#1}{{\the\count8}{\thepage}}}%
  \@esphack}}
%    \end{macrocode}
% We then define that the default is to typeset only the manual so we
% can live without cross references.
%    \begin{macrocode}
\OnlyDescription
\DisableCrossrefs
%    \end{macrocode}
% You can change this behaviour by uncommenting line two to five
% below.  That will include the implementation and also add
% crossreferences, an index of the command usage and definitions, and
% the change history.
%    \begin{macrocode}
\labelnextline{lin:AlsoImplementation}
 % \AlsoImplementation
 % \EnableCrossrefs
 % \CodelineIndex
 % \RecordChanges
%    \end{macrocode}
% We define the command \cmd{\semanticVersionPrint} containing the commands to 
% to typeset the version number with neatly formatting of the Greek letter.
%    \begin{macrocode}
\makeatletter
{\def\ver#1(#2)#3\relax{%
   \def\tc{#1}% 
   \def\td{#2}%
   \ifx\td\empty 
   \else \edef\td{$\csname #2\endcsname$}\fi}%
 \expandafter\ver\semanticVersion()\relax
 \xdef\semanticVersionPrint{\tc\td}}
%    \end{macrocode}
% (\cmd{\tc} and \cmd{\td} are use similarly in \LaTeX's \cmd{\GetInfo}.)
% \changes{2.0\delta}{2002/07/12}{Deleted \cs{GetInfo}.}
% \changes{2.0\delta}{2002/07/12}{Introduced \cs{semanticVersionPrint} to give a formatted version number.}
% We define a command \cmd{\parmark}\oarg{mark} which starts a
% paragraph with \meta{mark} to the left of the paragraph.  This is to
% put dangerous bends around certain paragraphs.  If \meta{mark} is
% not given, the default set with \cmd{\setparagraphmark} is used.
%    \begin{macrocode}
\newtoks\p@rm@rk 
\newcommand{\setparagraphmark}[1]{\p@rm@rk={#1}}
\newcommand{\parmark}[1][\the\p@rm@rk]{%
  \setbox0=\hbox{\huge #1}%
  \clubpenalty=10000%
  \noindent\hangindent=\wd0 \hangafter=-2%
  \llap{\raise.35em\hbox{\vbox to\z@{\box0 \vss}\hfill}}}
%    \end{macrocode}
%  We make an environment for typesetting small pieces of code
%    \begin{macrocode}
\newenvironment{code}
  {\begin{verse}\small}
  {\end{verse}}
%    \end{macrocode}
%  and a variant of the "itemize" environment to be used inside
%  columns (we choose smaller values of the indentation).
%    \begin{macrocode}
\newenvironment{columnItemize}%
  {\begin{list}%
    {$\bullet$}%
    {\settowidth{\labelwidth}{$\bullet$}%
     \setlength{\leftmargin}{5mm}%
     \setlength{\labelsep}{\leftmargin}%
     \addtolength{\labelsep}{-\labelwidth}}}%
  {\end{list}}
%    \end{macrocode}
%  Finally, we print a (hopefully) comforting message to the user
%    \begin{macrocode}
\typeout{}
\typeout{NOTE: If LaTeX complains}
\typeout{\@spaces\@spaces Font U/manual/m/n/9 manfnt at %
  9.0 not loadable: ...}
\typeout{\@spaces\space\space then comment out the line (around 2725)}
\typeout{\@spaces\@spaces \protect\dangertrue}
\typeout{}
\typeout{There will be some overfull and underfull boxes, %
           and some moved marginpars.}
\typeout{Do not bother!!!}
\typeout{}
\makeatother
%    \end{macrocode}
%  before we finally starts typesetting the manual.
%    \begin{macrocode}
\begin{document}
  \DocInput{semantic.dtx}
\end{document}
%</documentation>
%    \end{macrocode}
% 
% \begin{thebibliography}{1}
%   \bibitem{texbook}    
%     \textsc{D.E.~Knuth} \emph{The \TeX-book}, 1994, Addison-Wesley
%^^A   \bibitem{companinon} 
%^^A     \textsc{M.~Goosens, F.~Mittelbach, and A.~Samarin} \emph{The \LaTeX{} Companion}, 1994, Addison-Wesley
%   \bibitem{packagesguide}
%     \textsc{The \LaTeX3 Project} \emph{\LaTeXe\ for class and packages writers}, 10 June 1995
%   \bibitem{LaTeXbook}
%     \textsc{L. Lamport} \emph{\LaTeX\ : a Document preparation system}, 1994, Addison-Wesley
% \end{thebibliography}
%
% \Finale\PrintIndex \sloppy \PrintChanges
\endinput