% ----------------------------------------------------------------------
% Some useful commands when doing highlightning of Agda code in LaTeX.
% ----------------------------------------------------------------------

\ProvidesPackage{agda}

\usepackage{ifxetex, xcolor, polytable}

% 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

% ----------------------------------------------------------------------
% Font styles.

% Default font style.
\newcommand{\AgdaFontStyle}[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.

% 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]
    {\AgdaFontStyle{\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}