summaryrefslogtreecommitdiff
path: root/src/data/agda.sty
diff options
context:
space:
mode:
Diffstat (limited to 'src/data/agda.sty')
-rw-r--r--src/data/agda.sty173
1 files changed, 168 insertions, 5 deletions
diff --git a/src/data/agda.sty b/src/data/agda.sty
index 07dd540..bd2cf3e 100644
--- a/src/data/agda.sty
+++ b/src/data/agda.sty
@@ -195,6 +195,7 @@
\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}
@@ -342,7 +343,7 @@
% Misc.
\newcommand{\AgdaHole}[1]{\colorbox{AgdaHole}{#1}}
-\long\def\AgdaHide#1{} % Used to hide code from LaTeX.
+\long\def\AgdaHide#1{\ignorespaces} % Used to hide code from LaTeX.
\newcommand{\AgdaIndent}[1]{$\;\;$}
@@ -358,10 +359,172 @@
\newdimen\mathindent\mathindent\leftmargini
\fi
-\newenvironment{code}%
-{\noindent\ignorespaces\advance\leftskip\mathindent\AgdaCodeStyle\pboxed}%
-{\endpboxed\par\noindent%
-\ignorespacesafterend}
+% 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@{~}}