@@ -8,6 +8,8 @@
88%% + Defines a `numbers' and `default' listings style.
99%% + Defines a `code' environment for typesetting idris.
1010%% + \begin{code}[...] ... \end{code}
11+%% + Defines an input command for externally defined idris files.
12+%% + \inputIdrisListing[...]{file.idr}
1113%% + Defines commands typesetting the name Idris.
1214%% + \Idris{}
1315%% + \idris{}
@@ -46,6 +48,8 @@
4648\lstdefinelanguage{idris}{%
4749 sensitive,%
4850%% ----------------------------------------------------------- [ Default Style ]
51+ xleftmargin=\parindent,
52+ tabsize=2,
4953 basicstyle=\ttfamily,
5054 flexiblecolumns=false,
5155 commentstyle=\footnotesize\sffamily,
@@ -163,7 +167,8 @@
163167
164168\lstdefinestyle{default}{%
165169 xleftmargin=\parindent,
166− tabsize=2
170+ tabsize=2,
171+ basicstyle=\ttfamily
167172}
168173\lstdefinestyle{numbers}{%
169174 xleftmargin=\parindent,
@@ -186,5 +191,18 @@
186191 \lstset{style=default, #1}}
187192 }
188193 {}
194+%% ---------------------------------------------------------- [ Input Listings ]
195+%% Command to add externally defined Idris code to the document.
196+\newcommand{\inputIdrisListing}[2][]{%
197+\begingroup
198+ \ifthenelse{\boolean{literate}}{%
199+ \lstset{language=literateidris}}{%
200+ \lstset{language=idris}}
201+ \ifthenelse{\boolean{numbers}}{%
202+ \lstset{style=numbers}}{%
203+ \lstset{style=default}}
204+ \lstinputlisting[#1]{#2}
205+\endgroup
206+}
189207\endinput
190208%% --------------------------------------------------------------------- [ EOF ]