@@ -5,23 +5,32 @@
5%% + Provides a listings bindings:
5%% + Provides a listings bindings:
6%% + idris :: default ascii
6%% + idris :: default ascii
7%% + literateidris :: convert ascii maths to math symbols.
7%% + 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.
9%% + Defines a `code' environment for typesetting idris.
14%% + Defines a `code' environment for typesetting idris.
10%% + \begin{code}[...] ... \end{code}
15%% + \begin{code}[...] ... \end{code}
11%% + Defines an input command for externally defined idris files.
16%% + Defines an input command for externally defined idris files.
12%% + \inputIdrisListing[...]{file.idr}
17%% + \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.
13%% + Defines commands typesetting the name Idris.
21%% + Defines commands typesetting the name Idris.
14%% + \Idris{}
22%% + \Idris{}
15%% + \idris{}
23%% + \idris{}
17%% Options:
25%% Options:
18%% - literate :: turn on literate idris for code environments.
26%% - literate :: turn on literate idris for code environments.
19−%% - numbers :: turn on numbers for code environments.
21%% ----------------------------------------------------------- [ Begin Package ]
28%% ----------------------------------------------------------- [ Begin Package ]
22\ProvidesPackage{idrislang}
29\ProvidesPackage{idrislang}
24\RequirePackage{ifthen}
31\RequirePackage{ifthen}
32+\RequirePackage{xcolor}
33+\RequirePackage{fancyvrb}
25\RequirePackage{listings}
34\RequirePackage{listings}
26\RequirePackage{xspace}
35\RequirePackage{xspace}
27\RequirePackage{textcomp}
36\RequirePackage{textcomp}
@@ -29,22 +38,26 @@
29%% ----------------------------------------------------------------- [ Options ]
38%% ----------------------------------------------------------------- [ Options ]
30\newboolean{literate}
39\newboolean{literate}
31\setboolean{literate}{false}
40\setboolean{literate}{false}
33−\setboolean{numbers}{false}
35\DeclareOption{literate}{%
42\DeclareOption{literate}{%
36 \setboolean{literate}{true}
43 \setboolean{literate}{true}
39−\DeclareOption{numbers}{%
40− \setboolean{numbers}{true}
43\ProcessOptions\relax
46\ProcessOptions\relax
45%% ---------------------------------------------------------------- [ Commands ]
48%% ---------------------------------------------------------------- [ Commands ]
46\newcommand{\Idris}{\textsc{Idris}\xspace}
49\newcommand{\Idris}{\textsc{Idris}\xspace}
47\newcommand{\idris}{\textsc{Idris}\xspace}
50\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}}}
60+\fvset{commandchars=\\\{\}}
49%% --------------------------------------------------- [ Define Idris Listings ]
62%% --------------------------------------------------- [ Define Idris Listings ]
50\lstdefinelanguage{idris}{%
63\lstdefinelanguage{idris}{%
@@ -67,7 +80,7 @@
68%% ------------------------------------------------------- [ Prelude Functions ]
81%% ------------------------------------------------------- [ Prelude Functions ]
69 morekeywords={%
82 morekeywords={%
70− class, data, instance, record, dsl, postulate, default,
83+ class, data, instance, record, dsl, postulate, default,
71 lambda, variable, index_first, index_next
84 lambda, variable, index_first, index_next
73%% ---------------------------------------------------------------- [ Comments ]
86%% ---------------------------------------------------------------- [ Comments ]
@@ -89,7 +102,7 @@
89 {>=}{{$\geq$}}2
102 {>=}{{$\geq$}}2
90 {<-}{{$\leftarrow$}}2
103 {<-}{{$\leftarrow$}}2
91 {<=}{{$\leq$}}2
104 {<=}{{$\leq$}}2
92− {=>}{{$\Rightarrow$}}2
105+ {=>}{{$\Rightarrow$}}2
93 {==}{{$\equiv$}}2
106 {==}{{$\equiv$}}2
94 {\ .}{{$\circ$}}2
107 {\ .}{{$\circ$}}2
95 {\ .\ }{{$\circ$}}2
108 {\ .\ }{{$\circ$}}2
@@ -100,8 +113,9 @@
100%% -------------------------------------------------- [ Default Listings Style ]
113%% -------------------------------------------------- [ Default Listings Style ]
102\lstdefinestyle{default}{%
115\lstdefinestyle{default}{%
103− basicstyle=\ttfamily
116+ basicstyle=\ttfamily\normalsize,
105\lstdefinestyle{numbers}{%
119\lstdefinestyle{numbers}{%
106 numbers=left,
120 numbers=left,
107 numbersep=10pt,
121 numbersep=10pt,
@@ -109,6 +123,19 @@
109 frame=leftline
123 frame=leftline
126+\lstdefinestyle{stdout}{%
127+ xleftmargin=\parindent,
129+ basicstyle=\ttfamily\normalsize,
130+ showstringspaces=false,
134+\lstdefinestyle{beamer}{%
135+ basicstyle=\ttfamily\normalsize,
112%% ------------------------------------------------------ [ A Code Environment ]
139%% ------------------------------------------------------ [ A Code Environment ]
113%% Replicate the existence of literate haskell code environments,
140%% Replicate the existence of literate haskell code environments,
114%% option to make pretty with numbers.
141%% option to make pretty with numbers.
@@ -116,10 +143,7 @@
116 {\ifthenelse{\boolean{literate}}{%
143 {\ifthenelse{\boolean{literate}}{%
117 \lstset{language=literateidris}}{%
144 \lstset{language=literateidris}}{%
118 \lstset{language=idris}}
145 \lstset{language=idris}}
119− \ifthenelse{\boolean{numbers}}{%
146+ \IdrisLineSpacing{}
120− \lstset{style=numbers, #1}}{%
121− \lstset{style=default, #1}}
124%% ---------------------------------------------------------- [ Input Listings ]
148%% ---------------------------------------------------------- [ Input Listings ]
125%% Command to add externally defined Idris code to the document.
149%% Command to add externally defined Idris code to the document.
@@ -128,9 +152,6 @@
128 \ifthenelse{\boolean{literate}}{%
152 \ifthenelse{\boolean{literate}}{%
129 \lstset{language=literateidris}}{%
153 \lstset{language=literateidris}}{%
130 \lstset{language=idris}}
154 \lstset{language=idris}}
131− \ifthenelse{\boolean{numbers}}{%
132− \lstset{style=numbers}}{%
133− \lstset{style=default}}
134 \lstinputlisting[#1]{#2}
155 \lstinputlisting[#1]{#2}