[Agda] Re: Indentation in stdlib files

gallais guillaume.allais at ens-lyon.org
Fri Feb 13 14:29:50 CET 2015


Would it be welcomed to add these to the standard agda-mode?


On 13/02/15 11:47, N. Raghavendra wrote:
> At 2015-02-13T08:19:44+01:00, Andreas Abel wrote:
>
>> To align at ":" I use the align-regexp command of emacs.  (Of course,
>> it is not restricted to ":"...)
>>
>> Mark a region
>> M-x align-regexp RET
>> : RET
> Thanks!  With that and https://wiki.haskell.org/Emacs/Indentation, I've
> this in my Emacs init file now:
>
> --8<---------------cut here---------------start------------->8---
> (require 'align)
>
> (add-to-list 'align-rules-list
>               `(agda-colons
>                 (regexp . "\\(\\s-+\\)\\(:\\|∶\\)\\s-+")
>                 (modes . '(agda2-mode))))
>
> (add-to-list 'align-rules-list
>               `(agda-equals
>                 (regexp . "\\(\\s-+\\)=\\s-+")
>                 (modes . '(agda2-mode))))
>
> (add-to-list 'align-rules-list
>               `(agda-arrows
>                 (regexp . "\\(\\s-+\\)\\(->\\|→\\)\\s-+")
>                 (modes . '(agda2-mode))))
>
> (global-set-key (kbd "M-[") 'align)
> --8<---------------cut here---------------end--------------->8---
>
> I don't know if I'll need to align equals and arrows, but no harm having
> them also in the rules.
>
> Cheers,
> Raghu.
>



More information about the Agda mailing list