Commit 8fc62b38 authored by MARCHE Claude's avatar MARCHE Claude

doc now uses the distributed why3lang.sty file

parent 76fbca19
......@@ -42,8 +42,11 @@
%%% listings for Why3 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\RequirePackage{listings}
\RequirePackage{amssymb}
\usepackage{../share/latex/why3lang}
% \RequirePackage{listings}
% \RequirePackage{amssymb}
\lstset{
basicstyle={\ttfamily},
......@@ -54,41 +57,9 @@
commentstyle=\itshape,
columns=[l]fullflexible,
showstringspaces=false,
literate=%
}
\lstdefinelanguage{why3}
{
morekeywords={namespace,predicate,function,inductive,type,use,clone,%
import,export,theory,module,end,in,with,%
let,rec,for,to,do,done,match,if,then,else,while,try,invariant,variant,%
absurd,raise,assert,exception,private,abstract,mutable,ghost,%
downto,raises,writes,reads,requires,ensures,returns,val,model,%
goal,axiom,lemma,forall,meta},%
string=[b]",%
sensitive=true,%
morecomment=[s]{(*}{*)},%
keepspaces=true,
}
%literate=%
%{'a}{$\alpha$}{1}%
%{'b}{$\beta$}{1}%
%{<}{$<$}{1}%
%{>}{$>$}{1}%
%{<=}{$\le$}{1}%
%{>=}{$\ge$}{1}%
% {<>}{$\ne$}{1}%
% {/\\}{$\land$}{1}%
% {\\/}{ $\lor$ }{3}%
% {\ or(}{ $\lor$(}{3}%
% {not\ }{$\lnot$ }{1}%
% {not(}{$\lnot$(}{1}%
% {+->}{\texttt{+->}}{2}%
% % {+->}{$\mapsto$}{2}%
% {-->}{\texttt{-\relax->}}{2}%
% %{-->}{$\longrightarrow$}{2}%
% {->}{$\rightarrow$}{2}%
% {<->}{$\leftrightarrow$}{2}%
\lstnewenvironment{whycode}{\lstset{language=why3}}{}
\lstnewenvironment{ocamlcode}{\lstset{language={[Objective]Caml}}}{}
......
......@@ -4,13 +4,16 @@
\lstdefinelanguage{why3}
{
basicstyle=\ttfamily,
morekeywords=[1]{predicate,constant,function,goal,type,use,%
import,theory,end,in,%
mutable,invariant,model,requires,ensures,raises,returns,reads,writes,diverges,%
variant,let,val,while,for,loop,abstract,private,any,assert,assume,check,%
fun,rec,clone,if,then,else,result,old,ghost,by,so%
axiom,lemma,export,forall,exists,match,with,try,not,inductive,coinductive},%
basicstyle=\ttfamily,%
morekeywords=[1]{abstract,absurd,any,assert,assume,axiom,by,%
check,clone,coinductive,constant,diverges,do,done,downto,%
else,end,ensures,exception,exists,export,for,forall,fun,%
function,ghost,goal,if,import,in,inductive,invariant,lemma,%
let,loop,match,meta,model,module,mutable,namespace,not,old,%
predicate,private,raise,raises,reads,rec,requires,result,%
returns,so,then,theory,to,try,type,use,val,variant,while,%
with,writes},%
string=[b]",%
%keywordstyle=[1]{\color{red}},%
morekeywords=[2]{true,false},%
%keywordstyle=[2]{\color{blue}},%
......@@ -20,27 +23,27 @@ columns=[l]fullflexible,%
sensitive=true,%
morecomment=[s]{(*}{*)},%
escapeinside={*?}{?*},%
keepspaces=true,
keepspaces=true,%
literate=%
%{'a}{$\alpha$}{1}%
%{'b}{$\beta$}{1}%
{<}{$<$}{1}%
{>}{$>$}{1}%
{<=}{$\le$}{1}%
{>=}{$\ge$}{1}%
{<>}{$\ne$}{1}%
{/\\}{$\land$}{1}%
{\\/}{ $\lor$ }{3}%
{\ or(}{ $\lor$(}{3}%
% {'a}{$\alpha$}{1}%
% {'b}{$\beta$}{1}%
% {<}{$<$}{1}%
% {>}{$>$}{1}%
% {<=}{$\le$}{1}%
% {>=}{$\ge$}{1}%
% {<>}{$\ne$}{1}%
% {/\\}{$\land$}{1}%
% {\\/}{ $\lor$ }{3}%
% {\ or(}{ $\lor$(}{3}%
% {not\ }{$\lnot$ }{1}%
% {not(}{$\lnot$(}{1}%
{+->}{\texttt{+->}}{2}%
% {+->}{\texttt{+->}}{2}%
% {+->}{$\mapsto$}{2}%
{-->}{\texttt{-\relax->}}{2}%
%{-->}{$\longrightarrow$}{2}%
{->}{$\rightarrow$}{2}%
{<-}{$\leftarrow$}{2}%
{<->}{$\leftrightarrow$}{2}%
% {-->}{\texttt{-\relax->}}{2}%
% {-->}{$\longrightarrow$}{2}%
% {->}{$\rightarrow$}{2}%
% {<-}{$\leftarrow$}{2}%
% {<->}{$\leftrightarrow$}{2}%
%
%
}
......@@ -48,4 +51,3 @@ literate=%
\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