%% To import in the preambule
%\usepackage{listings}

\lstdefinelanguage{ML}{
  alsoletter={*},
  morekeywords={datatype, of, if, *},
  sensitive=true,
  morecomment=[s]{/*}{*/},
  morestring=[b]"
}

\lstdefinelanguage{tptp}{
  alsolanguage=Prolog,
  morekeywords={axiom, conjecture},
  keywordstyle={\color{blue}},
  columns=flexible,
  basicstyle={\small\ttfamily}
}

\lstdefinelanguage{console}{
  keywords={}
}

% "define" Scala
\lstdefinelanguage{scala}{
  alsoletter={@,=,>},
  morekeywords={end,abstract, case, catch, class, def, do, else, extends, false, final, finally, for, if, implicit, import, lazy, match, new, null, object,
override, package, private, protected, requires, return, sealed, super, then, this, throw, trait, try, true, type, val, var, while, with, yield, domain, 
postcondition, precondition,invariant, constraint, assert, assume, forAll, in, _, return, @generator, ensure, require, ensuring,=>},
  sensitive=true,
  morecomment=[l]{//},
  morecomment=[s]{/*}{*/},
  morestring=[b]"
}

\lstdefinelanguage{pscala}{
  alsoletter={@,=,>},
  morekeywords={abstract, case, catch, class, def, do, else, extends, false, final, finally, for, if, implicit, import, lazy, match, new, null, object,
override, package, private, protected, requires, return, sealed, super, then, this, throw, trait, try, true, type, val, var, while, with, yield, domain, 
postcondition, precondition,invariant, constraint, assert, assume, forAll, in, _, return, @generator, ensure, require, ensuring,=>},
  sensitive=true,
  morecomment=[l]{//},
  morecomment=[s]{/*}{*/},
  morestring=[b]"
}

\lstdefinelanguage{automath}{
  sensitive=true,
}

\lstdefinelanguage{pscala}{
  alsoletter={@,=,>},
  morekeywords={abstract, case, catch, class, def, do, else, extends, false, final, finally, for, if, implicit, import, lazy, match, new, null, object,
override, package, private, protected, requires, return, sealed, super, then, this, throw, trait, try, true, type, val, var, while, with, yield, domain, 
postcondition, precondition,invariant, constraint, assert, assume, forAll, in, _, return, @generator, ensure, require, ensuring,=>},
  sensitive=true,
  morecomment=[l]{//},
  morecomment=[s]{/*}{*/},
  morestring=[b]"
}

\lstdefinelanguage{isabelle}{
  basicstyle=\tiny,
  alsoletter={@,=,>},
  morekeywords={lemma,proof,show,have,also,finally,qed,next,assume,finally,fix,by}
  sensitive=true,
  morecomment=[s]{(*}{*)},
  morestring=[b]"  
}

\newcommand{\codestyle}{\small\sffamily}
%\newcommand{\codestyle}{\ttfamily\small}

%\newcommand{\union}{\mbox{\tt ++}}
%\newcommand{\difference}{\mbox{\tt --}}
%\newcommand{\RA}{\mbox{\tt =>}}
\newcommand{\RA}{\Rightarrow}
\newcommand{\EQ}{\mbox{\tt ==}}

% Default settings for code listings
\lstset{
%  frame=tb,
  language=scala,
%  aboveskip=3mm,
%  belowskip=3mm,
%  lineskip=-0.1em,
  showstringspaces=false,
  columns=fullflexible,
  mathescape=true,
  numbers=none,
  numberstyle=\tiny,
  basicstyle=\codestyle,
  commentstyle=\codestyle\color{blue}
} 

%\newenvironment{scala}
%        {\lstset{language=scala}\begin{lstlisting}}
%        {\end{lstlisting}}
