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

\ProvidesPackage{agda}

\RequirePackage{ifxetex, ifluatex, ifthen, xcolor, polytable, etoolbox}

% http://tex.stackexchange.com/questions/47576/combining-ifxetex-and-ifluatex-with-the-logical-or-operation
\newif\ifxetexorluatex
\ifxetex
  \xetexorluatextrue
\else
  \ifluatex
    \xetexorluatextrue
  \else
    \xetexorluatexfalse
  \fi
\fi

% XeLaTeX or LuaLaTeX
\ifxetexorluatex

    % Hack to get the amsthm package working.
    % http://tex.stackexchange.com/questions/130491/xelatex-error-paragraph-ended-before-tempa-was-complete
    \let\AgdaOpenBracket\[\let\AgdaCloseBracket\]
    \RequirePackage{fontspec}
    \let\[\AgdaOpenBracket\let\]\AgdaCloseBracket
    \RequirePackage{unicode-math}

    \tracinglostchars=2 % If the font is missing some symbol, then say
                        % so in the compilation output.
    \setmainfont[Ligatures=TeX]{texgyrepagella-regular.otf}
    \setmathfont{Asana-Math.otf}

    \providecommand{\DeclareUnicodeCharacter}[2]{\relax}

% pdfLaTeX
\else
    \RequirePackage{ucs, amsfonts, amssymb}
    \RequirePackage[safe]{tipa} % See page 12 of the tipa manual for what
                                % safe does.

    % http://tex.stackexchange.com/questions/1774/how-to-insert-pipe-symbol-in-latex
    \RequirePackage[T1]{fontenc}
    \RequirePackage[utf8x]{inputenc}
\fi

% ----------------------------------------------------------------------
% Colour schemes.

\newcommand{\AgdaColourScheme}{standard}

\DeclareOption{bw}   {\renewcommand{\AgdaColourScheme}{bw}}
\DeclareOption{conor}{\renewcommand{\AgdaColourScheme}{conor}}

% ----------------------------------------------------------------------
% Links (only done if the option is passed and the user has loaded the
% hyperref package).

\newif\if@AgdaEnableLinks\@AgdaEnableLinksfalse
\DeclareOption{links}{
    \@AgdaEnableLinkstrue
}
\ProcessOptions\relax

\if@AgdaEnableLinks
  \@ifpackageloaded{hyperref}{

    % List that holds added targets.
    \newcommand{\AgdaList}[0]{}

    \newtoggle{AgdaIsElem}
    \newcounter{AgdaIndex}
    \newcommand{\AgdaLookup}[3]{%
      \togglefalse{AgdaIsElem}%
      \setcounter{AgdaIndex}{0}%
      \renewcommand*{\do}[1]{%
      \ifstrequal{#1}{##1}%
        {\toggletrue{AgdaIsElem}\listbreak}%
        {\stepcounter{AgdaIndex}}}%
      \dolistloop{\AgdaList}%
      \iftoggle{AgdaIsElem}{#2}{#3}%
    }

    \newcommand*{\AgdaTargetHelper}[1]{%
      \AgdaLookup{#1}%
        {\PackageError{agda}{``#1'' used as target more than once}%
                            {Overloaded identifiers and links do not%
                             work well, consider using unique%
                             \MessageBreak identifiers instead.}%
        }%
        {\listadd{\AgdaList}{#1}%
         \hypertarget{Agda\theAgdaIndex}{}%
        }%
    }

    \newcommand{\AgdaTarget}[1]{\forcsvlist{\AgdaTargetHelper}{#1}}

    \newcommand{\AgdaLink}[1]{%
      \AgdaLookup{#1}%
        {\hyperlink{Agda\theAgdaIndex}{#1}}%
        {#1}%
    }
  }{\PackageError{agda}{Load the hyperref package before the agda package}{}}
\fi

\providecommand{\AgdaTarget}[1]{}
\providecommand{\AgdaLink}[1]{#1}

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

\ifxetexorluatex
  \newcommand{\AgdaFontStyle}[1]{\ensuremath{\mathsf{#1}}}
  \ifthenelse{\equal{\AgdaColourScheme}{bw}}{
      \newcommand{\AgdaKeywordFontStyle}[1]{\underline{#1}}
  }{
      \newcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathsf{#1}}}
  }
  \newcommand{\AgdaStringFontStyle}[1]{\ensuremath{\mathtt{#1}}}
  \newcommand{\AgdaCommentFontStyle}[1]{\ensuremath{\mathtt{#1}}}
  \newcommand{\AgdaBoundFontStyle}[1]{\ensuremath{\mathit{#1}}}

\else
  \newcommand{\AgdaFontStyle}[1]{\textsf{#1}}
  \ifthenelse{\equal{\AgdaColourScheme}{bw}}{
      \newcommand{\AgdaKeywordFontStyle}[1]{\underline{#1}}
  }{
      \newcommand{\AgdaKeywordFontStyle}[1]{\textsf{#1}}
  }
  \newcommand{\AgdaStringFontStyle}[1]{\texttt{#1}}
  \newcommand{\AgdaCommentFontStyle}[1]{\texttt{#1}}
  \newcommand{\AgdaBoundFontStyle}[1]{\textit{#1}}
\fi

% ----------------------------------------------------------------------
% 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}
    \definecolor{AgdaArgument}              {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}
    \definecolor{AgdaArgument}              {HTML}{404040}

    % 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}
    \definecolor{AgdaArgument}              {HTML}{404040}

    % 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]{\AgdaFontStyle{\textcolor{AgdaNumber}{#1}}}
\newcommand{\AgdaSymbol}      [1]{\AgdaFontStyle{\textcolor{AgdaSymbol}{#1}}}
\newcommand{\AgdaPrimitiveType}[1]
    {\AgdaFontStyle{\textcolor{AgdaPrimitiveType}{#1}}}
\newcommand{\AgdaOperator}    [1]{\AgdaFontStyle{\textcolor{AgdaOperator}{#1}}}

% NameKind commands.
\newcommand{\AgdaBound}[1]
    {\AgdaBoundFontStyle{\textcolor{AgdaBound}{#1}}}
\newcommand{\AgdaInductiveConstructor}[1]
    {\AgdaFontStyle{\textcolor{AgdaInductiveConstructor}{\AgdaLink{#1}}}}
\newcommand{\AgdaCoinductiveConstructor}[1]
    {\AgdaFontStyle{\textcolor{AgdaCoinductiveConstructor}{\AgdaLink{#1}}}}
\newcommand{\AgdaDatatype}[1]
    {\AgdaFontStyle{\textcolor{AgdaDatatype}{\AgdaLink{#1}}}}
\newcommand{\AgdaField}[1]
    {\AgdaFontStyle{\textcolor{AgdaField}{\AgdaLink{#1}}}}
\newcommand{\AgdaFunction}[1]
    {\AgdaFontStyle{\textcolor{AgdaFunction}{\AgdaLink{#1}}}}
\newcommand{\AgdaModule}[1]
    {\AgdaFontStyle{\textcolor{AgdaModule}{\AgdaLink{#1}}}}
\newcommand{\AgdaPostulate}[1]
    {\AgdaFontStyle{\textcolor{AgdaPostulate}{\AgdaLink{#1}}}}
\newcommand{\AgdaPrimitive}[1]
    {\AgdaFontStyle{\textcolor{AgdaPrimitive}{#1}}}
\newcommand{\AgdaRecord}[1]
    {\AgdaFontStyle{\textcolor{AgdaRecord}{\AgdaLink{#1}}}}
\newcommand{\AgdaArgument}[1]
    {\AgdaFontStyle{\textcolor{AgdaArgument}{\AgdaLink{#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]{$\;\;$}

% ----------------------------------------------------------------------
% 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@{~}}

\endinput