git.iko.soy/Idris-dev
on master help sign in
Merge pull request #701 from jfdm/contrib/idrislang.sty
2397a17Edwin Brady
contribs/idrislang.sty+19−1
compare with master
unifiedsplit
@@ -8,6 +8,8 @@
8%% + Defines a `numbers' and `default' listings style.
8%% + Defines a `numbers' and `default' listings style.
9%% + Defines a `code' environment for typesetting idris.
9%% + Defines a `code' environment for typesetting idris.
10%% + \begin{code}[...] ... \end{code}
10%% + \begin{code}[...] ... \end{code}
11+%% + Defines an input command for externally defined idris files.
12+%% + \inputIdrisListing[...]{file.idr}
11%% + Defines commands typesetting the name Idris.
13%% + Defines commands typesetting the name Idris.
12%% + \Idris{}
14%% + \Idris{}
13%% + \idris{}
15%% + \idris{}
@@ -46,6 +48,8 @@
46\lstdefinelanguage{idris}{%
48\lstdefinelanguage{idris}{%
47 sensitive,%
49 sensitive,%
48%% ----------------------------------------------------------- [ Default Style ]
50%% ----------------------------------------------------------- [ Default Style ]
51+ xleftmargin=\parindent,
52+ tabsize=2,
49 basicstyle=\ttfamily,
53 basicstyle=\ttfamily,
50 flexiblecolumns=false,
54 flexiblecolumns=false,
51 commentstyle=\footnotesize\sffamily,
55 commentstyle=\footnotesize\sffamily,
@@ -163,7 +167,8 @@
163
167
164\lstdefinestyle{default}{%
168\lstdefinestyle{default}{%
165 xleftmargin=\parindent,
169 xleftmargin=\parindent,
166− tabsize=2
170+ tabsize=2,
171+ basicstyle=\ttfamily
167}
172}
168\lstdefinestyle{numbers}{%
173\lstdefinestyle{numbers}{%
169 xleftmargin=\parindent,
174 xleftmargin=\parindent,
@@ -186,5 +191,18 @@
186 \lstset{style=default, #1}}
191 \lstset{style=default, #1}}
187 }
192 }
188 {}
193 {}
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+}
189\endinput
207\endinput
190%% --------------------------------------------------------------------- [ EOF ]
208%% --------------------------------------------------------------------- [ EOF ]