@@ -5,23 +5,32 @@
55%% + Provides a listings bindings:
66%% + idris :: default ascii
77%% + literateidris :: convert ascii maths to math symbols.
8−%% + Defines a `numbers' and `default' listings style.
8+%% + Defines a `numbers', `default', and `stdout' listings style.
9+%% + default :: Uses TT font for code and SF font for comments,
10+%% and indented by parident.
11+%% + numbers :: default but with numbers.
12+%% + beamer :: default minus parindent
13+%% + stdout :: for formatting stdout.
914%% + Defines a `code' environment for typesetting idris.
1015%% + \begin{code}[...] ... \end{code}
1116%% + Defines an input command for externally defined idris files.
1217%% + \inputIdrisListing[...]{file.idr}
18+%% + Provides definitions (from Idris Compiler) for pretty-printing Idris
19+%% code using Fancy Verbatim and colour commands.
20+%% + Sets commandchars for latex commands.
1321%% + Defines commands typesetting the name Idris.
1422%% + \Idris{}
1523%% + \idris{}
1624%%
1725%% Options:
1826%% - literate :: turn on literate idris for code environments.
19−%% - numbers :: turn on numbers for code environments.
2027%%
2128%% ----------------------------------------------------------- [ Begin Package ]
2229\ProvidesPackage{idrislang}
2330
2431\RequirePackage{ifthen}
32+\RequirePackage{xcolor}
33+\RequirePackage{fancyvrb}
2534\RequirePackage{listings}
2635\RequirePackage{xspace}
2736\RequirePackage{textcomp}
@@ -29,22 +38,26 @@
2938%% ----------------------------------------------------------------- [ Options ]
3039\newboolean{literate}
3140\setboolean{literate}{false}
32−\newboolean{numbers}
33−\setboolean{numbers}{false}
3441
3542\DeclareOption{literate}{%
3643 \setboolean{literate}{true}
3744}
3845
39−\DeclareOption{numbers}{%
40− \setboolean{numbers}{true}
41−}
42−
4346\ProcessOptions\relax
4447
4548%% ---------------------------------------------------------------- [ Commands ]
4649\newcommand{\Idris}{\textsc{Idris}\xspace}
4750\newcommand{\idris}{\textsc{Idris}\xspace}
51+\newcommand{\IdrisLineSpacing}{\singlespacing}
52+%% ---------------------------------------------------------- [ Color Commands ]
53+\newcommand{\IdrisData}[1]{\textcolor{red}{#1}}
54+\newcommand{\IdrisType}[1]{\textcolor{blue}{#1}}
55+\newcommand{\IdrisBound}[1]{\textcolor{magenta}{#1}}
56+\newcommand{\IdrisFunction}[1]{\textcolor{green}{#1}}
57+\newcommand{\IdrisKeyword}[1]{{\underline{#1}}}
58+\newcommand{\IdrisImplicit}[1]{{\itshape \IdrisBound{#1}}}
59+
60+\fvset{commandchars=\\\{\}}
4861
4962%% --------------------------------------------------- [ Define Idris Listings ]
5063\lstdefinelanguage{idris}{%
@@ -67,7 +80,7 @@
6780},
6881%% ------------------------------------------------------- [ Prelude Functions ]
6982 morekeywords={%
70− class, data, instance, record, dsl, postulate, default,
83+ class, data, instance, record, dsl, postulate, default,
7184 lambda, variable, index_first, index_next
7285 },
7386%% ---------------------------------------------------------------- [ Comments ]
@@ -89,7 +102,7 @@
89102 {>=}{{$\geq$}}2
90103 {<-}{{$\leftarrow$}}2
91104 {<=}{{$\leq$}}2
92− {=>}{{$\Rightarrow$}}2
105+ {=>}{{$\Rightarrow$}}2
93106 {==}{{$\equiv$}}2
94107 {\ .}{{$\circ$}}2
95108 {\ .\ }{{$\circ$}}2
@@ -100,8 +113,9 @@
100113%% -------------------------------------------------- [ Default Listings Style ]
101114
102115\lstdefinestyle{default}{%
103− basicstyle=\ttfamily
116+ basicstyle=\ttfamily\normalsize,
104117}
118+
105119\lstdefinestyle{numbers}{%
106120 numbers=left,
107121 numbersep=10pt,
@@ -109,6 +123,19 @@
109123 frame=leftline
110124}
111125
126+\lstdefinestyle{stdout}{%
127+ xleftmargin=\parindent,
128+ tabsize=2,
129+ basicstyle=\ttfamily\normalsize,
130+ showstringspaces=false,
131+ escapechar=^
132+}
133+
134+\lstdefinestyle{beamer}{%
135+ basicstyle=\ttfamily\normalsize,
136+ escapechar=^
137+}
138+
112139%% ------------------------------------------------------ [ A Code Environment ]
113140%% Replicate the existence of literate haskell code environments,
114141%% option to make pretty with numbers.
@@ -116,10 +143,7 @@
116143 {\ifthenelse{\boolean{literate}}{%
117144 \lstset{language=literateidris}}{%
118145 \lstset{language=idris}}
119− \ifthenelse{\boolean{numbers}}{%
120− \lstset{style=numbers, #1}}{%
121− \lstset{style=default, #1}}
122− \singlespacing
146+ \IdrisLineSpacing{}
123147 }{}
124148%% ---------------------------------------------------------- [ Input Listings ]
125149%% Command to add externally defined Idris code to the document.
@@ -128,9 +152,6 @@
128152 \ifthenelse{\boolean{literate}}{%
129153 \lstset{language=literateidris}}{%
130154 \lstset{language=idris}}
131− \ifthenelse{\boolean{numbers}}{%
132− \lstset{style=numbers}}{%
133− \lstset{style=default}}
134155 \lstinputlisting[#1]{#2}
135156\endgroup
136157}