hetcasl.sty revision 3f5ce32a7360129566b1f79719c3ac64d46046a9
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang\ProvidesPackage{hetcasl}[2002/10/04 v0.1 LaTeX Package for CASL v1.0.1]
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang\NeedsTeXFormat{LaTeX2e}
79a7f2de0a7e933d26b64d35b2801618ff015954Klaus Luettich% Required packages
79a7f2de0a7e933d26b64d35b2801618ff015954Klaus Luettich\RequirePackage{ifthen}
79a7f2de0a7e933d26b64d35b2801618ff015954Klaus Luettich\RequirePackage{tabularx}
79a7f2de0a7e933d26b64d35b2801618ff015954Klaus Luettich\RequirePackage{calc}
79a7f2de0a7e933d26b64d35b2801618ff015954Klaus Luettich\RequirePackage[latin1]{inputenc}
79a7f2de0a7e933d26b64d35b2801618ff015954Klaus Luettich\RequirePackage{xspace}
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang\newcounter{@opentabulars}
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang\setcounter{@opentabulars}{0}
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang\newlength{\@oldparindent}
79a7f2de0a7e933d26b64d35b2801618ff015954Klaus Luettich\newlength{\@hetcaslmaxwidth}
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang\newlength{\@remhetcaslwidth}
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang\newlength{\@KWwidth}%
b569e96f02dea40cb81899293c7d99e1d750b3c0Till Mossakowski% The next two length variables will be used in \KW
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang\newlength{\@realWidth}\newlength{\@neededWidth}
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang\newif\ifhetcasl \hetcaslfalse
1a5239c089cfe6c684855256c02496e6a7a4d281Heng Jiang\newenvironment{hetcasl}[1][\textwidth]%
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder\PackageError{hetcasl evironments cannot nested}%
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang\else\hetcasltrue\fi%
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang\setlength{\@oldparindent}{\the\parindent}%
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang\setlength{\parindent}{0cm}%
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang\setlength{\@hetcaslmaxwidth}{#1}%
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang\setlength{\@remhetcaslwidth}{\the\@hetcaslmaxwidth}%
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang%\begin{alltt}\begingroup\rmfamily
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang\begin{tabbing}%
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang% a little line to set up three useful tabstops for rendering parts
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang% of a library and or specification
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang\KW{view} \=\KW{preds} \=~~~~~~~\=\kill
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang\end{tabbing}%
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang%\endgroup\end{alltt}
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang%\@CloseAllTabulars%
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang\setlength{\parindent}{\the\@oldparindent}%
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang\hetcaslfalse%
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang\newcommand{\@HetCASLPrelude}{% HetCASL-Prelude
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang\settowidth{\@KWwidth}{\textbf{view}}
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang%%%% define all the makros needed for typesetting hetCASL
9312e4bac069d53091c92e20b03dcb4e07f40f9fHeng Jiang% \KW prints a KeyWord within a box that is at least \@KWwidth wide.
9312e4bac069d53091c92e20b03dcb4e07f40f9fHeng Jiang% If the keyword needs more space the box is as wide as the kyeword
9312e4bac069d53091c92e20b03dcb4e07f40f9fHeng Jiang% is. The optional argument overrides \@KWwidth with the width of the
9312e4bac069d53091c92e20b03dcb4e07f40f9fHeng Jiang% mandatory argument in bold face. The mandatory argument is always
9312e4bac069d53091c92e20b03dcb4e07f40f9fHeng Jiang% printed in bold face.
9312e4bac069d53091c92e20b03dcb4e07f40f9fHeng Jiang\newcommand{\KW}[2][no--format--keyword]%
9312e4bac069d53091c92e20b03dcb4e07f40f9fHeng Jiang{\ifthenelse{\equal{##1}{no--format--keyword}}%
9312e4bac069d53091c92e20b03dcb4e07f40f9fHeng Jiang{% no optional argument
9312e4bac069d53091c92e20b03dcb4e07f40f9fHeng Jiang\settowidth{\@neededWidth}{\textbf{##2}}}%
9312e4bac069d53091c92e20b03dcb4e07f40f9fHeng Jiang{% optional argument given
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder\settowidth{\@realWidth}{\textbf{##2}}%
9312e4bac069d53091c92e20b03dcb4e07f40f9fHeng Jiang\settowidth{\@KWwidth}{\textbf{##1}}%
9312e4bac069d53091c92e20b03dcb4e07f40f9fHeng Jiang\ifthenelse{\@KWwidth > \@realWidth}%
9312e4bac069d53091c92e20b03dcb4e07f40f9fHeng Jiang{\setlength{\@neededWidth}{\@KWwidth}}%
9312e4bac069d53091c92e20b03dcb4e07f40f9fHeng Jiang{\setlength{\@neededWidth}{\@realWidth}}}%
9312e4bac069d53091c92e20b03dcb4e07f40f9fHeng Jiang\makebox[% set the width of the box not smaller
9312e4bac069d53091c92e20b03dcb4e07f40f9fHeng Jiang% than the width of the KeyWord
9312e4bac069d53091c92e20b03dcb4e07f40f9fHeng Jiang\@neededWidth]%
9312e4bac069d53091c92e20b03dcb4e07f40f9fHeng Jiang[l]{\textbf{##2}}%
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang% \SId prints its argument in small caps as a Structured Id for names
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang% of specifications, views and libraries
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang\newcommand{\SId}[1]{\textsc{##1}}%
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang% \SIdIndex prints its argument like \SId but sets an Index Entry if
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang\newcommand{\SIdIndex}[1]{\SId{##1}}%
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang% \Id prints its argument in italic face as one word, for all other
20bcb42e212faef728ac606e69dc1f9de55a9988Heng Jiang% identifiers not covered by \SId and only containing letters, numbers
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang\newcommand{\Id}[1]{\textit{##1}}%
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang% \AX prints its argument in math modus
79a7f2de0a7e933d26b64d35b2801618ff015954Klaus Luettich\newcommand{\Ax}[1]{\ensuremath{##1}}%
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang\newcommand{\ANNOTEWORD}[1]{{\small{}\KW{\%##1}}}
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang%%%%% Heng todo:
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang%% Makros aus casl.sty definieren
20bcb42e212faef728ac606e69dc1f9de55a9988Heng Jiang\newcommand{\LBRACE} {\{}
79a7f2de0a7e933d26b64d35b2801618ff015954Klaus Luettich\newcommand{\RBRACE} {\}}
20bcb42e212faef728ac606e69dc1f9de55a9988Heng Jiang\newcommand{\FREE} {\KW{free}\xspace} %plain_keyword
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang\newcommand{\FREELBRACE} {\FREE~\LBRACE}
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang\newcommand{\GENERATED} {\KW{generated}\xspace}
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang% \newcommand{\TYPE} {\KW{type}}
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang% \newcommand{\TYPES} {\KW{types}}
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang\newcommand{\FREETYPE} {\FREE~\TYPE\xspace}
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang\newcommand{\FREETYPES} {\FREE~\TYPES\xspace}
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang\newcommand{\GENERATEDTYPE} {\GENERATED~\TYPE\xspace} %{\KW{generated~type}}
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang\newcommand{\GENERATEDTYPES} {\GENERATED~\TYPES\xspace}
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiang\newcommand{\VARS} {\KW{vars}\xspace}
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiang\newcommand{\AXIOM} {\KW{axiom}\xspace}
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiang\newcommand{\AXIOMS} {\KW{axioms}\xspace}
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang\newcommand{\HIDE} {\KW{hide}\xspace}
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang\newcommand{\REVEAL} {\KW{reveal}\xspace}
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang\newcommand{\WITH} {\KW{with}\xspace}
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang\newcommand{\THEN} {\KW[view]{then}\xspace} % hetcasl_keyword
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang\newcommand{\THENCONS} {\THEN~\ANNOTEWORD{cons}\xspace}
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang\newcommand{\THENDEF} {\THEN~\ANNOTEWORD{def}\xspace}
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiang\newcommand{\THENIMPLIES} {\THEN~\ANNOTEWORD{implies}\xspace}
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiang\newcommand{\THENMONO} {\THEN~\ANNOTEWORD{mono}\xspace}
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiang\newcommand{\AND} {\KW{and}\xspace}
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang\newcommand{\LOCAL} {\KW{local}\xspace}
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang\newcommand{\THENLOCAL} {\THEN~\LOCAL}
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang\newcommand{\WITHIN} {\KW{within}\xspace}
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang\newcommand{\CLOSED} {\KW{closed}\xspace}
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang\newcommand{\FIT} {\KW{fit}\xspace}
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang\newcommand{\TO} {\KW{to}\xspace}
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang\newcommand{\LOGIC} {\KW{logic}\xspace}
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang\newcommand{\SPEC} {\KW[view]{spec}\xspace}
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang\newcommand{\VIEW} {\KW[view]{view}\xspace}
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang\newcommand{\END} {\KW{end}\xspace}
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang\newcommand{\ARCH} {\KW{arch}\xspace}
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang\newcommand{\ARCHSPEC} {\ARCH~\KW{spec}\xspace}
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang\newcommand{\UNITSPEC} {\KW{unit}~\KW{spec}\xspace}
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang\newcommand{\UNITS} {\KW{units}\xspace}
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang\newcommand{\GIVEN} {\KW{given}\xspace}
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang\newcommand{\RESULT} {\KW{result}\xspace}
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang\newcommand{\LIBRARY} {\KW{library}\xspace}
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang\newcommand{\FROM} {\KW[view]{from}\xspace}
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang\newcommand{\GET} {\KW{get}\xspace}
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang\newcommand{\VERSION} {\KW{version}\xspace}
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang\newcommand{\PROD} {\Ax{\times}}
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiang\newcommand{\TOTAL} {\Ax{\rightarrow}}
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiang\newcommand{\PARTIAL} {\Ax{\rightarrow}}
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiang\newcommand{\MAPSTO} {\Ax{\mapsto}}
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder\newcommand{\ASSOC} {\Id{assoc}}
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder\newcommand{\COMM} {\Id{comm}}
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder\newcommand{\IDEM} {\Id{idem}}
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder\newcommand{\UNIT} {\Id{unit}\xspace}
79a7f2de0a7e933d26b64d35b2801618ff015954Klaus Luettich\newcommand{\EXISTS} {\Ax{\exists}}
79a7f2de0a7e933d26b64d35b2801618ff015954Klaus Luettich\newcommand{\EXISTSUNIQUE} {\AX{\exists!}}
79a7f2de0a7e933d26b64d35b2801618ff015954Klaus Luettich\newcommand{\IMPLIES} {\Ax{\Rightarrow}}
79a7f2de0a7e933d26b64d35b2801618ff015954Klaus Luettich\newcommand{\IFF} {\Ax{\Leftrightarrow}}
79a7f2de0a7e933d26b64d35b2801618ff015954Klaus Luettich\newcommand{\EEQ} {\Ax{\stackrel{e}{=}}}
79a7f2de0a7e933d26b64d35b2801618ff015954Klaus Luettich\newcommand{\A} {\Ax{\wedge}}
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder\newcommand{\V} {\Ax{\vee}}
9312e4bac069d53091c92e20b03dcb4e07f40f9fHeng Jiang\newcommand{\IN} {\Ax{\in}}
79a7f2de0a7e933d26b64d35b2801618ff015954Klaus Luettich\newcommand{\NOT} {\Ax{\neg}}
79a7f2de0a7e933d26b64d35b2801618ff015954Klaus Luettich\newcommand{\FORALL} {\Ax{\forall}}
79a7f2de0a7e933d26b64d35b2801618ff015954Klaus Luettich\newcommand{\BULLET} {\Ax{\;\bullet\;}}
79a7f2de0a7e933d26b64d35b2801618ff015954Klaus Luettich\newcommand{\IF} {\Id{if}\xspace}
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder\newcommand{\WHEN} {\Id{when}\xspace}
79a7f2de0a7e933d26b64d35b2801618ff015954Klaus Luettich\newcommand{\ELSE} {\Id{else}\xspace}
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder\newcommand{\DEF} {\Id{def}\xspace}
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang\newcommand{\VAR} {\Id{var}\xspace}
79a7f2de0a7e933d26b64d35b2801618ff015954Klaus Luettich\newcommand{\AS} {\Id{as}\xspace}
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder\newcommand{\TRUE} {\Id{true}\xspace}
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang\newcommand{\FALSE} {\Id{false}\xspace}
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder%%%% SORT, OP, PRED : drei Varianten %% Type auch
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder\newcommand{\KWC}[2][preds]{%
79a7f2de0a7e933d26b64d35b2801618ff015954Klaus Luettich\ifthenelse{\equal{##1}{KW}}%
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder{%KW as parameter
79a7f2de0a7e933d26b64d35b2801618ff015954Klaus Luettich{% else to KW as parameter
79a7f2de0a7e933d26b64d35b2801618ff015954Klaus Luettich\ifthenelse{\equal{##1}{ID}}%
79a7f2de0a7e933d26b64d35b2801618ff015954Klaus Luettich{%ID as parameter
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang{% else to ID as parameter
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang\KW[preds]{##2}}}%
20bcb42e212faef728ac606e69dc1f9de55a9988Heng Jiang}%% end of KWC definition
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder\newcommand{\SORT}[1][preds]{\KWC[##1]{sort}\xspace}
9312e4bac069d53091c92e20b03dcb4e07f40f9fHeng Jiang\newcommand{\SORTS}[1][preds]{\KWC[##1]{sorts}\xspace}
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang\newcommand{\OP}[1][preds]{\KWC[##1]{op}\xspace}
20bcb42e212faef728ac606e69dc1f9de55a9988Heng Jiang\newcommand{\OPS}[1][preds]{\KWC[##1]{ops}\xspace}
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang\newcommand{\PRED}[1][preds]{\KWC[##1]{pred}\xspace}
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang\newcommand{\PREDS}[1][preds]{\KWC[##1]{preds}\xspace}
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder\newcommand{\TYPE}[1][preds]{\KWC[##1]{type}\xspace}
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder\newcommand{\TYPES}[1][preds]{\KWC[##1]{type}\xspace}
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang%% 1. mit \KWC[preds]{} default
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder%% 2. mit \KWC[KW]{}
f5c7d6d3f873962ccbe63276243e88030ce8801dHeng Jiang%% 3. mit \KWC[ID]{}
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder% starting a library
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang\newcommand{\library}[1]{\KW{library}\ \SId{##1}\ }
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder% printing a version number
9312e4bac069d53091c92e20b03dcb4e07f40f9fHeng Jiang%\newcommand{\version}[1]{\KW{version}\ ##1}
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder% comments, annotations and labels
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang\newcommand{\commentline}[1]{\textbf{\%\%}{\small##1}}
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder\newenvironment{commentgroup}%
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder{\textbf{\%\{}\begingroup\small}%
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang{\endgroup\textbf{\}\%}}%
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder\newcommand{\annoteline}[2]{\textbf{\%##1}\ {\small \(##2\)}}%
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang\newenvironment{annotegroup}[1]%
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang{\textbf{\%##1(}\begingroup\small}%
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder{\endgroup\textbf{)\%}}%
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder\newcommand{\casllabel}[1]{\textbf{\%(}{\small##1}\textbf{)\%}}%
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder\newenvironment{mlabel}%
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder{\textbf{\%(}\begingroup\small}%
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang{\endgroup\textbf{)\%}}%
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder\newcommand{\place}{\_\_}%
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang%% download items (from, get are automatically printed)
20bcb42e212faef728ac606e69dc1f9de55a9988Heng Jiang\newenvironment{downloaditem}[1]%
9312e4bac069d53091c92e20b03dcb4e07f40f9fHeng Jiang{\begingroup\sc
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang\textnormal{\textbf{from}}\ ##1\ %
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder%\textnormal{\ifthenelse{\equal{##1}{no-version}}{}{\version{##1}\ }}%
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder\textnormal{\textbf{get}}}%
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder%% specifications
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang% specdefn starts a new spec defn
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang% arguments: ##1 ::= opt. semantic-anno
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder% ##2 ::= spec name
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang% ##3 ::= parameters (see parameterspecs-env)
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang% ##4 ::= imports (see importspecs-env)
0b31ea5ec0e20f17d55845a5d803c48466e01ca3Heng Jiang\newenvironment{specdefn}[4][no-semantic-anno]%
262ff0b92f2ba957c821ce8d9b4ee2f554cdf701Heng Jiang{\textbf{spec}\ \textsc{##2}%
9312e4bac069d53091c92e20b03dcb4e07f40f9fHeng Jiang\ifthenelse{\equal{##3}{}}{}{##3}%
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang% end of \@HetCASLPrelude
9312e4bac069d53091c92e20b03dcb4e07f40f9fHeng Jiang\@HetCASLPrelude%
1c7aefd3163ebc1cd1f56ed93f39a7d688b97fedHeng Jiang% calculate a new width based on \@remhetcaslwidth and the fixed width
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang% given as argument.
0b31ea5ec0e20f17d55845a5d803c48466e01ca3Heng Jiang\newcommand{\@calc@width}[1]{}
0b31ea5ec0e20f17d55845a5d803c48466e01ca3Heng Jiang%\newcommand{\@tabnewline}{\\&}
876096baba5bb126049ecde28ff6644fae78d7a3Christian Maeder\newcommand{\@condEOL}{\ifthenelse{\the@opentabulars=0}{\\}{\@tabnewline}}
0b31ea5ec0e20f17d55845a5d803c48466e01ca3Heng Jiang\newcommand{\@CloseAllTabulars}{}