@@ -6,25 +6,31 @@
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', `default', and `stdout' listings style.
8%% + Defines a `numbers', `default', and `stdout' listings style.
9−%% + default :: default for Idris which is to use a tt font.
9+%% + default :: Uses TT font for code and SF font for comments,
10+%% and indented by parident.
10%% + numbers :: default but with numbers.
11%% + numbers :: default but with numbers.
12+%% + beamer :: default minus parindent
11%% + stdout :: for formatting stdout.
13%% + stdout :: for formatting stdout.
12%% + Defines a `code' environment for typesetting idris.
14%% + Defines a `code' environment for typesetting idris.
13%% + \begin{code}[...] ... \end{code}
15%% + \begin{code}[...] ... \end{code}
14%% + Defines an input command for externally defined idris files.
16%% + Defines an input command for externally defined idris files.
15%% + \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.
16%% + Defines commands typesetting the name Idris.
21%% + Defines commands typesetting the name Idris.
17%% + \Idris{}
22%% + \Idris{}
18%% + \idris{}
23%% + \idris{}
20%% Options:
25%% Options:
21%% - literate :: turn on literate idris for code environments.
26%% - literate :: turn on literate idris for code environments.
22−%% - numbers :: turn on numbers for code environments.
24%% ----------------------------------------------------------- [ Begin Package ]
28%% ----------------------------------------------------------- [ Begin Package ]
25\ProvidesPackage{idrislang}
29\ProvidesPackage{idrislang}
27\RequirePackage{ifthen}
31\RequirePackage{ifthen}
32+\RequirePackage{xcolor}
33+\RequirePackage{fancyvrb}
28\RequirePackage{listings}
34\RequirePackage{listings}
29\RequirePackage{xspace}
35\RequirePackage{xspace}
30\RequirePackage{textcomp}
36\RequirePackage{textcomp}
@@ -32,22 +38,26 @@
32%% ----------------------------------------------------------------- [ Options ]
38%% ----------------------------------------------------------------- [ Options ]
33\newboolean{literate}
39\newboolean{literate}
34\setboolean{literate}{false}
40\setboolean{literate}{false}
36−\setboolean{numbers}{false}
38\DeclareOption{literate}{%
42\DeclareOption{literate}{%
39 \setboolean{literate}{true}
43 \setboolean{literate}{true}
42−\DeclareOption{numbers}{%
43− \setboolean{numbers}{true}
46\ProcessOptions\relax
46\ProcessOptions\relax
48%% ---------------------------------------------------------------- [ Commands ]
48%% ---------------------------------------------------------------- [ Commands ]
49\newcommand{\Idris}{\textsc{Idris}\xspace}
49\newcommand{\Idris}{\textsc{Idris}\xspace}
50\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=\\\{\}}
52%% --------------------------------------------------- [ Define Idris Listings ]
62%% --------------------------------------------------- [ Define Idris Listings ]
53\lstdefinelanguage{idris}{%
63\lstdefinelanguage{idris}{%
@@ -121,6 +131,11 @@
121 escapechar=^
131 escapechar=^
134+\lstdefinestyle{beamer}{%
135+ basicstyle=\ttfamily\normalsize,
124%% ------------------------------------------------------ [ A Code Environment ]
139%% ------------------------------------------------------ [ A Code Environment ]
125%% Replicate the existence of literate haskell code environments,
140%% Replicate the existence of literate haskell code environments,
126%% option to make pretty with numbers.
141%% option to make pretty with numbers.
@@ -128,10 +143,7 @@
128 {\ifthenelse{\boolean{literate}}{%
143 {\ifthenelse{\boolean{literate}}{%
129 \lstset{language=literateidris}}{%
144 \lstset{language=literateidris}}{%
130 \lstset{language=idris}}
145 \lstset{language=idris}}
131− \ifthenelse{\boolean{numbers}}{%
146+ \IdrisLineSpacing{}
132− \lstset{style=numbers, #1}}{%
133− \lstset{style=default, #1}}
136%% ---------------------------------------------------------- [ Input Listings ]
148%% ---------------------------------------------------------- [ Input Listings ]
137%% Command to add externally defined Idris code to the document.
149%% Command to add externally defined Idris code to the document.
@@ -140,9 +152,6 @@
140 \ifthenelse{\boolean{literate}}{%
152 \ifthenelse{\boolean{literate}}{%
141 \lstset{language=literateidris}}{%
153 \lstset{language=literateidris}}{%
142 \lstset{language=idris}}
154 \lstset{language=idris}}
143− \ifthenelse{\boolean{numbers}}{%
144− \lstset{style=numbers}}{%
145− \lstset{style=default}}
146 \lstinputlisting[#1]{#2}
155 \lstinputlisting[#1]{#2}