macros.tex 2.86 KB
Newer Older
1

2
\newcommand{\todo}[1]{{\Huge\bfseries TODO: #1}}
3

MARCHE Claude's avatar
MARCHE Claude committed
4
\newcommand{\why}{\textsf{Why3}\xspace}
5
\newcommand{\whyml}{\textsf{WhyML}\xspace}
6
\newcommand{\eg}{\emph{e.g.}\xspace}
7
\newcommand{\ie}{\emph{i.e.}\xspace}
MARCHE Claude's avatar
MARCHE Claude committed
8

9 10
\newcommand{\emptyitem}{\begin{latexonly}~\end{latexonly}}

MARCHE Claude's avatar
MARCHE Claude committed
11
% BNF grammar
12
\newcommand{\keyword}[1]{\texttt{#1}}
MARCHE Claude's avatar
MARCHE Claude committed
13 14 15 16 17
\newcommand{\indextt}[1]{\index{#1@\protect\keyword{#1}}}
\newcommand{\indexttbs}[1]{\index{#1@\protect\keywordbs{#1}}}
\newif\ifspace
\newif\ifnewentry
\newcommand{\addspace}{\ifspace ~ \spacefalse \fi}
18
\newcommand{\term}[2]{\addspace\mbox{\lstinline|#1|%
MARCHE Claude's avatar
MARCHE Claude committed
19 20 21
\ifthenelse{\equal{#2}{}}{}{\indexttbase{#2}{#1}}}\spacetrue}
\newcommand{\nonterm}[2]{%
  \ifthenelse{\equal{#2}{}}%
22 23
             {\addspace\mbox{\textsl{#1}\ifnewentry\index{#1@\textsl{#1}}\fi}\spacetrue}%
             {\addspace\mbox{\textsl{#1}\footnote{#2}\ifnewentry\index{grammar entries!\textsl{#1}}\fi}\spacetrue}}
MARCHE Claude's avatar
MARCHE Claude committed
24 25 26 27 28 29 30 31 32
\newcommand{\repetstar}{$^*$\spacetrue}
\newcommand{\repetplus}{$^+$\spacetrue}
\newcommand{\repetone}{$^?$\spacetrue}
\newcommand{\lparen}{\addspace(}
\newcommand{\rparen}{)}
\newcommand{\orelse}{\addspace$\mid$\spacetrue}
\newcommand{\sep}{ \\[2mm] \spacefalse\newentrytrue}
\newcommand{\newl}{ \\ & & \spacefalse}
\newcommand{\alt}{ \\ & $\mid$ & \spacefalse}
33
\newcommand{\is}{ & $::=$ & \spacefalse\newentryfalse}
MARCHE Claude's avatar
MARCHE Claude committed
34 35 36 37
\newenvironment{syntax}{\begin{tabular}{@{}rrll@{}}\spacefalse\newentrytrue}{\end{tabular}}
\newcommand{\synt}[1]{$\spacefalse#1$}
\newcommand{\emptystring}{$\epsilon$}
\newcommand{\below}{See\; below}
38

39 40 41 42 43
%%% listings for Why3 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\RequirePackage{listings}
\RequirePackage{amssymb}

44 45 46 47 48 49 50 51 52 53
\lstset{
  basicstyle={\ttfamily},
  framesep=2pt,
  frame=single,
  keywordstyle={\color{blue}},
  stringstyle=\itshape,
  commentstyle=\itshape,
  columns=[l]fullflexible,
  showstringspaces=false,
}
54 55 56

\lstdefinelanguage{why3}
{
57
morekeywords={namespace,predicate,function,inductive,type,use,clone,%
58 59
import,export,theory,module,end,in,with,%
let,rec,for,to,do,done,match,if,then,else,while,try,invariant,variant,%
60 61
absurd,raise,assert,exception,private,abstract,mutable,ghost,%
downto,raises,writes,reads,requires,ensures,returns,val,model,%
62 63 64 65 66
goal,axiom,lemma,forall},%
string=[b]",%
sensitive=true,%
morecomment=[s]{(*}{*)},%
keepspaces=true,
67 68
}
%literate=%
69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87
%{'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}%

88
\lstnewenvironment{whycode}{\lstset{language=why3}}{}
89
\lstnewenvironment{ocamlcode}{\lstset{language={[Objective]Caml}}}{}
90

MARCHE Claude's avatar
MARCHE Claude committed
91
%%% Local Variables:
92
%%% mode: latex
MARCHE Claude's avatar
MARCHE Claude committed
93
%%% TeX-master: "manual"
MARCHE Claude's avatar
MARCHE Claude committed
94 95
%%% TeX-PDF-mode: t
%%% End: