Agda-2.5.2: src/data/agda.sty
% ----------------------------------------------------------------------
% Some useful commands when doing highlighting of Agda code in LaTeX.
% ----------------------------------------------------------------------
\ProvidesPackage{agda}
\RequirePackage{ifxetex, ifluatex, xifthen, xcolor, polytable, etoolbox}
% 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
% 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{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
, BoldItalicFont = xits-bolditalic.otf
, BoldFont = xits-bold.otf
, ItalicFont = xits-italic.otf
]
{xits-regular.otf}
\setmathfont{xits-math.otf}
\setmonofont[Mapping=tex-text]{FreeMono.otf}
% Make mathcal and mathscr appear as different.
% https://tex.stackexchange.com/questions/120065/xetex-what-happened-to-mathcal-and-mathscr
\setmathfont[range={\mathcal,\mathbfcal},StylisticSet=1]{xits-math.otf}
\setmathfont[range=\mathscr]{xits-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.
% https://tex.stackexchange.com/questions/1774/how-to-insert-pipe-symbol-in-latex
\RequirePackage[T1]{fontenc}
\RequirePackage[utf8x]{inputenc}
\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
% ----------------------------------------------------------------------
% 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.
\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{\texttt{#1}}}
\newcommand{\AgdaCommentFontStyle}[1]{\ensuremath{\texttt{#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{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{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{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{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{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.
% 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{\AgdaNoSpaceMath}[1]
{\begingroup\thickmuskip=0mu\medmuskip=0mu#1\endgroup}
\newcommand{\AgdaBound}[1]
{\AgdaNoSpaceMath{\AgdaBoundFontStyle{\textcolor{AgdaBound}{#1}}}}
\newcommand{\AgdaInductiveConstructor}[1]
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaInductiveConstructor}{\AgdaLink{#1}}}}}
\newcommand{\AgdaCoinductiveConstructor}[1]
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaCoinductiveConstructor}{\AgdaLink{#1}}}}}
\newcommand{\AgdaDatatype}[1]
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaDatatype}{\AgdaLink{#1}}}}}
\newcommand{\AgdaField}[1]
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaField}{\AgdaLink{#1}}}}}
\newcommand{\AgdaFunction}[1]
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaFunction}{\AgdaLink{#1}}}}}
\newcommand{\AgdaMacro}[1]
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaMacro}{\AgdaLink{#1}}}}}
\newcommand{\AgdaModule}[1]
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaModule}{\AgdaLink{#1}}}}}
\newcommand{\AgdaPostulate}[1]
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaPostulate}{\AgdaLink{#1}}}}}
\newcommand{\AgdaPrimitive}[1]
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaPrimitive}{#1}}}}
\newcommand{\AgdaRecord}[1]
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaRecord}{\AgdaLink{#1}}}}}
\newcommand{\AgdaArgument}[1]
{\AgdaNoSpaceMath{\AgdaBoundFontStyle{\textcolor{AgdaArgument}{#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}}}}
% Misc.
\newcommand{\AgdaHole}[1]{\colorbox{AgdaHole}{#1}}
\long\def\AgdaHide#1{\ignorespaces} % 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
% 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{\AgdaNewlineWithVerticalSpace}[1]{%
{\parskip=0pt\parindent=0pt\par\vskip #1\noindent}}
% 0: No space around code. 1: Space around code.
\newcounter{Agda@SpaceAroundCode}
% Use this command to avoid extra space around code blocks.
\newcommand{\AgdaNoSpaceAroundCode}{%
\setcounter{Agda@SpaceAroundCode}{0}}
% Use this command to include extra space around code blocks.
\newcommand{\AgdaSpaceAroundCode}{%
\setcounter{Agda@SpaceAroundCode}{1}}
% 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}
% \AgdaHide{
% \begin{code}
% 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).
%
% The environment takes one argument, the number of wrapped code
% blocks (excluding hidden ones). Example usage:
%
% \begin{AgdaAlign}
% \begin{code}
% code
% more code
% \end{code}
% Explanation...
% \begin{AgdaSuppressSpace}{2}
% \begin{code}
% aligned with "code"
% aligned with "more code"
% \end{code}
% \AgdaHide{
% \begin{code}
% 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.
% 0: AgdaAlign is not active. 1: AgdaAlign is active.
\newcounter{Agda@Align}
\setcounter{Agda@Align}{0}
% The current code block.
\newcounter{Agda@AlignCurrent}
\newcommand{\Agda@AlignStart}{%
\setcounter{Agda@Align}{1}%
\setcounter{Agda@AlignCurrent}{1}}
\newcommand{\Agda@AlignEnd}{\setcounter{Agda@Align}{0}}
\newenvironment{AgdaAlign}{%
\Agda@AlignStart{}}{%
\Agda@AlignEnd{}%
\ignorespacesafterend}
% 0: AgdaSuppressSpace is not active. 1: AgdaSuppressSpace is active.
\newcounter{Agda@Suppress}
\setcounter{Agda@Suppress}{0}
% The current code block.
\newcounter{Agda@SuppressCurrent}
% The expected number of code blocks.
\newcounter{Agda@SuppressLast}
\newcommand{\Agda@SuppressStart}[1]{%
\setcounter{Agda@Suppress}{1}%
\setcounter{Agda@SuppressLast}{#1}%
\setcounter{Agda@SuppressCurrent}{1}}
\newcommand{\Agda@SuppressEnd}{\setcounter{Agda@Suppress}{0}}
\newenvironment{AgdaSuppressSpace}[1]{%
\Agda@SuppressStart{#1}}{%
\Agda@SuppressEnd{}%
\ignorespacesafterend}
\newenvironment{AgdaMultiCode}[1]{%
\Agda@AlignStart{}%
\Agda@SuppressStart{#1}}{%
\Agda@SuppressEnd{}%
\Agda@AlignEnd{}%
\ignorespacesafterend}
% The code environment.
%
% The implementation is based on plainhscode in lhs2TeX's
% polycode.fmt, written by Andres Löh.
\newenvironment{code}{%
\ifthenelse{\value{Agda@SpaceAroundCode} = 0 \or%
\not \(\value{Agda@Suppress} = 0 \or%
\value{Agda@SuppressCurrent} = 1\)}{%
\AgdaNewlineWithVerticalSpace{0pt}}{%
\AgdaNewlineWithVerticalSpace{\abovedisplayskip}}%
\advance\leftskip\mathindent%
\AgdaCodeStyle%
\pboxed%
\ifthenelse{\value{Agda@Align} = 0}{}{%
\ifthenelse{\value{Agda@AlignCurrent} = 1}{%
\savecolumns}{%
\restorecolumns}}}{%
\endpboxed%
\ifthenelse{\value{Agda@SpaceAroundCode} = 0 \or%
\not \(\value{Agda@Suppress} = 0 \or%
\value{Agda@SuppressCurrent} =%
\value{Agda@SuppressLast}\)}{%
\AgdaNewlineWithVerticalSpace{0pt}}{%
\AgdaNewlineWithVerticalSpace{\belowdisplayskip}}%
\stepcounter{Agda@AlignCurrent}%
\stepcounter{Agda@SuppressCurrent}%
\ignorespacesafterend}
% Default column for polytable.
\defaultcolumn{@{~}l@{~}}
\endinput