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

\ProvidesPackage{agda}

\RequirePackage{ifxetex, ifluatex, xifthen, xcolor, polytable, etoolbox,
                calc, environ, xparse}

% https://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

% ----------------------------------------------------------------------
% Options

\DeclareOption{bw}   {\newcommand{\AgdaColourScheme}{bw}}
\DeclareOption{conor}{\newcommand{\AgdaColourScheme}{conor}}

\newif\if@AgdaEnableReferences\@AgdaEnableReferencesfalse
\DeclareOption{references}{
  \@AgdaEnableReferencestrue
}

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

\ProcessOptions\relax

% ----------------------------------------------------------------------
% Font setup

\tracinglostchars=2 % If the font is missing some symbol, then say
                    % so in the compilation output.

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

\providecommand{\AgdaColourScheme}{standard}

% ----------------------------------------------------------------------
% References to code (needs additional post-processing of tex files to
% work, see wiki for details).

\if@AgdaEnableReferences
  \RequirePackage{catchfilebetweentags, xstring}
  \newcommand{\AgdaRef}[2][]{%
    \StrSubstitute{#2}{\_}{AgdaUnderscore}[\tmp]%
    \ifthenelse{\isempty{#1}}%
               {\ExecuteMetaData{AgdaTag-\tmp}}%
               {\ExecuteMetaData{#1}{AgdaTag-\tmp}}
  }
\fi

\providecommand{\AgdaRef}[2][]{#2}

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

\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.

\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}}

% ----------------------------------------------------------------------
% Colours.

% ----------------------------------
% The black and white colour scheme.
\ifthenelse{\equal{\AgdaColourScheme}{bw}}{

    % Aspect colours.
    \definecolor{AgdaComment}      {HTML}{000000}
    \definecolor{AgdaPragma}       {HTML}{000000}
    \definecolor{AgdaKeyword}      {HTML}{000000}
    \definecolor{AgdaString}       {HTML}{000000}
    \definecolor{AgdaNumber}       {HTML}{000000}
    \definecolor{AgdaSymbol}       {HTML}{000000}
    \definecolor{AgdaPrimitiveType}{HTML}{000000}

    % NameKind colours.
    \definecolor{AgdaBound}                 {HTML}{000000}
    \definecolor{AgdaGeneralizable}         {HTML}{000000}
    \definecolor{AgdaInductiveConstructor}  {HTML}{000000}
    \definecolor{AgdaCoinductiveConstructor}{HTML}{000000}
    \definecolor{AgdaDatatype}              {HTML}{000000}
    \definecolor{AgdaField}                 {HTML}{000000}
    \definecolor{AgdaFunction}              {HTML}{000000}
    \definecolor{AgdaMacro}                 {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{AgdaPragma}       {HTML}{000000}
    \definecolor{AgdaKeyword}      {HTML}{000000}
    \definecolor{AgdaString}       {HTML}{000000}
    \definecolor{AgdaNumber}       {HTML}{000000}
    \definecolor{AgdaSymbol}       {HTML}{000000}
    \definecolor{AgdaPrimitiveType}{HTML}{0000CD}

    % NameKind colours.
    \definecolor{AgdaBound}                 {HTML}{A020F0}
    \definecolor{AgdaGeneralizable}         {HTML}{A020F0}
    \definecolor{AgdaInductiveConstructor}  {HTML}{8B0000}
    \definecolor{AgdaCoinductiveConstructor}{HTML}{8B0000}
    \definecolor{AgdaDatatype}              {HTML}{0000CD}
    \definecolor{AgdaField}                 {HTML}{8B0000}
    \definecolor{AgdaFunction}              {HTML}{006400}
    \definecolor{AgdaMacro}                 {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{AgdaPragma}       {HTML}{000000}
    \definecolor{AgdaKeyword}      {HTML}{CD6600}
    \definecolor{AgdaString}       {HTML}{B22222}
    \definecolor{AgdaNumber}       {HTML}{A020F0}
    \definecolor{AgdaSymbol}       {HTML}{404040}
    \definecolor{AgdaPrimitiveType}{HTML}{0000CD}

    % NameKind colours.
    \definecolor{AgdaBound}                 {HTML}{000000}
    \definecolor{AgdaGeneralizable}         {HTML}{000000}
    \definecolor{AgdaInductiveConstructor}  {HTML}{008B00}
    \definecolor{AgdaCoinductiveConstructor}{HTML}{8B7500}
    \definecolor{AgdaDatatype}              {HTML}{0000CD}
    \definecolor{AgdaField}                 {HTML}{EE1289}
    \definecolor{AgdaFunction}              {HTML}{0000CD}
    \definecolor{AgdaMacro}                 {HTML}{458B74}
    \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.

\newcommand{\AgdaNoSpaceMath}[1]
    {\begingroup\thickmuskip=0mu\medmuskip=0mu#1\endgroup}

% Aspect commands.
\newcommand{\AgdaComment}     [1]
    {\AgdaNoSpaceMath{\AgdaCommentFontStyle{\textcolor{AgdaComment}{#1}}}}
\newcommand{\AgdaPragma}      [1]
    {\AgdaNoSpaceMath{\AgdaCommentFontStyle{\textcolor{AgdaPragma}{#1}}}}
\newcommand{\AgdaKeyword}     [1]
    {\AgdaNoSpaceMath{\AgdaKeywordFontStyle{\textcolor{AgdaKeyword}{#1}}}}
\newcommand{\AgdaString}      [1]
    {\AgdaNoSpaceMath{\AgdaStringFontStyle{\textcolor{AgdaString}{#1}}}}
\newcommand{\AgdaNumber}      [1]
    {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaNumber}{#1}}}}
\newcommand{\AgdaSymbol}      [1]
    {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaSymbol}{#1}}}}
\newcommand{\AgdaPrimitiveType}[1]
    {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaPrimitiveType}{#1}}}}
% Note that, in code generated by the LaTeX backend, \AgdaOperator is
% always applied to a NameKind command.
\newcommand{\AgdaOperator}    [1]{#1}

% NameKind commands.

% The user can control the typesetting of (certain) individual tokens
% by redefining the following command. The first argument is the token
% and the second argument the thing to be typeset (sometimes just the
% token, sometimes \AgdaLink{<the token>}). Example:
%
%   \usepackage{ifthen}
%
%   % Insert extra space before some tokens.
%   \DeclareRobustCommand{\AgdaFormat}[2]{%
%     \ifthenelse{
%       \equal{#1}{≡⟨} \OR
%       \equal{#1}{≡⟨⟩} \OR
%       \equal{#1}{∎}
%     }{\ }{}#2}
%
% Note the use of \DeclareRobustCommand.

\newcommand{\AgdaFormat}[2]{#2}

\newcommand{\AgdaBound}[1]
    {\AgdaNoSpaceMath{\AgdaBoundFontStyle{\textcolor{AgdaBound}{\AgdaFormat{#1}{#1}}}}}
\newcommand{\AgdaGeneralizable}[1]
    {\AgdaNoSpaceMath{\AgdaBoundFontStyle{\textcolor{AgdaGeneralizable}{\AgdaFormat{#1}{#1}}}}}
\newcommand{\AgdaInductiveConstructor}[1]
    {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaInductiveConstructor}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
\newcommand{\AgdaCoinductiveConstructor}[1]
    {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaCoinductiveConstructor}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
\newcommand{\AgdaDatatype}[1]
    {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaDatatype}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
\newcommand{\AgdaField}[1]
    {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaField}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
\newcommand{\AgdaFunction}[1]
    {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaFunction}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
\newcommand{\AgdaMacro}[1]
    {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaMacro}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
\newcommand{\AgdaModule}[1]
    {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaModule}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
\newcommand{\AgdaPostulate}[1]
    {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaPostulate}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
\newcommand{\AgdaPrimitive}[1]
    {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaPrimitive}{\AgdaFormat{#1}{#1}}}}}
\newcommand{\AgdaRecord}[1]
    {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaRecord}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
\newcommand{\AgdaArgument}[1]
    {\AgdaNoSpaceMath{\AgdaBoundFontStyle{\textcolor{AgdaArgument}{\AgdaFormat{#1}{#1}}}}}

% Other aspect commands.
\newcommand{\AgdaFixityOp}          [1]{\AgdaNoSpaceMath{$#1$}}
\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}}}}
\newcommand{\AgdaCatchallClause}    [1]{#1} % feel free to change this

% Used to hide code from LaTeX.
%
% Note that this macro has been deprecated in favour of giving the
% hide argument to the code environment.
\long\def\AgdaHide#1{\ignorespaces}

% Misc.
\newcommand{\AgdaHole}[1]{\colorbox{AgdaHole}{#1}}

% ----------------------------------------------------------------------
% The code environment.

\newcommand{\AgdaCodeStyle}{}
% \newcommand{\AgdaCodeStyle}{\tiny}

\ifdefined\mathindent
  {}
\else
  \newdimen\mathindent\mathindent\leftmargini
\fi

% Adds the given amount of vertical space and starts a new line.
%
% The implementation comes from lhs2TeX's polycode.fmt, written by
% Andres Löh.
\newcommand{\Agda@NewlineWithVerticalSpace}[1]{%
  {\parskip=0pt\parindent=0pt\par\vskip #1\noindent}}

% Should there be space around code?
\newboolean{Agda@SpaceAroundCode}

% Use this command to avoid extra space around code blocks.
\newcommand{\AgdaNoSpaceAroundCode}{%
  \setboolean{Agda@SpaceAroundCode}{false}}

% Use this command to include extra space around code blocks.
\newcommand{\AgdaSpaceAroundCode}{%
  \setboolean{Agda@SpaceAroundCode}{true}}

% By default space is inserted around code blocks.
\AgdaSpaceAroundCode{}

% Sometimes one might want to break up a code block into multiple
% pieces, but keep code in different blocks aligned with respect to
% each other. Then one can use the AgdaAlign environment. Example
% usage:
%
%   \begin{AgdaAlign}
%   \begin{code}
%     code
%       code  (more code)
%   \end{code}
%   Explanation...
%   \begin{code}
%     aligned with "code"
%       code  (aligned with (more code))
%   \end{code}
%   \end{AgdaAlign}
%
% Note that AgdaAlign environments should not be nested.
%
% Sometimes one might also want to hide code in the middle of a code
% block. This can be accomplished in the following way:
%
%   \begin{AgdaAlign}
%   \begin{code}
%     visible
%   \end{code}
%   \begin{code}[hide]
%     hidden
%   \end{code}
%   \begin{code}
%     visible
%   \end{code}
%   \end{AgdaAlign}
%
% However, the result may be ugly: extra space is perhaps inserted
% around the code blocks.
%
% The AgdaSuppressSpace environment ensures that extra space is only
% inserted before the first code block, and after the last one (but
% not if \AgdaNoSpaceAroundCode{} is used). Example usage:
%
%   \begin{AgdaAlign}
%   \begin{code}
%     code
%       more code
%   \end{code}
%   Explanation...
%   \begin{AgdaSuppressSpace}
%   \begin{code}
%     aligned with "code"
%       aligned with "more code"
%   \end{code}
%   \begin{code}[hide]
%     hidden code
%   \end{code}
%   \begin{code}
%       also aligned with "more code"
%   \end{code}
%   \end{AgdaSuppressSpace}
%   \end{AgdaAlign}
%
% Note that AgdaSuppressSpace environments should not be nested.
%
% There is also a combined environment, AgdaMultiCode, that combines
% the effects of AgdaAlign and AgdaSuppressSpace.

% The number of the current/next code block (excluding hidden ones).
\newcounter{Agda@Current}
\setcounter{Agda@Current}{0}

% The number of the previous code block (excluding hidden ones), used
% locally in \Agda@SuppressEnd.
\newcounter{Agda@Previous}

% Is AgdaAlign active?
\newboolean{Agda@Align}
\setboolean{Agda@Align}{false}

% The number of the first code block (if any) in a given AgdaAlign
% environment.
\newcounter{Agda@AlignStart}

\newcommand{\Agda@AlignStart}{%
  \ifthenelse{\boolean{Agda@Align}}{%
    \PackageError{agda}{Nested AgdaAlign environments}{%
      AgdaAlign and AgdaMultiCode environments must not be
      nested.}}{%
    \setboolean{Agda@Align}{true}%
    \setcounter{Agda@AlignStart}{\value{Agda@Current}}}}

\newcommand{\Agda@AlignEnd}{\setboolean{Agda@Align}{false}}

\newenvironment{AgdaAlign}{%
  \Agda@AlignStart{}}{%
  \Agda@AlignEnd{}%
  \ignorespacesafterend}

% Is AgdaSuppressSpace active?
\newboolean{Agda@Suppress}
\setboolean{Agda@Suppress}{false}

% The number of the first code block (if any) in a given
% AgdaSuppressSpace environment.
\newcounter{Agda@SuppressStart}

% Does a "do not suppress space after" label exist for the current
% code block? (This boolean is used locally in the code environment's
% implementation.)
\newboolean{Agda@DoNotSuppressSpaceAfter}

\newcommand{\Agda@SuppressStart}{%
  \ifthenelse{\boolean{Agda@Suppress}}{%
    \PackageError{agda}{Nested AgdaSuppressSpace environments}{%
      AgdaSuppressSpace and AgdaMultiCode environments must not be
      nested.}}{%
    \setboolean{Agda@Suppress}{true}%
    \setcounter{Agda@SuppressStart}{\value{Agda@Current}}}}

% Marks the given code block as one that space should not be
% suppressed after (if AgdaSpaceAroundCode and AgdaSuppressSpace are
% both active).
\newcommand{\Agda@DoNotSuppressSpaceAfter}[1]{%
  % The use of labels is intended to ensure that LaTeX will provide a
  % warning if the document needs to be recompiled.
  \label{Agda@DoNotSuppressSpaceAfter@#1}}

\newcommand{\Agda@SuppressEnd}{%
  \ifthenelse{\value{Agda@SuppressStart} = \value{Agda@Current}}{}{%
    % Mark the previous code block in the .aux file.
    \setcounter{Agda@Previous}{\theAgda@Current-1}%
    \immediate\write\@auxout{%
      \noexpand\Agda@DoNotSuppressSpaceAfter{\theAgda@Previous}}}%
  \setboolean{Agda@Suppress}{false}}

\newenvironment{AgdaSuppressSpace}{%
  \Agda@SuppressStart{}}{%
  \Agda@SuppressEnd{}%
  \ignorespacesafterend}

\newenvironment{AgdaMultiCode}{%
  \Agda@AlignStart{}%
  \Agda@SuppressStart{}}{%
  \Agda@SuppressEnd{}%
  \Agda@AlignEnd{}%
  \ignorespacesafterend}

% Vertical space used for empty lines. By default \abovedisplayskip.
\newlength{\AgdaEmptySkip}
\setlength{\AgdaEmptySkip}{\abovedisplayskip}

% Extra space to be inserted for empty lines (the difference between
% \AgdaEmptySkip and \baselineskip). Used internally.
\newlength{\AgdaEmptyExtraSkip}

% The code environment.
%
% Code can be hidden by writing \begin{code}[hide].
%
% Inline code can be emitted by writing \begin{code}[inline]. In this
% case most of the discussion above does not apply, alignment is not
% respected, and so on. It is recommended to only use this option for
% a single line of code, and to not use two consecutive spaces in this
% piece of code.
%
% Note that this environment ignores spaces after its end. If a space
% (\AgdaSpace{}) should be inserted after the inline code, use inline*
% instead of inline.
%
% The implementation is based on plainhscode in lhs2TeX's
% polycode.fmt, written by Andres Löh.
\NewEnviron{code}[1][]{%
  % Conditionally hide the code.
  \ifthenelse{\equal{#1}{hide}}{}{%
  \ifthenelse{\equal{#1}{inline}}{%
    % Inline code.
    %
    % Make the polytable primitives emitted by the LaTeX backend
    % do nothing.
    \DeclareDocumentCommand{\>}{O{}O{}}{}%
    \DeclareDocumentCommand{\<}{O{}}{}%
    \AgdaCodeStyle\BODY}{%
  \ifthenelse{\equal{#1}{inline*}}{%
    % Inline code with space at the end.
    %
    \DeclareDocumentCommand{\>}{O{}O{}}{}%
    \DeclareDocumentCommand{\<}{O{}}{}%
    \AgdaCodeStyle\BODY\AgdaSpace{}}{%
    %
    % Displayed code.
    %
    % Conditionally emit space before the code block. Unconditionally
    % switch to a new line.
    \ifthenelse{\boolean{Agda@SpaceAroundCode} \and%
                \(\not \boolean{Agda@Suppress} \or%
                  \value{Agda@SuppressStart} = \value{Agda@Current}\)}{%
      \Agda@NewlineWithVerticalSpace{\abovedisplayskip}}{%
      \Agda@NewlineWithVerticalSpace{0pt}}%
    %
    % Indent the entire code block.
    \advance\leftskip\mathindent%
    %
    % The code's style can be customised.
    \AgdaCodeStyle%
    %
    % Used to control the height of empty lines.
    \setlength{\AgdaEmptyExtraSkip}{\AgdaEmptySkip - \baselineskip}%
    %
    % The environment used to handle indentation (of individual lines)
    % and alignment.
    \begin{pboxed}%
      %
      % Conditionally preserve alignment between code blocks.
      \ifthenelse{\boolean{Agda@Align}}{%
        \ifthenelse{\value{Agda@AlignStart} = \value{Agda@Current}}{%
          \savecolumns}{%
          \restorecolumns}}{}%
      %
      % The code.
      \BODY%
    \end{pboxed}%
    %
    % Does the label Agda@DoNotSuppressAfter@<current code block
    % number> exist?
    \ifcsdef{r@Agda@DoNotSuppressSpaceAfter@\theAgda@Current}{%
      \setboolean{Agda@DoNotSuppressSpaceAfter}{true}}{%
      \setboolean{Agda@DoNotSuppressSpaceAfter}{false}}%
    %
    % Conditionally emit space after the code block. Unconditionally
    % switch to a new line.
    \ifthenelse{\boolean{Agda@SpaceAroundCode} \and%
                \(\not \boolean{Agda@Suppress} \or%
                  \boolean{Agda@DoNotSuppressSpaceAfter}\)}{%
      \Agda@NewlineWithVerticalSpace{\belowdisplayskip}}{%
      \Agda@NewlineWithVerticalSpace{0pt}}%
    %
    % Step the code block counter, but only for non-hidden code.
    \stepcounter{Agda@Current}}}}}

% Space inserted after tokens.
\newcommand{\AgdaSpace}{ }

% Space inserted to indent something.
\newcommand{\AgdaIndentSpace}{\AgdaSpace{}$\;\;$}

% Default column for polytable.
\defaultcolumn{@{}l@{\AgdaSpace{}}}

% \AgdaIndent expects a non-negative integer as its only argument.
% This integer should be the distance, in code blocks, to the thing
% relative to which the text is indented.
%
% The default implementation only indents if the thing that the text
% is indented relative to exists in the same code block or is wrapped
% in the same AgdaAlign or AgdaMultiCode environment.
\newcommand{\AgdaIndent}[1]{%
  \ifthenelse{#1 = 0
                \or
              \( \boolean{Agda@Align}
                   \and
                 \cnttest{\value{Agda@Current} - #1}{>=}{
                          \value{Agda@AlignStart}}
              \)}{\AgdaIndentSpace{}}{}}

% Underscores are typeset using \AgdaUnderscore{}.
\newcommand{\AgdaUnderscore}{\_}

\endinput