[Agda] Indentation for abstract and private declarations

[Wolfram Kahl]

On Thu, Oct 11, 2012 at 10:34:40AM -0400, Guillaume Brunerie wrote:
> 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?
>
> [...]
>
> 1. I can indent the first two lines with only one space, but one-space
> indentation is a bit weird

and does not work with lhs2TeX.

> 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

I live with that...

> and I haven’t found an easy way to indent a
> block of code

With cursor at the beginning of the first original line:

C-Space               -- to set the mark
C-u 3 C-n             -- or some other way to move the cursor to the beginning of the last line
C-x r t               -- insert text into rectangle
  Space Space Return  -- insert two spaces.


Wolfram