% \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\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