% event-b.tex --- Event-B language definition for listings -*-latex-*-

% Copyright (C) 2018 Nancy Day <nday@uwaterloo.ca>
% Copyright (C) 2018 Ali Abbassi <aabbassi@uwaterloo.ca>
% Copyright (C) 2018, 2020 Amin Bandali <bandali@uwaterloo.ca>

% This file is part of Amin Bandali's MMath thesis.

% This thesis is free software: you can redistribute it and/or modify
% it under the terms of the GNU General Public License as published by
% the Free Software Foundation, either version 3 of the License, or
% (at your option) any later version.

% This thesis is distributed in the hope that it will be useful,
% but WITHOUT ANY WARRANTY; without even the implied warranty of
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
% GNU General Public License for more details.

% You should have received a copy of the GNU General Public License
% along with this thesis.  If not, see <https://www.gnu.org/licenses/>.


\usepackage[formats]{listings}
% Define Language
\lstdefinelanguage{eventb}
{
	% list of keywords
	morekeywords={
        CONTEXT,
        AXIOMS,
		MACHINE,
		SETS,
		VARIABLES,
		INVARIANTS,
		DEFINITIONS,
		EVENTS,
		INITIALISATION,
		OPERATIONS,
		ASSERTIONS,
		SEES,
		PROMOTES,
		INCLUDES,
		USES,
		EXTENDS,
		IMPORTS,
		REFINES,
		CONSTANTS,
		PROPERTIES,
		BOOL,
		END,
		POW,
		POW1,
		INT,
		ANY,
        WHERE,
		THEN,
		GOAL,
        TRUE,
        FALSE,
        card,
        not
	},
	sensitive=true, % keywords are case-sensitive
	morecomment=[l]{//}, % l is for line comment
	morecomment=[s]{(*}{*)}, % s is for start and end delimiter
	morestring=[b]" % defines that strings are enclosed in double quotes
}



% Set Language
\lstdefinestyle{eventb}{
	language={eventb},
	basicstyle=\footnotesize\ttfamily, % Global Code Style
	captionpos=b, % Position of the Caption (t for top, b for bottom)
	extendedchars=true, % Allows 256 instead of 128 ASCII characters
	tabsize=2, % number of spaces indented when discovering a tab 
	columns=flexible, % make all characters equal width
	keepspaces=true, % does not ignore spaces to fit width, convert tabs to spaces
	showstringspaces=false, % lets spaces in strings appear as real spaces
	breaklines=true, % wrap lines if they don't fit
	%frame=trbl, % draw a frame at the top, right, left and bottom of the listing
	%frameround=tttt, % make the frame round at all four corners
	framesep=4pt, % quarter circle size of the round corners
	numbers=left, % show line numbers at the left
  numberstyle=\footnotesize\ttfamily, % style of the line numbers
	commentstyle=\color{eclipseGreen}, % style of comments
	keywordstyle=\bfseries\color{ceventb}, % style of keywords
	stringstyle=\color{eclipseBlue}, % style of strings
	xleftmargin=0.8cm,
	escapeinside={\%*}{*)}          % if you want to add LaTeX within your code
}

\newcommand{\eventbcode}[1]{\lstinline[style=eventb, basicstyle=\ttfamily]{#1}}


%% Local Variables:
%% tex-main-file: "../bandali-mmath-thesis.tex"
%% End:
