%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% A LaTeX2e style for TeXing programs
%
% by P. Pepper  opal2x.sty 1996/03/19 TU Berlin program package (v 0.1)
% (adapted for CASL by C. Maeder 2002/08/12)
%
% (Note: This package is almost completely written in TeX!)
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{caslx}[2002/08/12 Uni Bremen program package (v 0.1)]
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                  %
% Options
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
\newif\if@AmsWanted
\newif\if@SuppressSymbols
%
\DeclareOption{ams}{\PassOptionsToPackage{ams}{symbols}}
\DeclareOption{suppress}{\PassOptionsToPackage{suppress}{symbols}}
\ProcessOptions
\relax
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Load other packages
%
\RequirePackage{basicprg}
\RequirePackage{symbols}
\RequirePackage{scanner}
%
%     +-------------------------------------------------------+
%     | Used variables from "basicprg.sty":                  |
%     |     \@TeXCmnt                                         |
%     |     \@CmntSymb                                        |
%     |                                                       |
%     | Redefined variables from "basicprg.sty":             |
%     |     \@Cmnt                                            |
%     |                                                       |
%     +-------------------------------------------------------+
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                  %
% Options (none available)
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                             %
%     +-------------------------------------------------------+
%     | Interface: The following macros from "basicprg.sty"   |
%     |            are redefined                              |
%     |                                                       |
%     |            \KeyWord                                   |
%     |            \@CommentSymb                              |
%     |            \@Comment                                  |
%     |                                                       |
%     +-------------------------------------------------------+
%                                                             %
\def\KeyWord#1{\textbf{\lowercase{#1}}}%    % default         %
\def\@CommentSymb{{}}%                                        %
\def\@Comment#1{\textit{#1}}%                                 %
%                                                             %
%     +-------------------------------------------------------+
%     | Interface: The following macros from "scanner.sty"    |
%     |            are redefined                              |
%     |                                                       |
%     |            \DigitFont                                 |
%     |            \IdentifierFont                            |
%     |                                                       |
%     +-------------------------------------------------------+
%                                                             %
\DigitFont{it}%         %
\IdentifierFont{it}%    %
%                                                             %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%%  Miscellaneous
%
\DefLanguage{Casl}                                 %
%                                                  %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%
%% The main environments: "opal" and "embeddedopal"
%% ---------------------
%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                  %
\newenvironment{casl}{%                            % LaTeX!
   \bgroup%                                        %
   \Casl@NormalSymbols%                            %
   \CaslPrelude%                                   %
   \begin{program}%                                %
   }{%                                             %
   \end{program}%                                  %
   \egroup%                                        %
   }%                                              %
%                                                  %
\def\@EmbeddedProgramPrelude{%                     %
   \Casl@NormalSymbols%                            %
   }%                                              %
\def\CaslPrelude{\relax}%                          %
%                                                  %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Special symbols
%%                
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                  %
\def\Casl@NormalSymbols{%                          %
  \catcode`\_=12%                                  %
  \catcode`\^=12%                                  %
  \catcode`\#=12%                                  %
  \catcode`\&=12%                                  %
  \catcode`\%=12%                                  %
  \catcode`\@=11%                                  %
  \@DefNormSymb%                                   %
  \def\Backslash{\texttt{\@Backslash}}             %
}%                                                 %
{
  \catcode`\#=12
  \catcode`\&=12
  \catcode`\%=12
  \gdef\@DefNormSymb{
    \SetSymbol{#}{\mathop{\@TxtIde{\@Hashmark}}}
    \SetSymbol{&}{\mathbin{\@TxtIde{\@Ampersand}}}
    \SetSymbol{%}{\mathbin{\@TxtIde{\@Percent}}}
    \SetSymbol{@}{\@TxtIde{\@At}}
    }
}
%                                                  %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% CASL keywords and special symbols
%%                
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\SpecName}[1]{\IdentifierFont{sc}\DigitFont{sc}\textsc{#1}}
%
%
\SetSymbol{exists}{\exists}
\SetSymbol{Forall}{\forall}
\SetSymbol{in}{\in}
\SetSymbol{not}{\neg}
\SetSymbol{exeq}{\stackrel{e}{=}}
% def is normal identifier
\SetCommand{And}{\KeyWord{and}}
\SetCommand{To}{\KeyWord{to}}
\SetCommand{End}{\@TopKW{\KeyWord}{end}}
\SetCommand{forall}{\@MainKW{\KeyWord}{forall}}
\SetCommand{Dot}{\@MainKW{}{{\scriptstyle\bullet}\;}}
\SetCommand{Program}{\@MainKW{\KeyWord}{program}}
\SetCommand{internal}{\@MainKW{\KeyWord}{internal}}
% else is normal identifier
%
\SetSymbol{--}{\UaCmnt}
\SetSymbol{.}{\;{\scriptstyle\bullet}\;}
\SetSymbol{;}{;~}
\SetSymbol{|}{~|~}
\SetSymbol{->?}{\to?\,}
\SetSymbol{.!}{\;{\scriptstyle\bullet}!\;}
\SetSymbol{__}{\underline{~~}}
\SetSymbol{_}{\underline{~}}
\SetSymbol{=!}{\stackrel{e}{=}}
\SetSymbol{*}{\times}
\SetSymbol{[]}{\texttt{[]}}
\SetSymbol{::=}{::=}
%
\def\CaslTopKeyWord#1{\TopKeyWord[3em]{#1}}
%
\CaslTopKeyWord{spec}
\CaslTopKeyWord{then}
\CaslTopKeyWord{arch}
\CaslTopKeyWord{unit}
\CaslTopKeyWord{units}
\CaslTopKeyWord{library}
\CaslTopKeyWord{view}
\CaslTopKeyWord{from}
%
\def\CaslMainKeyWord#1{\MainKeyWord[3em]{#1}}
%
\MainKeyWord{free}
\MainKeyWord{generated}
\CaslMainKeyWord{var}
\CaslMainKeyWord{vars}
\CaslMainKeyWord{op}
\CaslMainKeyWord{ops}
\CaslMainKeyWord{pred}
\CaslMainKeyWord{preds}
\CaslMainKeyWord{sort}
\CaslMainKeyWord{sorts}
\CaslMainKeyWord{type}
\CaslMainKeyWord{types}
%
\FollowKeyWord[1em]{COMPLETELY}
\FollowKeyWord{get}
\FollowKeyWord{given}
%
\BeginKeyWord{LET}
%
\IfLikeKeyWord{IF}
\IfLikeKeyWord[1em]{OTHERWISE}
%                                                   %
\ThenLikeKeyWord{THEN}    
%
% \ElseLikeKeyWord{else}  %% does not work!
%
% \EndKeyWord{end}
%
%\PlainKeyWord{as}
%\PlainKeyWord{assoc}
%\PlainKeyWord{comm}
%\PlainKeyWord{false}
\PlainKeyWord{fit}
\PlainKeyWord{hide}
%\PlainKeyWord{idem}
% \PlainKeyWord{lambda} %% collides with \lambda
\PlainKeyWord{local}
\PlainKeyWord{result}
\PlainKeyWord{reveal}
% \PlainKeyWord{and}    %% does this work?
% \PlainKeyWord{to}     %% does collide with \to 
%\PlainKeyWord{true}
\PlainKeyWord{version}
\PlainKeyWord{with}
\PlainKeyWord{within}
%\PlainKeyWord{not}    %% not bold
% \PlainKeyWord{def}   %% does not work!
%\PlainKeyWord{when}   %% not bold 
% \PlainKeyWord{if}    %% does not work!
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Finally: Set special symbols
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%\SetAllSymbols
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% End of file `caslx.sty'
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
