[Agda] VIM syntax highlighting for Agda

Anthony de Almeida Lopes guerrilla_thought at gmx.de
Wed Feb 24 09:44:12 CET 2010


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>

Note that the general Agda syntax file should go in
~/.vim/syntax/agda.vim and the other piece of code goes in
~/.vim/after/syntax/agda.vim

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 : ∀"

- Tony

On 24 February 2010 08:38, Petr Pudlak <deb at pudlak.name> wrote:
> Hi,
>
> is there a VIM syntax highlighting script for Agda?
>
> At Hackage I saw a package Agda.Interaction.Highlighting.Vim, but I
> have no idea how (or if) I can use it to highlight Agda sources in Vim.
>
>    Thanks,
>    Petr Pudlak
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: agda.vim
Type: application/octet-stream
Size: 1079 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20100224/9baf51b0/agda.obj


More information about the Agda mailing list