on master help sign in
Several updates to idrislang.sty

+ Removal of numbers package option. Listing styles must be set either globally using `\lstset{}` or per code or listings environment options. + Addition of a beamer style. + Inclusion of the `:pprint` LaTeX formatting commands. No more need to copy everything from the result of `:pprint`, just the code snippet. + command chars for fancy verbatim has been set globally. + Option to change spacing command, useful for cases where line spacing is changed via different commands. For example: memoir has `\SingleSpacing`, setspace has `\singlespacing`.

commit64f9d19ca8ba125f093ab35c0edf7c5397b31963 authorJan de Muijnck-Hughes <jfdm@st-andrews.ac.uk> dateWed 10 Dec 2014, 00:16 (12 years ago) parent8698e57
1 file changed+24−15
contribs/idrislang.sty+24−15
contribs/idrislang.sty+24−15
@@ -6,25 +6,31 @@
66%% + idris :: default ascii
77%% + literateidris :: convert ascii maths to math symbols.
88%% + 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.
1011%% + numbers :: default but with numbers.
12+%% + beamer :: default minus parindent
1113%% + stdout :: for formatting stdout.
1214%% + Defines a `code' environment for typesetting idris.
1315%% + \begin{code}[...] ... \end{code}
1416%% + Defines an input command for externally defined idris files.
1517%% + \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.
1621%% + Defines commands typesetting the name Idris.
1722%% + \Idris{}
1823%% + \idris{}
1924%%
2025%% Options:
2126%% - literate :: turn on literate idris for code environments.
22−%% - numbers :: turn on numbers for code environments.
2327%%
2428%% ----------------------------------------------------------- [ Begin Package ]
2529\ProvidesPackage{idrislang}
2630
2731\RequirePackage{ifthen}
32+\RequirePackage{xcolor}
33+\RequirePackage{fancyvrb}
2834\RequirePackage{listings}
2935\RequirePackage{xspace}
3036\RequirePackage{textcomp}
@@ -32,22 +38,26 @@
3238%% ----------------------------------------------------------------- [ Options ]
3339\newboolean{literate}
3440\setboolean{literate}{false}
35−\newboolean{numbers}
36−\setboolean{numbers}{false}
3741
3842\DeclareOption{literate}{%
3943 \setboolean{literate}{true}
4044}
4145
42−\DeclareOption{numbers}{%
43− \setboolean{numbers}{true}
44−}
45−
4646\ProcessOptions\relax
4747
4848%% ---------------------------------------------------------------- [ Commands ]
4949\newcommand{\Idris}{\textsc{Idris}\xspace}
5050\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=\\\{\}}
5161
5262%% --------------------------------------------------- [ Define Idris Listings ]
5363\lstdefinelanguage{idris}{%
@@ -121,6 +131,11 @@
121131 escapechar=^
122132}
123133
134+\lstdefinestyle{beamer}{%
135+ basicstyle=\ttfamily\normalsize,
136+ escapechar=^
137+}
138+
124139%% ------------------------------------------------------ [ A Code Environment ]
125140%% Replicate the existence of literate haskell code environments,
126141%% option to make pretty with numbers.
@@ -128,10 +143,7 @@
128143 {\ifthenelse{\boolean{literate}}{%
129144 \lstset{language=literateidris}}{%
130145 \lstset{language=idris}}
131− \ifthenelse{\boolean{numbers}}{%
132− \lstset{style=numbers, #1}}{%
133− \lstset{style=default, #1}}
134− \singlespacing
146+ \IdrisLineSpacing{}
135147 }{}
136148%% ---------------------------------------------------------- [ Input Listings ]
137149%% Command to add externally defined Idris code to the document.
@@ -140,9 +152,6 @@
140152 \ifthenelse{\boolean{literate}}{%
141153 \lstset{language=literateidris}}{%
142154 \lstset{language=idris}}
143− \ifthenelse{\boolean{numbers}}{%
144− \lstset{style=numbers}}{%
145− \lstset{style=default}}
146155 \lstinputlisting[#1]{#2}
147156\endgroup
148157}