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

\ProvidesPackage{agda}

\usepackage{ifxetex, 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}
