% Listing style definition for the Lean Theorem Prover.
% Defined by Jeremy Avigad, 2015, by modifying Assia Mahboubi's SSR style.
% Unicode replacements taken from Olivier Verdier's unixode.sty
% Extensions by Jasmin Blanchette.

\lstdefinelanguage{minijavaandc} {

% Anything betweeen $ becomes LaTeX math mode
mathescape=true,
% Comments may or not include Latex commands
texcl=false,

alsoletter={\#},

procnamekeys={class,interface},

morekeywords=[1]{
  public, interface, class, implements, int, this, enum, struct, char, union,
  sizeof, return, if, else, try, throw, catch, new
},

morekeywords=[3]{\#include},

% Comments
%comment=[s][\itshape \color{commentcolor}]{/-}{-/},
morecomment=[s][\color{commentcolor}]{/-}{-/},
morecomment=[l][\itshape \color{commentcolor}]{//},

% Spaces are not displayed as a special character
showstringspaces=false,

% keep spaces
keepspaces=true,

% String delimiters
morestring=[b]",
morestring=[d],

% Size of tabulations
tabsize=3,

% Enables ASCII chars 128 to 255
extendedchars=false,

% Case sensitivity
sensitive=true,

% Automatic breaking of long lines
breaklines=true,

% Default style fors listingsred
basicstyle=\ttfamily,

% Position of captions is bottom
captionpos=b,

% Full flexible columns
columns=[l]fullflexible,


% Style for (listings') identifiers
identifierstyle={\ttfamily\color{black}},
% Note : highlighting of Coq identifiers is done through a new
% delimiter definition through an lstset at the begining of the
% document. Don't know how to do better.

% Style for declaration keywords
keywordstyle=[1]{\ttfamily\color{keywordcolor}},

% Style for preprocessorcolor keywords
keywordstyle=[3]{\ttfamily\color{preprocessorcolor}},

% Style for strings
stringstyle=\ttfamily,

% Style for comments
% commentstyle={\ttfamily\footnotesize },

}
