% ----------------------------------------------------------------------
% Some useful commands when doing highlighting of Agda code in LaTeX.
% ----------------------------------------------------------------------
\ProvidesPackage
\RequirePackage
% 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
\DeclareOption
\newif\if@AgdaEnableReferences\@AgdaEnableReferencesfalse
\DeclareOption
\newif\if@AgdaEnableLinks\@AgdaEnableLinksfalse
\DeclareOption
% If the "nofontsetup" option is used, then the package does not
% select any fonts, and it does not change the font encoding.
\newif\if@AgdaSetupFonts\@AgdaSetupFontstrue
\DeclareOption
% If the "noinputencodingsetup" option is used, then the package does
% not change the input encoding, and it does not load the `ucs`
% package.
\newif\if@AgdaSetupInputEncoding\@AgdaSetupInputEncodingtrue
\DeclareOption
\ProcessOptions\relax
% ----------------------------------------------------------------------
% Input encoding setup
\if@AgdaSetupInputEncoding
\ifxetexorluatex
\providecommand[2]
\else
\RequirePackage
\RequirePackage[utf8x]
\fi
\fi
% ----------------------------------------------------------------------
% Font setup
\tracinglostchars=2 % If the font is missing some symbol, then say
% so in the compilation output.
\if@AgdaSetupFonts
% XeLaTeX or LuaLaTeX
\ifxetexorluatex
% Hack to get the amsthm package working.
% https://tex.stackexchange.com/questions/130491/xelatex-error-paragraph-ended-before-tempa-was-complete
\let\AgdaOpenBracket\[\let\AgdaCloseBracket\]
\RequirePackage
\let\[\AgdaOpenBracket\let\]\AgdaCloseBracket
\RequirePackage
\setmainfont
[ Ligatures = TeX
, BoldItalicFont = xits-bolditalic.otf
, BoldFont = xits-bold.otf
, ItalicFont = xits-italic.otf
]
\setmathfont
\setmonofont[Mapping=tex-text]
% Make mathcal and mathscr appear as different.
% https://tex.stackexchange.com/questions/120065/xetex-what-happened-to-mathcal-and-mathscr
\setmathfont[range=,StylisticSet=1]
\setmathfont[range=\mathscr]
% pdfLaTeX
\else
% https://tex.stackexchange.com/questions/1774/how-to-insert-pipe-symbol-in-latex
\RequirePackage[T1]
\RequirePackage
\RequirePackage[safe] % See page 12 of the tipa manual for what
% safe does.
\fi
\fi
% ----------------------------------------------------------------------
% Colour schemes.
\providecommand
% ----------------------------------------------------------------------
% References to code (needs additional post-processing of tex files to
% work, see wiki for details).
\if@AgdaEnableReferences
\RequirePackage
\newcommand[2][]
\fi
\providecommand[2][]
% ----------------------------------------------------------------------
% Links (only done if the option is passed and the user has loaded the
% hyperref package).
\if@AgdaEnableLinks
\@ifpackageloaded
\fi
\providecommand[1]
\providecommand[1]
% ----------------------------------------------------------------------
% Font styles.
\ifxetexorluatex
\newcommand[1]
\ifthenelse
\newcommand[1]
\newcommand[1]
\newcommand[1]
\else
\newcommand[1]
\ifthenelse
\newcommand[1]
\newcommand[1]
\newcommand[1]
\fi
% ----------------------------------------------------------------------
% Colours.
% ----------------------------------
% The black and white colour scheme.
\ifthenelse
% ----------------------------------------------------------------------
% Commands.
\newcommand[1]
% Aspect commands.
\newcommand [1]
\newcommand [1]
\newcommand [1]
\newcommand [1]
\newcommand [1]
\newcommand [1]
\newcommand[1]
% Note that, in code generated by the LaTeX backend, \AgdaOperator is
% always applied to a NameKind command.
\newcommand [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[2]
\newcommand[1]
\newcommand[1]
\newcommand[1]
\newcommand[1]
\newcommand[1]
\newcommand[1]
\newcommand[1]
\newcommand[1]
\newcommand[1]
\newcommand[1]
\newcommand[1]
\newcommand[1]
% Other aspect commands.
\newcommand [1]
\newcommand [1]
\newcommand [1]
\newcommand[1]
\newcommand [1]
\newcommand [1]
\newcommand [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
% Misc.
\newcommand[1]
% ----------------------------------------------------------------------
% The code environment.
\newcommand
% \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[1]
% Should there be space around code?
\newboolean
% Use this command to avoid extra space around code blocks.
\newcommand
% Use this command to include extra space around code blocks.
\newcommand
% 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
\setcounter
% The number of the previous code block (excluding hidden ones), used
% locally in \Agda@SuppressEnd.
\newcounter
% Is AgdaAlign active?
\newboolean
\setboolean
% The number of the first code block (if any) in a given AgdaAlign
% environment.
\newcounter
\newcommand
\newcommand
\newenvironment
% Is AgdaSuppressSpace active?
\newboolean
\setboolean
% The number of the first code block (if any) in a given
% AgdaSuppressSpace environment.
\newcounter
% 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
\newcommand
% Marks the given code block as one that space should not be
% suppressed after (if AgdaSpaceAroundCode and AgdaSuppressSpace are
% both active).
\newcommand[1]
\newcommand
\newenvironment
\newenvironment
% Vertical space used for empty lines. By default \baselineskip.
\newlength
\setlength
% Extra space to be inserted for empty lines (the difference between
% \AgdaEmptySkip and \baselineskip). Used internally.
\newlength
% The code environment.
%
% Code can be hidden by writing \begin{code}[hide].
%
% The implementation is based on plainhscode in lhs2TeX's
% polycode.fmt, written by Andres Löh.
\NewEnviron[1][]
% Space inserted after tokens.
\newcommand
% Space inserted to indent something.
\newcommand
% Default column for polytable.
\defaultcolumn
% \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[1]
% Underscores are typeset using \AgdaUnderscore{}.
\newcommand
\endinput