Syntax Highlighting in VIM
The Agda compiler has an option to generate VIM syntax files.
To generate a VIM syntax file for a specific Agda file named file.agda, simply use "agda --vim file.agda".
This will generate a file named .file.vim in the current directory.
It will also recursively generate VIM syntax files for all the corresponding Agda source files for each imported module and place them in the directory where the source files reside.
For generic Agda syntax highlighting, copy the VIM syntax file to ~/.vim/syntax/agda.vim . An example of such a file is given later in this document. To use the syntax file, add the following line to ~/.vim/filetype.vim :
au BufNewFile,BufRead *.agda setf agda
The above command causes VIM to automatically load the file ~/.vim/syntax/agda.vim each time a file with the file extension .agda is opened for editing.
To get the local VIM syntax highlighting file to load after the generic syntax highlighting file, you can either manually execute :source .%.vim in command mode. For automatic loading of syntax files, you can create a file named ~/.vim/after/syntax/agda.vim and add the following:
function! ReloadSyntax()
syntax clear
runtime syntax/agda.vim
let f = expand('%:h') . "/." . expand('%:t') . ".vim"
if filereadable(f)
exec "source " . escape(f, '*')
endif
endfunction
call ReloadSyntax()
map ,rs :call ReloadSyntax()<CR>
This will cause the local syntax file to be loaded after generic Agda syntax file. Furthermore, you can execute ,rs in command to reload the local syntax file.
Work has begun on a generic Agda syntax highlighting file, however, it is still incomplete:
" File: ~/.vim/syntax/agda.vim
if version < 600
syn clear
elseif exists("b:current_syntax")
finish
endif
" To tokenize, the best pattern I've found so far is this:
" (^|\s|[.(){};])@<=token($|\s|[.(){};])@=
" The patterns @<= and @= look behind and ahead, respectively, without matching.
" `agda --vim` extends these groups:
" agdaConstructor
" agdaFunction
" agdaInfixConstructor
" agdaInfixFunction
syn match agdaKeywords "\v(^|\s|[.(){};])@<=(abstract|data|hiding|import|as|infix|infixl|infixr|module|mutual|open|primitive|private|public|record|renaming|rewrite|using|where|with|field|constructor|infix|infixl|infixr|syntax)($|\s|[.(){};])@="
syn match agdaDubious "\v(^|\s|[.(){};])@<=(postulate|codata)($|\s|[.(){};])@="
syn match agdaOperator "\v(^|\s|[.(){};])@<=(let|in|forall|λ|→|-\>|:|∀|\=|\||\\)($|\s|[.(){};])@="
syn match agdaFunction "\v(^|\s|[.(){};])@<=(Set[0-9₀-₉]*)($|\s|[.(){};])@="
syn match agdaNumber "\v(^|\s|[.(){};])@<=[0-9]+($|\s|[.(){};])@="
syn match agdaCharCode contained "\\\([0-9]\+\|o[0-7]\+\|x[0-9a-fA-F]\+\|[\"\\'&\\abfnrtv]\|^[A-Z^_\[\\\]]\)"
syn match agdaCharCode contained "\v\\(NUL|SOH|STX|ETX|EOT|ENQ|ACK|BEL|BS|HT|LF|VT|FF|CR|SO|SI|DLE|DC1|DC2|DC3|DC4|NAK|SYN|ETB|CAN|EM|SUB|ESC|FS|GS|RS|US|SP|DEL)"
syn match agdaCharCodeErr contained "\\&\|'''\+"
syn region agdaString start=+"+ skip=+\\\\\|\\"+ end=+"+ contains=agdaCharCode
syn match agdaHole "\v(^|\s|[.(){};])@<=(\?)($|\s|[.(){};])@="
syn region agdaX matchgroup=agdaHole start="{!" end="!}" contains=ALL
syn match agdaLineComment "\v(^|\s|[.(){};])@<=--.*$" contains=@agdaInComment
syn region agdaBlockComment start="{-" end="-}" contains=agdaBlockComment,@agdaInComment
syn region agdaPragma start="{-#" end="#-}"
syn cluster agdaInComment contains=agdaTODO,agdaFIXME,agdaXXX
syn keyword agdaTODO contained TODO
syn keyword agdaFIXME contained FIXME
syn keyword agdaXXX contained XXX
hi def link agdaNumber Number
hi def link agdaString String
hi def link agdaConstructor Constant
hi def link agdaCharCode SpecialChar
hi def link agdaCharCodeErr Error
hi def link agdaHole WarningMsg
hi def link agdaDubious WarningMsg
hi def link agdaKeywords Structure
hi def link agdaFunction Macro
hi def link agdaOperator Operator
hi def link agdaInfixConstructor Operator
hi def link agdaInfixFunction Operator
hi def link agdaLineComment Comment
hi def link agdaBlockComment Comment
hi def link agdaPragma Comment
hi def agdaTODO cterm=bold,underline ctermfg=2 " green
hi def agdaFIXME cterm=bold,underline ctermfg=3 " yellow
hi def agdaXXX cterm=bold,underline ctermfg=1 " red
Typing Unicode Characters
Agda code commonly uses unicode characters for many mathematical and logical notations like:
The best way is to use XCompose.
Another easy way to enter unicode in vim is to create mappings in insert mode:
imap <buffer> \forall ∀ imap <buffer> \to → imap <buffer> \lambda λ imap <buffer> \Sigma Σ imap <buffer> \exists ∃ imap <buffer> \equiv ≡
Then to get a ∀, just type \forall in insert mode. Many more example mappings can be found in agda-utf8.vim and unicode-keys.vim. Add mappings to ~/after/syntax/agda.vim (or ~/.vimrc, if you want them available globally). More information can be found on the vim wiki: Entering Special Characters.
Holes in vim
There is some preliminary, unofficial support for using holes a la the emacs mode at agda-vim as well as a compilation of a selection of the scripts referenced above.
Emulating vi inside emacs
It's worth mentioning that using agda-mode in emacs is more than syntax highlighting and utf-8 insertion, holes and all features that come with them makes a big difference.
A good option is to use Evil.
;;; Maps C-c C-<key> to \<key in evil-normal-state
(eval-after-load 'agda2
'(progn
(evil-define-key 'normal agda2-mode-map
"\\a" 'agda2-auto
"\\k" 'agda2-previous-goal
"\\j" 'agda2-next-goal
"\\c" 'agda2-make-case
"\\d" 'agda2-infer-type-maybe-toplevel
"\\e" 'agda2-show-context
"\\l" 'agda2-load
"\\n" 'agda2-compute-normalised-maybe-toplevel
"\\o" 'agda2-module-contents-maybe-toplevel
"\\r" 'agda2-refine
"\\s" 'agda2-solveAll
"\\t" 'agda2-goal-type
"\\ " 'agda2-give
"\\," 'agda2-goal-and-context
"\\." 'agda2-goal-and-context-and-inferred
"\\=" 'agda2-show-constraints
"\\?" 'agda2-show-goals
"\\xc" 'agda2-compile
"\\xd" 'agda2-remove-annotations
"\\xh" 'agda2-display-implicit-arguments
"\\xl" 'agda2-load
"\\xq" 'agda2-quit
"\\xr" 'agda2-restart)))
Alternatively, add the following to your .emacs to emulate vi keybindings inside emacs:
; Viper mode emulates basic vi keys, part of emacs. (setq viper-mode t) (require 'viper) ; Vimpulse emulates some more advanced vim keys, needs to be downloaded ; and put into emacs load-path. ; http://www.emacswiki.org/emacs/vimpulse.el ; (require 'vimpulse) ; Rect-mark improves visual mode (I think), also needs to be downloaded ; and put into emacs load-path. ; http://www.emacswiki.org/cgi-bin/wiki/download/rect-mark.el ; (require 'rect-mark) ; If you choose level 5 (I think you should) when viper asks what ; skill level you are, you will get access to all of emacs key ; bindings on top of vi's -- this can be annoying, when you by accident ; use some of emacs' bindings. The following disables some emacs bindings ; you probably won't miss anyway: (global-unset-key (kbd "M-k")) (global-unset-key (kbd "M-j")) (global-unset-key (kbd "M-h")) (global-unset-key (kbd "M-l")) (global-unset-key (kbd "M-o")) (global-unset-key (kbd "C-x C-l")) (global-unset-key (kbd "C-x C-d")) (global-unset-key (kbd "M-:")) (global-unset-key (kbd "M-u")) ; If you use emacs from a terminal you want to add the following bindings, ; for some reason they work in GUI mode but not in terminal mode. (global-set-key (kbd "C-c ,") 'agda2-goal-and-context) (global-set-key (kbd "C-c .") 'agda2-goal-and-context-and-inferred) (global-set-key (kbd "C-c C-@") 'agda2-give)
For unicode input in evil, you need to set a hook that when you go into insert mode, Agda input is turned on. Add this to your .emacs,
(add-hook 'evil-insert-state-entry-hook (lambda () (set-input-method "Agda"))) (add-hook 'evil-insert-state-exit-hook (lambda () (set-input-method nil)))