[Agda] Indentation for abstract and private declarations

[Guillaume Brunerie]

Hello,
I have a very practical question about indentation and emacs
interaction with Agda.
Suppose I have a program spanning several lines:

> program : type
> program = something
>   something-else
>   again-something-else

(lines 3 and 4 are indented with two spaces)

Now I decide that I want it to be abstract (or private).
What sequence of key-press am I supposed to do?

If I simply add a line "abstract" at the beginning, this doesn’t work
because the next two lines want to be indented more than the
"abstract" line.
If I indent the next two lines with two spaces, this doesn’t work
either because the two lines after that will want to be indented even
further

1. I can indent the first two lines with only one space, but one-space
indentation is a bit weird
2. I can indent the first two lines with two spaces and the subsequent
lines with four spaces, but this also looks weird because it doesn’t
match the rest of the file and I haven’t found an easy way to indent a
block of code (select + tab doesn’t work, so I usually use an emacs
macro to add two spaces at the beginning of each line, but this seems
overkill)

Also, would it be possible to be able to define abstract or private
terms without having to indent everything further ?

Thanks,

Guillaume