[Agda] VIM syntax highlighting for Agda

Nicolas Pouillard nicolas.pouillard at gmail.com
Wed Feb 24 10:16:03 CET 2010


On Wed, 24 Feb 2010 09:44:12 +0100, Anthony de Almeida Lopes <guerrilla_thought at gmx.de> wrote:
> Petr,
>  Agda can generate VIM syntax files with the --vim argument. This
> generates hidden VIM syntax files in the current directory. I use a
> VIM script that is loaded when an Agda source file is loaded that
> loads the Agda-VIM syntax highlighting (which I made by modifying
> Haskell's) and then loads the syntax file for the specific Agda source
> file that I'm working on. Of course this is bound to a key so that I
> do not have to restart VIM each time I modify the file in a way that
> would require a syntax update.
> 
> I've attached my (incomplete) VIM syntax file and below I'll paste the
> other command:
> 
> function ReloadSyntax()
>         if filereadable("." . expand('%:') . ".vim")
>                 source .%.vim
>         endif
> endfunction
> 
> map ,rs :call ReloadSyntax()<CR>

Thanks!

> Another tip: to get some shortcuts for UTF-8, add the following kind
> of lines to your syntax too:
> 
> imap <buffer> \forall ∀
> 
> This way you can just type "a : \forall" and it immediatly transforms to "a : ∀"

To input fancy characters, I use XCompose. It has the nice property to work on
any X application and so I can type those pretty much everywhere. To have a
growing set of shortcuts for fancy characters I use a module of the Yi editor
project and generate my .XCompose file.

-- 
Nicolas Pouillard
http://nicolaspouillard.fr


More information about the Agda mailing list