add agda.sty, to be safe

diff --git a/agda.sty b/agda.sty
new file mode 100644 (file)
index 0000000..850cd05
--- /dev/null
+++ b/agda.sty
@@ -0,0 +1,242 @@
+% ----------------------------------------------------------------------
+% Some useful commands when doing highlighting of Agda code in LaTeX.
+% ----------------------------------------------------------------------
+
+\ProvidesPackage{agda}
+
+\usepackage{ifxetex, xcolor, polytable, ifthen}
+
+% XeLaTeX
+\ifxetex
+    \usepackage{polyglossia}
+    \usepackage{fontspec}
+    \usepackage[]{unicode-math}
+
+% pdfLaTeX
+\else
+    \usepackage{ucs, amsfonts, amssymb}
+    \usepackage[safe]{tipa} % See page 12 of the tipa manual for what
+                            % safe does.
+
+    % FIX: This doesn't seem to help solve the pipe problem?
+    % http://tex.stackexchange.com/questions/1774/how-to-insert-pipe-symbol-in-latex
+    \usepackage[T1]{fontenc}
+    \usepackage[utf8x]{inputenc}
+
+    % FIX: Complete the list and send it upstream to the ucs package devs.
+    \DeclareUnicodeCharacter{9657}{$\triangleright$}
+    \DeclareUnicodeCharacter{8759}{::}
+    \DeclareUnicodeCharacter{8263}{$?\!?$}
+    \DeclareUnicodeCharacter{737} {$^l$}  % FIX: Ugly, apparently ^r is
+                                          % defined, I can't find the
+                                          % definition though.
+    \DeclareUnicodeCharacter{8718}{$\blacksquare$}
+    \DeclareUnicodeCharacter{8255}{$\_$} % FIX: Couldn't find \undertie.
+    \DeclareUnicodeCharacter{9667}{$\triangleleft$}
+    \DeclareUnicodeCharacter{10218}{$\langle\!\langle$}
+    \DeclareUnicodeCharacter{10219}{$\rangle\!\rangle$}
+\fi
+
+% ----------------------------------------------------------------------
+% Colour schemes.
+
+\newcommand{\AgdaColourScheme}{standard}
+
+\DeclareOption{bw}   {\renewcommand{\AgdaColourScheme}{bw}}
+\DeclareOption{conor}{\renewcommand{\AgdaColourScheme}{conor}}
+\ProcessOptions\relax
+
+% ----------------------------------------------------------------------
+% Font styles.
+
+% Default font style.
+\newcommand{\AgdaFontStyle}[1]{\textsf{#1}}
+
+% Keyword font style.
+\ifthenelse{\equal{\AgdaColourScheme}{bw}}{
+    \newcommand{\AgdaKeywordFontStyle}[1]{\underline{#1}}
+}{
+    \newcommand{\AgdaKeywordFontStyle}[1]{\textsf{#1}}
+}
+
+% String font style.
+\newcommand{\AgdaStringFontStyle}[1]{\texttt{#1}}
+
+% Comment font style.
+\newcommand{\AgdaCommentFontStyle}[1]{\texttt{#1}}
+
+% Bounded variables font style.
+\newcommand{\AgdaBoundFontStyle}[1]{\textit{#1}}
+
+% ----------------------------------------------------------------------
+% Colours.
+
+% ----------------------------------
+% The black and white colour scheme.
+\ifthenelse{\equal{\AgdaColourScheme}{bw}}{
+
+    % Aspect colours.
+    \definecolor{AgdaComment}      {HTML}{000000}
+    \definecolor{AgdaKeyword}      {HTML}{000000}
+    \definecolor{AgdaString}       {HTML}{000000}
+    \definecolor{AgdaNumber}       {HTML}{000000}
+    \definecolor{AgdaSymbol}       {HTML}{000000}
+    \definecolor{AgdaPrimitiveType}{HTML}{000000}
+    \definecolor{AgdaOperator}     {HTML}{000000}
+
+    % NameKind colours.
+    \definecolor{AgdaBound}                 {HTML}{000000}
+    \definecolor{AgdaInductiveConstructor}  {HTML}{000000}
+    \definecolor{AgdaCoinductiveConstructor}{HTML}{000000}
+    \definecolor{AgdaDatatype}              {HTML}{000000}
+    \definecolor{AgdaField}                 {HTML}{000000}
+    \definecolor{AgdaFunction}              {HTML}{000000}
+    \definecolor{AgdaModule}                {HTML}{000000}
+    \definecolor{AgdaPostulate}             {HTML}{000000}
+    \definecolor{AgdaPrimitive}             {HTML}{000000}
+    \definecolor{AgdaRecord}                {HTML}{000000}
+
+    % Other aspect colours.
+    \definecolor{AgdaDottedPattern}     {HTML}{000000}
+    \definecolor{AgdaUnsolvedMeta}      {HTML}{D3D3D3}
+    \definecolor{AgdaTerminationProblem}{HTML}{BEBEBE}
+    \definecolor{AgdaIncompletePattern} {HTML}{D3D3D3}
+    \definecolor{AgdaError}             {HTML}{696969}
+
+    % Misc.
+    \definecolor{AgdaHole}              {HTML}{BEBEBE}
+
+% ----------------------------------
+% Conor McBride's colour scheme.
+}{ \ifthenelse{\equal{\AgdaColourScheme}{conor}}{
+
+    % Aspect colours.
+    \definecolor{AgdaComment}      {HTML}{B22222}
+    \definecolor{AgdaKeyword}      {HTML}{000000}
+    \definecolor{AgdaString}       {HTML}{000000}
+    \definecolor{AgdaNumber}       {HTML}{000000}
+    \definecolor{AgdaSymbol}       {HTML}{000000}
+    \definecolor{AgdaPrimitiveType}{HTML}{0000CD}
+    \definecolor{AgdaOperator}     {HTML}{000000}
+
+    % NameKind colours.
+    \definecolor{AgdaBound}                 {HTML}{A020F0}
+    \definecolor{AgdaInductiveConstructor}  {HTML}{8B0000}
+    \definecolor{AgdaCoinductiveConstructor}{HTML}{8B0000}
+    \definecolor{AgdaDatatype}              {HTML}{0000CD}
+    \definecolor{AgdaField}                 {HTML}{8B0000}
+    \definecolor{AgdaFunction}              {HTML}{006400}
+    \definecolor{AgdaModule}                {HTML}{006400}
+    \definecolor{AgdaPostulate}             {HTML}{006400}
+    \definecolor{AgdaPrimitive}             {HTML}{006400}
+    \definecolor{AgdaRecord}                {HTML}{0000CD}
+
+    % Other aspect colours.
+    \definecolor{AgdaDottedPattern}     {HTML}{000000}
+    \definecolor{AgdaUnsolvedMeta}      {HTML}{FFD700}
+    \definecolor{AgdaTerminationProblem}{HTML}{FF0000}
+    \definecolor{AgdaIncompletePattern} {HTML}{A020F0}
+    \definecolor{AgdaError}             {HTML}{F4A460}
+
+    % Misc.
+    \definecolor{AgdaHole}              {HTML}{9DFF9D}
+
+% ----------------------------------
+% The standard colour scheme.
+}{
+    % Aspect colours.
+    \definecolor{AgdaComment}      {HTML}{B22222}
+    \definecolor{AgdaKeyword}      {HTML}{CD6600}
+    \definecolor{AgdaString}       {HTML}{B22222}
+    \definecolor{AgdaNumber}       {HTML}{A020F0}
+    \definecolor{AgdaSymbol}       {HTML}{404040}
+    \definecolor{AgdaPrimitiveType}{HTML}{0000CD}
+    \definecolor{AgdaOperator}     {HTML}{000000}
+
+    % NameKind colours.
+    \definecolor{AgdaBound}                 {HTML}{000000}
+    \definecolor{AgdaInductiveConstructor}  {HTML}{008B00}
+    \definecolor{AgdaCoinductiveConstructor}{HTML}{8B7500}
+    \definecolor{AgdaDatatype}              {HTML}{0000CD}
+    \definecolor{AgdaField}                 {HTML}{EE1289}
+    \definecolor{AgdaFunction}              {HTML}{0000CD}
+    \definecolor{AgdaModule}                {HTML}{A020F0}
+    \definecolor{AgdaPostulate}             {HTML}{0000CD}
+    \definecolor{AgdaPrimitive}             {HTML}{0000CD}
+    \definecolor{AgdaRecord}                {HTML}{0000CD}
+
+    % Other aspect colours.
+    \definecolor{AgdaDottedPattern}     {HTML}{000000}
+    \definecolor{AgdaUnsolvedMeta}      {HTML}{FFFF00}
+    \definecolor{AgdaTerminationProblem}{HTML}{FFA07A}
+    \definecolor{AgdaIncompletePattern} {HTML}{F5DEB3}
+    \definecolor{AgdaError}             {HTML}{FF0000}
+
+    % Misc.
+    \definecolor{AgdaHole}              {HTML}{9DFF9D}
+}}
+
+% ----------------------------------------------------------------------
+% Commands.
+
+% Aspect commands.
+\newcommand{\AgdaComment}     [1]
+    {\AgdaCommentFontStyle{\textcolor{AgdaComment}{#1}}}
+\newcommand{\AgdaKeyword}     [1]
+    {\AgdaKeywordFontStyle{\textcolor{AgdaKeyword}{#1}}}
+\newcommand{\AgdaString}      [1]{\AgdaStringFontStyle{\textcolor{AgdaString}{#1}}}
+\newcommand{\AgdaNumber}      [1]{\textcolor{AgdaNumber}{#1}}
+\newcommand{\AgdaSymbol}      [1]{\textcolor{AgdaSymbol}{#1}}
+\newcommand{\AgdaPrimitiveType}[1]
+    {\AgdaFontStyle{\textcolor{AgdaPrimitiveType}{#1}}}
+\newcommand{\AgdaOperator}    [1]{\textcolor{AgdaOperator}{#1}}
+
+% NameKind commands.
+\newcommand{\AgdaBound}    [1]{\AgdaBoundFontStyle{\textcolor{AgdaBound}{#1}}}
+\newcommand{\AgdaInductiveConstructor}[1]
+    {\AgdaFontStyle{\textcolor{AgdaInductiveConstructor}{#1}}}
+\newcommand{\AgdaCoinductiveConstructor}[1]
+    {\AgdaFontStyle{\textcolor{AgdaCoinductiveConstructor}{#1}}}
+\newcommand{\AgdaDatatype} [1]{\AgdaFontStyle{\textcolor{AgdaDatatype}{#1}}}
+\newcommand{\AgdaField}    [1]{\AgdaFontStyle{\textcolor{AgdaField}{#1}}}
+\newcommand{\AgdaFunction} [1]{\AgdaFontStyle{\textcolor{AgdaFunction}{#1}}}
+\newcommand{\AgdaModule}   [1]{\AgdaFontStyle{\textcolor{AgdaModule}{#1}}}
+\newcommand{\AgdaPostulate}[1]{\AgdaFontStyle{\textcolor{AgdaPostulate}{#1}}}
+\newcommand{\AgdaPrimitive}[1]{\AgdaFontStyle{\textcolor{AgdaPrimitive}{#1}}}
+\newcommand{\AgdaRecord}   [1]{\AgdaFontStyle{\textcolor{AgdaRecord}{#1}}}
+
+% Other aspect commands.
+\newcommand{\AgdaDottedPattern}     [1]{\textcolor{AgdaDottedPattern}{#1}}
+\newcommand{\AgdaUnsolvedMeta}      [1]
+    {\AgdaFontStyle{\colorbox{AgdaUnsolvedMeta}{#1}}}
+\newcommand{\AgdaTerminationProblem}[1]
+    {\AgdaFontStyle{\colorbox{AgdaTerminationProblem}{#1}}}
+\newcommand{\AgdaIncompletePattern} [1]{\colorbox{AgdaIncompletePattern}{#1}}
+\newcommand{\AgdaError}             [1]
+    {\AgdaFontStyle{\textcolor{AgdaError}{\underline{#1}}}}
+
+% Misc.
+\newcommand{\AgdaHole}[1]{\colorbox{AgdaHole}{#1}}
+\long\def\AgdaHide#1{} % Used to hide code from LaTeX.
+
+\newcommand{\AgdaIndent}[1]{\quad}
+
+% ----------------------------------------------------------------------
+% The code environment.
+
+\newcommand{\AgdaCodeStyle}{}
+% \newcommand{\AgdaCodeStyle}{\tiny}
+
+\ifdefined\mathindent
+  {}
+\else
+  \newdimen\mathindent\mathindent\leftmargini
+\fi
+
+\newenvironment{code}%
+{\noindent\ignorespaces\advance\leftskip\mathindent\AgdaCodeStyle\pboxed}%
+{\endpboxed\par\noindent%
+\ignorespacesafterend}
+
+% Default column for polytable.
+\defaultcolumn{l}