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)))