Incorrect indentation when \AgdaHide is used

[nad]

Consider the following code:

\documentclass{article}

\usepackage{agda}

\pagestyle{empty}

\begin{document}

\noindent Text.
\AgdaHide{
\begin{code}
  mutual
\end{code}}
\begin{code}
    postulate A : Set
\end{code}
More text.
\begin{AgdaMultiCode}{2}
\begin{code}
  mutual
\end{code}
\begin{code}
    postulate B : Set
\end{code}
\end{AgdaMultiCode}
Even more text.

\end{document}

In the resulting document the two code blocks are not aligned:

As a workaround one can add a module header, and make sure that everything is indented relative to it:

\documentclass{article}

\usepackage{agda}

\pagestyle{empty}

\begin{document}

\AgdaHide{
\begin{code}
module Bug where
\end{code}}

\noindent Text.
\AgdaHide{
\begin{code}
  mutual
\end{code}}
\begin{code}
    postulate A : Set
\end{code}
More text.
\begin{AgdaMultiCode}{2}
\begin{code}
  mutual
\end{code}
\begin{code}
    postulate B : Set
\end{code}
\end{AgdaMultiCode}
Even more text.

\end{document}

[nad]

By the way, I found a way to quickly generate PNG files without lots of empty space for use in bug reports:

• Make sure that the document does not contain a page number, for instance by using \pagestyle{empty}.
• Use the ImageMagick command convert in the following way to create the image file:

  convert -density 150 -trim Bug.pdf Bug.png
  

  (The density value could perhaps be a bit lower.)

[andreasabel]

I tried your original example, and found it looks even more wrong when the \AgdaHide is not used.
I did not know that this was even legal Agda code, indentation without a layout keyword. I think the base indentation should be at column 1, everything else should be a syntax error.

[nad]

I tried your original example, and found it looks even more wrong when the \AgdaHide is not used.

From the CHANGELOG: "Note that if any token in L or E belongs to a previous code block, then the constraint may not be satisfied unless (say) the AgdaAlign environment is used in an appropriate way." If you use (say) AgdaMultiCode, then the code without \AgdaHide is unproblematic:

\noindent Text.
\begin{AgdaMultiCode}{2}
\begin{code}
  mutual
\end{code}
\begin{code}
    postulate A : Set
\end{code}
\end{AgdaMultiCode}
More text.
\begin{AgdaMultiCode}{2}
\begin{code}
  mutual
\end{code}
\begin{code}
    postulate B : Set
\end{code}
\end{AgdaMultiCode}
Even more text.

[nad]

The example in the OP has been fixed by 2d85838. However, I'm not satisfied with how the following code is handled:

\documentclass{article}

\usepackage{agda}

\pagestyle{empty}

\begin{document}

\begin{AgdaAlign}
\begin{code}
  postulate
   A : Set
\end{code}
\AgdaHide{
\begin{code}
  mutual
\end{code}}
\begin{code}
    postulate B : Set
\end{code}
\end{AgdaAlign}

\end{document}

Output:

I think \AgdaHide should be deprecated in favour of an environment that does not typeset its contents, but still performs the same kind of bookkeeping as the code environment.

[nad]

Upon closer thought I think that the code above is handled in a reasonable way, assuming that it should be handled at all, rather than throwing an error message.

Here is a different example, that one might expect should work:

\documentclass{article}

\usepackage{agda}
\AgdaNoSpaceAroundCode{}

\pagestyle{empty}

\begin{document}

\begin{AgdaAlign}
\begin{code}
postulate
  A
\end{code}
\AgdaHide{
\begin{code}
    B
\end{code}}
\begin{code}
    C : Set
\end{code}
\end{AgdaAlign}

\end{document}

Output:

Should we even try to handle code of this form?

[nad]

I added a test case for the example in the OP.