[Agda] Indentation for abstract and private declarations

[Andreas Abel]

To indent a selected block in Emacs by 2 spaces, press

   C-u 2 C-x C-i

(C-i is the same as TAB).  Alternatively, use the rectangle command

   C-x r t SPC SPC RET

(which can be used to replace a rectangle (which can have width 0) by a 
rectangle of the same height with identical text in each line).

Unfortunately, "abstract" is not available as a modifier for an 
identifier, like in

   abstract program : type
   program = ...

"abstract" always expects a block, and this has to be indented.

Cheers,
Andreas

On 11.10.2012 16:34, Guillaume Brunerie wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/