[Agda] Re: Indentation in stdlib files

N. Raghavendra raghu at hri.res.in
Fri Feb 13 12:47:53 CET 2015


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.

-- 
N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/



More information about the Agda mailing list