691 lines
23 KiB
TeX
691 lines
23 KiB
TeX
% ----------------------------------------------------------------------
|
|
% Some useful commands when doing highlighting of Agda code in LaTeX.
|
|
% ----------------------------------------------------------------------
|
|
|
|
\ProvidesPackage{agda}
|
|
|
|
\RequirePackage{ifxetex, ifluatex, xifthen, xcolor, polytable, etoolbox,
|
|
calc, environ}
|
|
|
|
% 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
|
|
}
|
|
|
|
% 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{nofontsetup}{
|
|
\@AgdaSetupFontsfalse
|
|
}
|
|
|
|
% 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{noinputencodingsetup}{
|
|
\@AgdaSetupInputEncodingfalse
|
|
}
|
|
|
|
\ProcessOptions\relax
|
|
|
|
% ----------------------------------------------------------------------
|
|
% Input encoding setup
|
|
|
|
\if@AgdaSetupInputEncoding
|
|
\ifxetexorluatex
|
|
|
|
\providecommand{\DeclareUnicodeCharacter}[2]{\relax}
|
|
|
|
\else
|
|
|
|
\RequirePackage{ucs}
|
|
\RequirePackage[utf8x]{inputenc}
|
|
|
|
\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{fontspec}
|
|
\let\[\AgdaOpenBracket\let\]\AgdaCloseBracket
|
|
\RequirePackage{unicode-math}
|
|
|
|
\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}
|
|
|
|
% pdfLaTeX
|
|
\else
|
|
|
|
% https://tex.stackexchange.com/questions/1774/how-to-insert-pipe-symbol-in-latex
|
|
\RequirePackage[T1]{fontenc}
|
|
|
|
\RequirePackage{amsfonts, amssymb}
|
|
\RequirePackage[safe]{tipa} % See page 12 of the tipa manual for what
|
|
% safe does.
|
|
|
|
\fi
|
|
\fi
|
|
|
|
% ----------------------------------------------------------------------
|
|
% 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{AgdaOption} {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{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{AgdaOption} {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{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{AgdaOption} {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{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{\AgdaOption} [1]
|
|
{\AgdaNoSpaceMath{\AgdaCommentFontStyle{\textcolor{AgdaOption}{#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{\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 \baselineskip.
|
|
\newlength{\AgdaEmptySkip}
|
|
\setlength{\AgdaEmptySkip}{\baselineskip}
|
|
|
|
% 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].
|
|
%
|
|
% 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}}{}{%
|
|
%
|
|
% 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
|