idris-lang/Idris-dev — pull request #1547 by david-christiansen (2014-09-24 19:37:26+00:00)
Title: New command :pprint for outputting paper/slide bits

The command:

:pprint fmt width n

outputs the definition of name n for format FMT, with a screen width of
WIDTH columns.

:pprint fmt width tm

outputs the term TM.

The allowed formats are "html" and "latex".

Sample output:
```
Idris> :pprint latex 80 Vect
\documentclass{article}
\usepackage{fancyvrb}
\usepackage[usenames]{xcolor}
\newcommand{\IdrisData}[1]{\textcolor{red}{#1}}
\newcommand{\IdrisType}[1]{\textcolor{blue}{#1}}
\newcommand{\IdrisBound}[1]{\textcolor{magenta}{#1}}
\newcommand{\IdrisFunction}[1]{\textcolor{green}{#1}}
\newcommand{\IdrisKeyword}[1]{{\underline{#1}}}
\newcommand{\IdrisImplicit}[1]{{\itshape \IdrisBound{#1}}}

\begin{document}
% START CODE
\begin{Verbatim}[commandchars=\\\{\}]
\IdrisKeyword{data} \IdrisType{Vect} : \IdrisType{Nat} -> \IdrisType{Type} -> \IdrisType{Type} \IdrisKeyword{where}
\IdrisData{Nil} : \IdrisType{Vect} \IdrisData{0} \IdrisImplicit{a}
\IdrisData{(::)} : \IdrisImplicit{a} -> \IdrisType{Vect} \IdrisImplicit{n} \IdrisImplicit{a} -> \IdrisType{Vect} (\IdrisData{S} \IdrisImplicit{n}) \IdrisImplicit{a}
\end{Verbatim}
% END CODE
\end{document}
Idris> :pprint html 80 Vect

data Vect : Nat -> Type -> Type where
Nil : Vect 0 a
(::) : a -> Vect n a -> Vect (S n) a

```