[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