Evgenii Akentev
·
2019-01-18
agda.sty
1% ----------------------------------------------------------------------
2% Some useful commands when doing highlighting of Agda code in LaTeX.
3% ----------------------------------------------------------------------
4
5\ProvidesPackage{agda}
6
7\RequirePackage{ifxetex, ifluatex, xifthen, xcolor, polytable, etoolbox}
8
9% https://tex.stackexchange.com/questions/47576/combining-ifxetex-and-ifluatex-with-the-logical-or-operation
10\newif\ifxetexorluatex
11\ifxetex
12 \xetexorluatextrue
13\else
14 \ifluatex
15 \xetexorluatextrue
16 \else
17 \xetexorluatexfalse
18 \fi
19\fi
20
21% XeLaTeX or LuaLaTeX
22\ifxetexorluatex
23
24 % Hack to get the amsthm package working.
25 % https://tex.stackexchange.com/questions/130491/xelatex-error-paragraph-ended-before-tempa-was-complete
26 \let\AgdaOpenBracket\[\let\AgdaCloseBracket\]
27 \RequirePackage{fontspec}
28 \let\[\AgdaOpenBracket\let\]\AgdaCloseBracket
29 \RequirePackage{unicode-math}
30
31 \tracinglostchars=2 % If the font is missing some symbol, then say
32 % so in the compilation output.
33 \setmainfont
34 [ Ligatures = TeX
35 , BoldItalicFont = xits-bolditalic.otf
36 , BoldFont = xits-bold.otf
37 , ItalicFont = xits-italic.otf
38 ]
39 {xits-regular.otf}
40
41 \setmathfont{xits-math.otf}
42 \setmonofont[Mapping=tex-text]{FreeMono.otf}
43
44 % Make mathcal and mathscr appear as different.
45 % https://tex.stackexchange.com/questions/120065/xetex-what-happened-to-mathcal-and-mathscr
46 \setmathfont[range={\mathcal,\mathbfcal},StylisticSet=1]{xits-math.otf}
47 \setmathfont[range=\mathscr]{xits-math.otf}
48
49 \providecommand{\DeclareUnicodeCharacter}[2]{\relax}
50
51% pdfLaTeX
52\else
53 \RequirePackage{ucs, amsfonts, amssymb}
54 \RequirePackage[safe]{tipa} % See page 12 of the tipa manual for what
55 % safe does.
56
57 % https://tex.stackexchange.com/questions/1774/how-to-insert-pipe-symbol-in-latex
58 \RequirePackage[T1]{fontenc}
59 \RequirePackage[utf8x]{inputenc}
60\fi
61
62% ----------------------------------------------------------------------
63% Options
64
65\DeclareOption{bw} {\newcommand{\AgdaColourScheme}{bw}}
66\DeclareOption{conor}{\newcommand{\AgdaColourScheme}{conor}}
67
68\newif\if@AgdaEnableReferences\@AgdaEnableReferencesfalse
69\DeclareOption{references}{
70 \@AgdaEnableReferencestrue
71}
72
73\newif\if@AgdaEnableLinks\@AgdaEnableLinksfalse
74\DeclareOption{links}{
75 \@AgdaEnableLinkstrue
76}
77
78\ProcessOptions\relax
79
80% ----------------------------------------------------------------------
81% Colour schemes.
82
83\providecommand{\AgdaColourScheme}{standard}
84
85% ----------------------------------------------------------------------
86% References to code (needs additional post-processing of tex files to
87% work, see wiki for details).
88
89\if@AgdaEnableReferences
90 \RequirePackage{catchfilebetweentags, xstring}
91 \newcommand{\AgdaRef}[2][]{%
92 \StrSubstitute{#2}{\_}{AgdaUnderscore}[\tmp]%
93 \ifthenelse{\isempty{#1}}%
94 {\ExecuteMetaData{AgdaTag-\tmp}}%
95 {\ExecuteMetaData{#1}{AgdaTag-\tmp}}
96 }
97\fi
98
99\providecommand{\AgdaRef}[2][]{#2}
100
101% ----------------------------------------------------------------------
102% Links (only done if the option is passed and the user has loaded the
103% hyperref package).
104
105\if@AgdaEnableLinks
106 \@ifpackageloaded{hyperref}{
107
108 % List that holds added targets.
109 \newcommand{\AgdaList}[0]{}
110
111 \newtoggle{AgdaIsElem}
112 \newcounter{AgdaIndex}
113 \newcommand{\AgdaLookup}[3]{%
114 \togglefalse{AgdaIsElem}%
115 \setcounter{AgdaIndex}{0}%
116 \renewcommand*{\do}[1]{%
117 \ifstrequal{#1}{##1}%
118 {\toggletrue{AgdaIsElem}\listbreak}%
119 {\stepcounter{AgdaIndex}}}%
120 \dolistloop{\AgdaList}%
121 \iftoggle{AgdaIsElem}{#2}{#3}%
122 }
123
124 \newcommand*{\AgdaTargetHelper}[1]{%
125 \AgdaLookup{#1}%
126 {\PackageError{agda}{``#1'' used as target more than once}%
127 {Overloaded identifiers and links do not%
128 work well, consider using unique%
129 \MessageBreak identifiers instead.}%
130 }%
131 {\listadd{\AgdaList}{#1}%
132 \hypertarget{Agda\theAgdaIndex}{}%
133 }%
134 }
135
136 \newcommand{\AgdaTarget}[1]{\forcsvlist{\AgdaTargetHelper}{#1}}
137
138 \newcommand{\AgdaLink}[1]{%
139 \AgdaLookup{#1}%
140 {\hyperlink{Agda\theAgdaIndex}{#1}}%
141 {#1}%
142 }
143 }{\PackageError{agda}{Load the hyperref package before the agda package}{}}
144\fi
145
146\providecommand{\AgdaTarget}[1]{}
147\providecommand{\AgdaLink}[1]{#1}
148
149% ----------------------------------------------------------------------
150% Font styles.
151
152\ifxetexorluatex
153 \newcommand{\AgdaFontStyle}[1]{\ensuremath{\mathsf{#1}}}
154 \ifthenelse{\equal{\AgdaColourScheme}{bw}}{
155 \newcommand{\AgdaKeywordFontStyle}[1]{\underline{#1}}
156 }{
157 \newcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathsf{#1}}}
158 }
159 \newcommand{\AgdaStringFontStyle}[1]{\ensuremath{\texttt{#1}}}
160 \newcommand{\AgdaCommentFontStyle}[1]{\ensuremath{\texttt{#1}}}
161 \newcommand{\AgdaBoundFontStyle}[1]{\ensuremath{\mathit{#1}}}
162
163\else
164 \newcommand{\AgdaFontStyle}[1]{\textsf{#1}}
165 \ifthenelse{\equal{\AgdaColourScheme}{bw}}{
166 \newcommand{\AgdaKeywordFontStyle}[1]{\underline{#1}}
167 }{
168 \newcommand{\AgdaKeywordFontStyle}[1]{\textsf{#1}}
169 }
170 \newcommand{\AgdaStringFontStyle}[1]{\texttt{#1}}
171 \newcommand{\AgdaCommentFontStyle}[1]{\texttt{#1}}
172 \newcommand{\AgdaBoundFontStyle}[1]{\textit{#1}}
173\fi
174
175% ----------------------------------------------------------------------
176% Colours.
177
178% ----------------------------------
179% The black and white colour scheme.
180\ifthenelse{\equal{\AgdaColourScheme}{bw}}{
181
182 % Aspect colours.
183 \definecolor{AgdaComment} {HTML}{000000}
184 \definecolor{AgdaOption} {HTML}{000000}
185 \definecolor{AgdaKeyword} {HTML}{000000}
186 \definecolor{AgdaString} {HTML}{000000}
187 \definecolor{AgdaNumber} {HTML}{000000}
188 \definecolor{AgdaSymbol} {HTML}{000000}
189 \definecolor{AgdaPrimitiveType}{HTML}{000000}
190 \definecolor{AgdaOperator} {HTML}{000000}
191
192 % NameKind colours.
193 \definecolor{AgdaBound} {HTML}{000000}
194 \definecolor{AgdaInductiveConstructor} {HTML}{000000}
195 \definecolor{AgdaCoinductiveConstructor}{HTML}{000000}
196 \definecolor{AgdaDatatype} {HTML}{000000}
197 \definecolor{AgdaField} {HTML}{000000}
198 \definecolor{AgdaFunction} {HTML}{000000}
199 \definecolor{AgdaMacro} {HTML}{000000}
200 \definecolor{AgdaModule} {HTML}{000000}
201 \definecolor{AgdaPostulate} {HTML}{000000}
202 \definecolor{AgdaPrimitive} {HTML}{000000}
203 \definecolor{AgdaRecord} {HTML}{000000}
204 \definecolor{AgdaArgument} {HTML}{000000}
205
206 % Other aspect colours.
207 \definecolor{AgdaDottedPattern} {HTML}{000000}
208 \definecolor{AgdaUnsolvedMeta} {HTML}{D3D3D3}
209 \definecolor{AgdaTerminationProblem}{HTML}{BEBEBE}
210 \definecolor{AgdaIncompletePattern} {HTML}{D3D3D3}
211 \definecolor{AgdaError} {HTML}{696969}
212
213 % Misc.
214 \definecolor{AgdaHole} {HTML}{BEBEBE}
215
216% ----------------------------------
217% Conor McBride's colour scheme.
218}{ \ifthenelse{\equal{\AgdaColourScheme}{conor}}{
219
220 % Aspect colours.
221 \definecolor{AgdaComment} {HTML}{B22222}
222 \definecolor{AgdaOption} {HTML}{000000}
223 \definecolor{AgdaKeyword} {HTML}{000000}
224 \definecolor{AgdaString} {HTML}{000000}
225 \definecolor{AgdaNumber} {HTML}{000000}
226 \definecolor{AgdaSymbol} {HTML}{000000}
227 \definecolor{AgdaPrimitiveType}{HTML}{0000CD}
228 \definecolor{AgdaOperator} {HTML}{000000}
229
230 % NameKind colours.
231 \definecolor{AgdaBound} {HTML}{A020F0}
232 \definecolor{AgdaInductiveConstructor} {HTML}{8B0000}
233 \definecolor{AgdaCoinductiveConstructor}{HTML}{8B0000}
234 \definecolor{AgdaDatatype} {HTML}{0000CD}
235 \definecolor{AgdaField} {HTML}{8B0000}
236 \definecolor{AgdaFunction} {HTML}{006400}
237 \definecolor{AgdaMacro} {HTML}{006400}
238 \definecolor{AgdaModule} {HTML}{006400}
239 \definecolor{AgdaPostulate} {HTML}{006400}
240 \definecolor{AgdaPrimitive} {HTML}{006400}
241 \definecolor{AgdaRecord} {HTML}{0000CD}
242 \definecolor{AgdaArgument} {HTML}{404040}
243
244 % Other aspect colours.
245 \definecolor{AgdaDottedPattern} {HTML}{000000}
246 \definecolor{AgdaUnsolvedMeta} {HTML}{FFD700}
247 \definecolor{AgdaTerminationProblem}{HTML}{FF0000}
248 \definecolor{AgdaIncompletePattern} {HTML}{A020F0}
249 \definecolor{AgdaError} {HTML}{F4A460}
250
251 % Misc.
252 \definecolor{AgdaHole} {HTML}{9DFF9D}
253
254% ----------------------------------
255% The standard colour scheme.
256}{
257 % Aspect colours.
258 \definecolor{AgdaComment} {HTML}{B22222}
259 \definecolor{AgdaOption} {HTML}{000000}
260 \definecolor{AgdaKeyword} {HTML}{CD6600}
261 \definecolor{AgdaString} {HTML}{B22222}
262 \definecolor{AgdaNumber} {HTML}{A020F0}
263 \definecolor{AgdaSymbol} {HTML}{404040}
264 \definecolor{AgdaPrimitiveType}{HTML}{0000CD}
265 \definecolor{AgdaOperator} {HTML}{000000}
266
267 % NameKind colours.
268 \definecolor{AgdaBound} {HTML}{000000}
269 \definecolor{AgdaInductiveConstructor} {HTML}{008B00}
270 \definecolor{AgdaCoinductiveConstructor}{HTML}{8B7500}
271 \definecolor{AgdaDatatype} {HTML}{0000CD}
272 \definecolor{AgdaField} {HTML}{EE1289}
273 \definecolor{AgdaFunction} {HTML}{0000CD}
274 \definecolor{AgdaMacro} {HTML}{458B74}
275 \definecolor{AgdaModule} {HTML}{A020F0}
276 \definecolor{AgdaPostulate} {HTML}{0000CD}
277 \definecolor{AgdaPrimitive} {HTML}{0000CD}
278 \definecolor{AgdaRecord} {HTML}{0000CD}
279 \definecolor{AgdaArgument} {HTML}{404040}
280
281 % Other aspect colours.
282 \definecolor{AgdaDottedPattern} {HTML}{000000}
283 \definecolor{AgdaUnsolvedMeta} {HTML}{FFFF00}
284 \definecolor{AgdaTerminationProblem}{HTML}{FFA07A}
285 \definecolor{AgdaIncompletePattern} {HTML}{F5DEB3}
286 \definecolor{AgdaError} {HTML}{FF0000}
287
288 % Misc.
289 \definecolor{AgdaHole} {HTML}{9DFF9D}
290}}
291
292% ----------------------------------------------------------------------
293% Commands.
294
295\newcommand{\AgdaNoSpaceMath}[1]
296 {\begingroup\thickmuskip=0mu\medmuskip=0mu#1\endgroup}
297
298% Aspect commands.
299\newcommand{\AgdaComment} [1]
300 {\AgdaNoSpaceMath{\AgdaCommentFontStyle{\textcolor{AgdaComment}{#1}}}}
301\newcommand{\AgdaOption} [1]
302 {\AgdaNoSpaceMath{\AgdaCommentFontStyle{\textcolor{AgdaOption}{#1}}}}
303\newcommand{\AgdaKeyword} [1]
304 {\AgdaNoSpaceMath{\AgdaKeywordFontStyle{\textcolor{AgdaKeyword}{#1}}}}
305\newcommand{\AgdaString} [1]
306 {\AgdaNoSpaceMath{\AgdaStringFontStyle{\textcolor{AgdaString}{#1}}}}
307\newcommand{\AgdaNumber} [1]
308 {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaNumber}{#1}}}}
309\newcommand{\AgdaSymbol} [1]
310 {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaSymbol}{#1}}}}
311\newcommand{\AgdaPrimitiveType}[1]
312 {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaPrimitiveType}{#1}}}}
313\newcommand{\AgdaOperator} [1]
314 {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaOperator}{#1}}}}
315
316% NameKind commands.
317
318% The user can control the typesetting of (certain) individual tokens
319% by redefining the following command. The first argument is the token
320% and the second argument the thing to be typeset (sometimes just the
321% token, sometimes \AgdaLink{<the token>}). Example:
322%
323% \usepackage{ifthen}
324%
325% % Insert extra space before some tokens.
326% \DeclareRobustCommand{\AgdaFormat}[2]{%
327% \ifthenelse{
328% \equal{#1}{≡⟨} \OR
329% \equal{#1}{≡⟨⟩} \OR
330% \equal{#1}{∎}
331% }{\ }{}#2}
332%
333% Note the use of \DeclareRobustCommand.
334
335\newcommand{\AgdaFormat}[2]{#2}
336
337\newcommand{\AgdaBound}[1]
338 {\AgdaNoSpaceMath{\AgdaBoundFontStyle{\textcolor{AgdaBound}{\AgdaFormat{#1}{#1}}}}}
339\newcommand{\AgdaInductiveConstructor}[1]
340 {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaInductiveConstructor}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
341\newcommand{\AgdaCoinductiveConstructor}[1]
342 {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaCoinductiveConstructor}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
343\newcommand{\AgdaDatatype}[1]
344 {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaDatatype}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
345\newcommand{\AgdaField}[1]
346 {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaField}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
347\newcommand{\AgdaFunction}[1]
348 {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaFunction}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
349\newcommand{\AgdaMacro}[1]
350 {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaMacro}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
351\newcommand{\AgdaModule}[1]
352 {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaModule}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
353\newcommand{\AgdaPostulate}[1]
354 {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaPostulate}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
355\newcommand{\AgdaPrimitive}[1]
356 {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaPrimitive}{\AgdaFormat{#1}{#1}}}}}
357\newcommand{\AgdaRecord}[1]
358 {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaRecord}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
359\newcommand{\AgdaArgument}[1]
360 {\AgdaNoSpaceMath{\AgdaBoundFontStyle{\textcolor{AgdaArgument}{\AgdaFormat{#1}{#1}}}}}
361
362% Other aspect commands.
363\newcommand{\AgdaFixityOp} [1]{\AgdaNoSpaceMath{$#1$}}
364\newcommand{\AgdaDottedPattern} [1]{\textcolor{AgdaDottedPattern}{#1}}
365\newcommand{\AgdaUnsolvedMeta} [1]
366 {\AgdaFontStyle{\colorbox{AgdaUnsolvedMeta}{#1}}}
367\newcommand{\AgdaTerminationProblem}[1]
368 {\AgdaFontStyle{\colorbox{AgdaTerminationProblem}{#1}}}
369\newcommand{\AgdaIncompletePattern} [1]{\colorbox{AgdaIncompletePattern}{#1}}
370\newcommand{\AgdaError} [1]
371 {\AgdaFontStyle{\textcolor{AgdaError}{\underline{#1}}}}
372
373% Misc.
374\newcommand{\AgdaHole}[1]{\colorbox{AgdaHole}{#1}}
375\long\def\AgdaHide#1{\ignorespaces} % Used to hide code from LaTeX.
376
377% ----------------------------------------------------------------------
378% The code environment.
379
380\newcommand{\AgdaCodeStyle}{\fontsize{12pt}{14pt}}
381% \newcommand{\AgdaCodeStyle}{\tiny}
382
383\ifdefined\mathindent
384 {}
385\else
386 \newdimen\mathindent\mathindent\leftmargini
387\fi
388
389% Adds the given amount of vertical space and starts a new line.
390%
391% The implementation comes from lhs2TeX's polycode.fmt, written by
392% Andres Löh.
393\newcommand{\AgdaNewlineWithVerticalSpace}[1]{%
394 {\parskip=0pt\parindent=0pt\par\vskip #1\noindent}}
395
396% 0: No space around code. 1: Space around code.
397\newcounter{Agda@SpaceAroundCode}
398
399% Use this command to avoid extra space around code blocks.
400\newcommand{\AgdaNoSpaceAroundCode}{%
401 \setcounter{Agda@SpaceAroundCode}{0}}
402
403% Use this command to include extra space around code blocks.
404\newcommand{\AgdaSpaceAroundCode}{%
405 \setcounter{Agda@SpaceAroundCode}{1}}
406
407% By default space is inserted around code blocks.
408\AgdaSpaceAroundCode{}
409
410% Sometimes one might want to break up a code block into multiple
411% pieces, but keep code in different blocks aligned with respect to
412% each other. Then one can use the AgdaAlign environment. Example
413% usage:
414%
415% \begin{AgdaAlign}
416% \begin{code}
417% code
418% code (more code)
419% \end{code}
420% Explanation...
421% \begin{code}
422% aligned with "code"
423% code (aligned with (more code))
424% \end{code}
425% \end{AgdaAlign}
426%
427% Note that AgdaAlign environments should not be nested.
428%
429% Sometimes one might also want to hide code in the middle of a code
430% block. This can be accomplished in the following way:
431%
432% \begin{AgdaAlign}
433% \begin{code}
434% visible
435% \end{code}
436% \AgdaHide{
437% \begin{code}
438% hidden
439% \end{code}}
440% \begin{code}
441% visible
442% \end{code}
443% \end{AgdaAlign}
444%
445% However, the result may be ugly: extra space is perhaps inserted
446% around the code blocks.
447%
448% The AgdaSuppressSpace environment ensures that extra space is only
449% inserted before the first code block, and after the last one (but
450% not if \AgdaNoSpaceAroundCode{} is used).
451%
452% The environment takes one argument, the number of wrapped code
453% blocks (excluding hidden ones). Example usage:
454%
455% \begin{AgdaAlign}
456% \begin{code}
457% code
458% more code
459% \end{code}
460% Explanation...
461% \begin{AgdaSuppressSpace}{2}
462% \begin{code}
463% aligned with "code"
464% aligned with "more code"
465% \end{code}
466% \AgdaHide{
467% \begin{code}
468% hidden code
469% \end{code}}
470% \begin{code}
471% also aligned with "more code"
472% \end{code}
473% \end{AgdaSuppressSpace}
474% \end{AgdaAlign}
475%
476% Note that AgdaSuppressSpace environments should not be nested.
477%
478% There is also a combined environment, AgdaMultiCode, that combines
479% the effects of AgdaAlign and AgdaSuppressSpace.
480
481% 0: AgdaAlign is not active. 1: AgdaAlign is active.
482\newcounter{Agda@Align}
483\setcounter{Agda@Align}{0}
484
485% The current code block.
486\newcounter{Agda@AlignCurrent}
487
488\newcommand{\Agda@AlignStart}{%
489 \setcounter{Agda@Align}{1}%
490 \setcounter{Agda@AlignCurrent}{1}}
491
492\newcommand{\Agda@AlignEnd}{\setcounter{Agda@Align}{0}}
493
494\newenvironment{AgdaAlign}{%
495 \Agda@AlignStart{}}{%
496 \Agda@AlignEnd{}%
497 \ignorespacesafterend}
498
499% 0: AgdaSuppressSpace is not active. 1: AgdaSuppressSpace is active.
500\newcounter{Agda@Suppress}
501\setcounter{Agda@Suppress}{0}
502
503% The current code block.
504\newcounter{Agda@SuppressCurrent}
505
506% The expected number of code blocks.
507\newcounter{Agda@SuppressLast}
508
509\newcommand{\Agda@SuppressStart}[1]{%
510 \setcounter{Agda@Suppress}{1}%
511 \setcounter{Agda@SuppressLast}{#1}%
512 \setcounter{Agda@SuppressCurrent}{1}}
513
514\newcommand{\Agda@SuppressEnd}{\setcounter{Agda@Suppress}{0}}
515
516\newenvironment{AgdaSuppressSpace}[1]{%
517 \Agda@SuppressStart{#1}}{%
518 \Agda@SuppressEnd{}%
519 \ignorespacesafterend}
520
521\newenvironment{AgdaMultiCode}[1]{%
522 \Agda@AlignStart{}%
523 \Agda@SuppressStart{#1}}{%
524 \Agda@SuppressEnd{}%
525 \Agda@AlignEnd{}%
526 \ignorespacesafterend}
527
528% The code environment.
529%
530% The implementation is based on plainhscode in lhs2TeX's
531% polycode.fmt, written by Andres Löh.
532\newenvironment{code}{%
533 \ifthenelse{\value{Agda@SpaceAroundCode} = 0 \or%
534 \not \(\value{Agda@Suppress} = 0 \or%
535 \value{Agda@SuppressCurrent} = 1\)}{%
536 \AgdaNewlineWithVerticalSpace{0pt}}{%
537 \AgdaNewlineWithVerticalSpace{\abovedisplayskip}}%
538 \advance\leftskip\mathindent%
539 \AgdaCodeStyle%
540 \pboxed%
541 \ifthenelse{\value{Agda@Align} = 0}{}{%
542 \ifthenelse{\value{Agda@AlignCurrent} = 1}{%
543 \savecolumns}{%
544 \restorecolumns}}}{%
545 \endpboxed%
546 \ifthenelse{\value{Agda@SpaceAroundCode} = 0 \or%
547 \not \(\value{Agda@Suppress} = 0 \or%
548 \value{Agda@SuppressCurrent} =%
549 \value{Agda@SuppressLast}\)}{%
550 \AgdaNewlineWithVerticalSpace{0pt}}{%
551 \AgdaNewlineWithVerticalSpace{\belowdisplayskip}}%
552 \stepcounter{Agda@AlignCurrent}%
553 \stepcounter{Agda@SuppressCurrent}%
554 \ignorespacesafterend}
555
556% Space inserted after tokens.
557\newcommand{\AgdaSpace}{ }
558
559% Space inserted to indent something.
560\newcommand{\AgdaIndentSpace}{\AgdaSpace{}$\;\;$}
561
562% Default column for polytable.
563\defaultcolumn{@{}l@{\AgdaSpace{}}}
564
565% \AgdaIndent expects a non-negative integer as its only argument.
566% This integer should be the distance, in code blocks, to the thing
567% relative to which the text is indented.
568%
569% The default implementation only indents if the thing that the text
570% is indented relative to exists in the same code block or is wrapped
571% in the same AgdaAlign or AgdaMultiCode environment.
572\newcommand{\AgdaIndent}[1]{%
573 \ifthenelse{#1 = 0
574 \OR
575 \( \value{Agda@Align} = 1
576 \AND
577 #1 < \value{Agda@AlignCurrent}
578 \)}{\AgdaIndentSpace{}}{}}
579
580\endinput