Commit 169c7ec1 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

LaTeX: a nicer lstlisting config

parent 52a889b5
...@@ -2,10 +2,14 @@ ...@@ -2,10 +2,14 @@
\RequirePackage{listings} \RequirePackage{listings}
\RequirePackage{amssymb} \RequirePackage{amssymb}
\lstdefinelanguage{Why3} \lstdefinelanguage{why3}
{ {
basicstyle=\ttfamily,
morekeywords=[1]{predicate,function,goal,type,use,import,theory,end,in,% morekeywords=[1]{predicate,function,goal,type,use,import,theory,end,in,%
axiom,lemma,export,forall,match,with,not,inductive},% mutable,invariant,model,requires,ensures,raises,returns,reads,writes,%
variant,let,val,while,for,loop,abstract,private,any,assert,assume,check,%
rec,clone,if,then,else,result,old,ghost,%
axiom,lemma,export,forall,exists,match,with,not,inductive,coinductive},%
%keywordstyle=[1]{\color{red}},% %keywordstyle=[1]{\color{red}},%
morekeywords=[2]{true,false},% morekeywords=[2]{true,false},%
%keywordstyle=[2]{\color{blue}},% %keywordstyle=[2]{\color{blue}},%
...@@ -17,8 +21,8 @@ morecomment=[s]{(*}{*)},% ...@@ -17,8 +21,8 @@ morecomment=[s]{(*}{*)},%
escapeinside={*?}{?*},% escapeinside={*?}{?*},%
keepspaces=true, keepspaces=true,
literate=% literate=%
{'a}{$\alpha$}{1}% %{'a}{$\alpha$}{1}%
{'b}{$\beta$}{1}% %{'b}{$\beta$}{1}%
{<}{$<$}{1}% {<}{$<$}{1}%
{>}{$>$}{1}% {>}{$>$}{1}%
{<=}{$\le$}{1}% {<=}{$\le$}{1}%
...@@ -34,7 +38,13 @@ literate=% ...@@ -34,7 +38,13 @@ literate=%
{-->}{\texttt{-\relax->}}{2}% {-->}{\texttt{-\relax->}}{2}%
%{-->}{$\longrightarrow$}{2}% %{-->}{$\longrightarrow$}{2}%
{->}{$\rightarrow$}{2}% {->}{$\rightarrow$}{2}%
{<-}{$\leftarrow$}{2}%
{<->}{$\leftrightarrow$}{2}% {<->}{$\leftrightarrow$}{2}%
% %
% %
} }
\lstnewenvironment{why3}{\lstset{language=why3}}{}
\newcommand{\whyf}[1]{\lstinline[language=why3]{#1}}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment