macros.tex 2.17 KB
Newer Older
1

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

MARCHE Claude's avatar
MARCHE Claude committed
8 9 10
\newcommand{\emptyitem}{%
%BEGIN LATEX
~
11
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
12
}
13

MARCHE Claude's avatar
MARCHE Claude committed
14
% BNF grammar
15
\newcommand{\keyword}[1]{\texttt{#1}}
MARCHE Claude's avatar
MARCHE Claude committed
16 17 18 19
\newcommand{\indextt}[1]{\index{#1@\protect\keyword{#1}}}
\newcommand{\indexttbs}[1]{\index{#1@\protect\keywordbs{#1}}}
\newif\ifspace
\newif\ifnewentry
20
\newcommand{\addspace}{\ifspace\:\:\spacefalse\fi}
21
\newcommand{\term}[2]{\addspace\mbox{\lstinline|#1|%
MARCHE Claude's avatar
MARCHE Claude committed
22 23 24
\ifthenelse{\equal{#2}{}}{}{\indexttbase{#2}{#1}}}\spacetrue}
\newcommand{\nonterm}[2]{%
  \ifthenelse{\equal{#2}{}}%
25 26
             {\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}}
27
\newcommand{\interval}{\addspace--\spacetrue}
MARCHE Claude's avatar
MARCHE Claude committed
28 29 30 31 32 33 34 35 36
\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}
37
\newcommand{\is}{ & $::=$ & \spacefalse\newentryfalse}
MARCHE Claude's avatar
MARCHE Claude committed
38 39 40 41
\newenvironment{syntax}{\begin{tabular}{@{}rrll@{}}\spacefalse\newentrytrue}{\end{tabular}}
\newcommand{\synt}[1]{$\spacefalse#1$}
\newcommand{\emptystring}{$\epsilon$}
\newcommand{\below}{See\; below}
42

43 44
%%% listings for Why3 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

45

MARCHE Claude's avatar
MARCHE Claude committed
46 47
% cannot use \usepackage here because it breaks hevea (no colored keywords anymore :-()
\input{../share/latex/why3lang.sty}
48 49 50

% \RequirePackage{listings}
% \RequirePackage{amssymb}
51

52 53 54 55 56 57 58 59 60 61
\lstset{
  basicstyle={\ttfamily},
  framesep=2pt,
  frame=single,
  keywordstyle={\color{blue}},
  stringstyle=\itshape,
  commentstyle=\itshape,
  columns=[l]fullflexible,
  showstringspaces=false,
}
62

63
\lstnewenvironment{whycode}{\lstset{language=why3}}{}
64
\lstnewenvironment{ocamlcode}{\lstset{language={[Objective]Caml}}}{}
65

MARCHE Claude's avatar
MARCHE Claude committed
66
%%% Local Variables:
67
%%% mode: latex
MARCHE Claude's avatar
MARCHE Claude committed
68
%%% TeX-master: "manual"
MARCHE Claude's avatar
MARCHE Claude committed
69 70
%%% TeX-PDF-mode: t
%%% End: