doc now uses the distributed why3lang.sty file

doc/macros.tex

@@ -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}}}{}
 

share/latex/why3lang.sty

@@ -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}}
-