diff options
Diffstat (limited to '')
| -rw-r--r-- | README.md | 3 | ||||
| -rw-r--r-- | after/ftplugin/idris.vim | 5 | ||||
| -rw-r--r-- | after/syntax/idris.vim | 82 | ||||
| -rwxr-xr-x | build | 1 | ||||
| -rw-r--r-- | ftdetect/polyglot.vim | 15 | ||||
| -rw-r--r-- | ftplugin/idris.vim | 346 | ||||
| -rw-r--r-- | indent/idris.vim | 148 | ||||
| -rw-r--r-- | syntax/idris.vim | 93 | ||||
| -rw-r--r-- | syntax/lidris.vim | 26 |
9 files changed, 718 insertions, 1 deletions
@@ -8,7 +8,7 @@ A collection of language packs for Vim. > One to rule them all, one to find them, one to bring them all and in the darkness bind them. - It **won't affect your startup time**, as scripts are loaded only on demand\*. -- It **installs and updates 100+ times faster** than the <!--Package Count-->121<!--/Package Count--> packages it consists of. +- It **installs and updates 100+ times faster** than the <!--Package Count-->122<!--/Package Count--> packages it consists of. - Solid syntax and indentation support (other features skipped). Only the best language packs. - All unnecessary files are ignored (like enormous documentation from php support). - No support for esoteric languages, only most popular ones (modern too, like `slim`). @@ -88,6 +88,7 @@ If you need full functionality of any plugin, please use it directly with your p - [haxe](https://github.com/yaymukund/vim-haxe) (syntax) - [html5](https://github.com/othree/html5.vim) (syntax, indent, autoload, ftplugin) - [i3](https://github.com/mboughaba/i3config.vim) (syntax, ftplugin) +- [idris](https://github.com/idris-hackers/idris-vim) (syntax, indent, ftplugin) - [jasmine](https://github.com/glanotte/vim-jasmine) (syntax) - [javascript](https://github.com/pangloss/vim-javascript) (syntax, indent, compiler, ftplugin, extras) - [jenkins](https://github.com/martinda/Jenkinsfile-vim-syntax) (syntax, indent) diff --git a/after/ftplugin/idris.vim b/after/ftplugin/idris.vim new file mode 100644 index 00000000..ce46b796 --- /dev/null +++ b/after/ftplugin/idris.vim @@ -0,0 +1,5 @@ +if exists('g:polyglot_disabled') && index(g:polyglot_disabled, 'idris') != -1 + finish +endif + +setlocal iskeyword+=' diff --git a/after/syntax/idris.vim b/after/syntax/idris.vim new file mode 100644 index 00000000..bef36f62 --- /dev/null +++ b/after/syntax/idris.vim @@ -0,0 +1,82 @@ +if exists('g:polyglot_disabled') && index(g:polyglot_disabled, 'idris') != -1 + finish +endif + +" This script allows for unicode concealing of certain characters +" For instance -> goes to → +" +" It needs vim >= 7.3, set nocompatible, set enc=utf-8 +" +" If you want to turn this on, let g:idris_conceal = 1 + +if !exists('g:idris_conceal') || !has('conceal') || &enc != 'utf-8' + finish +endif + +" vim: set fenc=utf-8: +syntax match idrNiceOperator "\\\ze[[:alpha:][:space:]_([]" conceal cchar=λ +syntax match idrNiceOperator "<-" conceal cchar=← +syntax match idrNiceOperator "->" conceal cchar=→ +syntax match idrNiceOperator "\<sum\>" conceal cchar=∑ +syntax match idrNiceOperator "\<product\>" conceal cchar=∏ +syntax match idrNiceOperator "\<sqrt\>" conceal cchar=√ +syntax match idrNiceOperator "\<pi\>" conceal cchar=π +syntax match idrNiceOperator "==" conceal cchar=≡ +syntax match idrNiceOperator "\/=" conceal cchar=≠ + + +let s:extraConceal = 1 + +let s:doubleArrow = 1 +" Set this to 0 to use the more technically correct arrow from bar + +" Some windows font don't support some of the characters, +" so if they are the main font, we don't load them :) +if has("win32") + let s:incompleteFont = [ 'Consolas' + \ , 'Lucida Console' + \ , 'Courier New' + \ ] + let s:mainfont = substitute( &guifont, '^\([^:,]\+\).*', '\1', '') + for s:fontName in s:incompleteFont + if s:mainfont ==? s:fontName + let s:extraConceal = 0 + break + endif + endfor +endif + +if s:extraConceal + syntax match idrNiceOperator "Void" conceal cchar=⊥ + + " Match greater than and lower than w/o messing with Kleisli composition + syntax match idrNiceOperator "<=\ze[^<]" conceal cchar=≤ + syntax match idrNiceOperator ">=\ze[^>]" conceal cchar=≥ + + if s:doubleArrow + syntax match idrNiceOperator "=>" conceal cchar=⇒ + else + syntax match idrNiceOperator "=>" conceal cchar=↦ + endif + + syntax match idrNiceOperator "=\zs<<" conceal cchar=« + + syntax match idrNiceOperator "++" conceal cchar=⧺ + syntax match idrNiceOperator "::" conceal cchar=∷ + syntax match idrNiceOperator "-<" conceal cchar=↢ + syntax match idrNiceOperator ">-" conceal cchar=↣ + syntax match idrNiceOperator "-<<" conceal cchar=⤛ + syntax match idrNiceOperator ">>-" conceal cchar=⤜ + + " Only replace the dot, avoid taking spaces around. + syntax match idrNiceOperator /\s\.\s/ms=s+1,me=e-1 conceal cchar=∘ + syntax match idrNiceOperator "\.\." conceal cchar=‥ + + syntax match idrNiceOperator "`elem`" conceal cchar=∈ + syntax match idrNiceOperator "`notElem`" conceal cchar=∉ +endif + +hi link idrNiceOperator Operator +hi! link Conceal Operator +setlocal conceallevel=2 + @@ -196,6 +196,7 @@ PACKS=" haxe:yaymukund/vim-haxe html5:othree/html5.vim i3:mboughaba/i3config.vim + idris:idris-hackers/idris-vim jasmine:glanotte/vim-jasmine javascript:pangloss/vim-javascript:_JAVASCRIPT jenkins:martinda/Jenkinsfile-vim-syntax diff --git a/ftdetect/polyglot.vim b/ftdetect/polyglot.vim index b91c235f..3e6aa32a 100644 --- a/ftdetect/polyglot.vim +++ b/ftdetect/polyglot.vim @@ -479,6 +479,21 @@ aug end augroup end endif +if !exists('g:polyglot_disabled') || index(g:polyglot_disabled, 'idris') == -1 + augroup filetypedetect + " idris, from idris.vim in idris-hackers/idris-vim +au BufNewFile,BufRead *.idr setf idris +au BufNewFile,BufRead idris-response setf idris + augroup end +endif + +if !exists('g:polyglot_disabled') || index(g:polyglot_disabled, 'idris') == -1 + augroup filetypedetect + " idris, from lidris.vim in idris-hackers/idris-vim +au BufNewFile,BufRead *.lidr setf lidris + augroup end +endif + if !exists('g:polyglot_disabled') || index(g:polyglot_disabled, 'jasmine') == -1 augroup filetypedetect " jasmine, from jasmine.vim in glanotte/vim-jasmine diff --git a/ftplugin/idris.vim b/ftplugin/idris.vim new file mode 100644 index 00000000..ce18060d --- /dev/null +++ b/ftplugin/idris.vim @@ -0,0 +1,346 @@ +if exists('g:polyglot_disabled') && index(g:polyglot_disabled, 'idris') != -1 + finish +endif + +if bufname('%') == "idris-response" + finish +endif + +if exists("b:did_ftplugin") + finish +endif + +setlocal shiftwidth=2 +setlocal tabstop=2 +if !exists("g:idris_allow_tabchar") || g:idris_allow_tabchar == 0 + setlocal expandtab +endif +setlocal comments=s1:{-,mb:-,ex:-},:\|\|\|,:-- +setlocal commentstring=--%s +setlocal iskeyword+=? +setlocal wildignore+=*.ibc + +let idris_response = 0 +let b:did_ftplugin = 1 + +" Text near cursor position that needs to be passed to a command. +" Refinment of `expand(<cword>)` to accomodate differences between +" a (n)vim word and what Idris requires. +function! s:currentQueryObject() + let word = expand("<cword>") + if word =~ '^?' + " Cut off '?' that introduces a hole identifier. + let word = strpart(word, 1) + endif + return word +endfunction + +function! s:IdrisCommand(...) + let idriscmd = shellescape(join(a:000)) + return system("idris --client " . idriscmd) +endfunction + +function! IdrisDocFold(lineNum) + let line = getline(a:lineNum) + + if line =~ "^\s*|||" + return "1" + endif + + return "0" +endfunction + +function! IdrisFold(lineNum) + return IdrisDocFold(a:lineNum) +endfunction + +setlocal foldmethod=expr +setlocal foldexpr=IdrisFold(v:lnum) + +function! IdrisResponseWin() + if (!bufexists("idris-response")) + botright 10split + badd idris-response + b idris-response + let g:idris_respwin = "active" + set buftype=nofile + wincmd k + elseif (bufexists("idris-response") && g:idris_respwin == "hidden") + botright 10split + b idris-response + let g:idris_respwin = "active" + wincmd k + endif +endfunction + +function! IdrisHideResponseWin() + let g:idris_respwin = "hidden" +endfunction + +function! IdrisShowResponseWin() + let g:idris_respwin = "active" +endfunction + +function! IWrite(str) + if (bufexists("idris-response")) + let save_cursor = getcurpos() + b idris-response + %delete + let resp = split(a:str, '\n') + call append(1, resp) + b # + call setpos('.', save_cursor) + else + echo a:str + endif +endfunction + +function! IdrisReload(q) + w + let file = expand("%:p") + let tc = s:IdrisCommand(":l", file) + if (! (tc is "")) + call IWrite(tc) + else + if (a:q==0) + echo "Successfully reloaded " . file + call IWrite("") + endif + endif + return tc +endfunction + +function! IdrisReloadToLine(cline) + return IdrisReload(1) + "w + "let file = expand("%:p") + "let tc = s:IdrisCommand(":lto", a:cline, file) + "if (! (tc is "")) + " call IWrite(tc) + "endif + "return tc +endfunction + +function! IdrisShowType() + w + let word = s:currentQueryObject() + let cline = line(".") + let tc = IdrisReloadToLine(cline) + if (! (tc is "")) + echo tc + else + let ty = s:IdrisCommand(":t", word) + call IWrite(ty) + endif + return tc +endfunction + +function! IdrisShowDoc() + w + let word = expand("<cword>") + let ty = s:IdrisCommand(":doc", word) + call IWrite(ty) +endfunction + +function! IdrisProofSearch(hint) + let view = winsaveview() + w + let cline = line(".") + let word = s:currentQueryObject() + let tc = IdrisReload(1) + + if (a:hint==0) + let hints = "" + else + let hints = input ("Hints: ") + endif + + if (tc is "") + let result = s:IdrisCommand(":ps!", cline, word, hints) + if (! (result is "")) + call IWrite(result) + else + e + call winrestview(view) + endif + endif +endfunction + +function! IdrisMakeLemma() + let view = winsaveview() + w + let cline = line(".") + let word = s:currentQueryObject() + let tc = IdrisReload(1) + + if (tc is "") + let result = s:IdrisCommand(":ml!", cline, word) + if (! (result is "")) + call IWrite(result) + else + e + call winrestview(view) + call search(word, "b") + endif + endif +endfunction + +function! IdrisRefine() + let view = winsaveview() + w + let cline = line(".") + let word = expand("<cword>") + let tc = IdrisReload(1) + + let name = input ("Name: ") + + if (tc is "") + let result = s:IdrisCommand(":ref!", cline, word, name) + if (! (result is "")) + call IWrite(result) + else + e + call winrestview(view) + endif + endif +endfunction + +function! IdrisAddMissing() + let view = winsaveview() + w + let cline = line(".") + let word = expand("<cword>") + let tc = IdrisReload(1) + + if (tc is "") + let result = s:IdrisCommand(":am!", cline, word) + if (! (result is "")) + call IWrite(result) + else + e + call winrestview(view) + endif + endif +endfunction + +function! IdrisCaseSplit() + let view = winsaveview() + let cline = line(".") + let word = expand("<cword>") + let tc = IdrisReloadToLine(cline) + + if (tc is "") + let result = s:IdrisCommand(":cs!", cline, word) + if (! (result is "")) + call IWrite(result) + else + e + call winrestview(view) + endif + endif +endfunction + +function! IdrisMakeWith() + let view = winsaveview() + w + let cline = line(".") + let word = s:currentQueryObject() + let tc = IdrisReload(1) + + if (tc is "") + let result = s:IdrisCommand(":mw!", cline, word) + if (! (result is "")) + call IWrite(result) + else + e + call winrestview(view) + call search("_") + endif + endif +endfunction + +function! IdrisMakeCase() + let view = winsaveview() + w + let cline = line(".") + let word = s:currentQueryObject() + let tc = IdrisReload(1) + + if (tc is "") + let result = s:IdrisCommand(":mc!", cline, word) + if (! (result is "")) + call IWrite(result) + else + e + call winrestview(view) + call search("_") + endif + endif +endfunction + +function! IdrisAddClause(proof) + let view = winsaveview() + w + let cline = line(".") + let word = expand("<cword>") + let tc = IdrisReloadToLine(cline) + + if (tc is "") + if (a:proof==0) + let fn = ":ac!" + else + let fn = ":apc!" + endif + + let result = s:IdrisCommand(fn, cline, word) + if (! (result is "")) + call IWrite(result) + else + e + call winrestview(view) + call search(word) + + endif + endif +endfunction + +function! IdrisEval() + w + let tc = IdrisReload(1) + if (tc is "") + let expr = input ("Expression: ") + let result = s:IdrisCommand(expr) + call IWrite(" = " . result) + endif +endfunction + +nnoremap <buffer> <silent> <LocalLeader>t :call IdrisShowType()<ENTER> +nnoremap <buffer> <silent> <LocalLeader>r :call IdrisReload(0)<ENTER> +nnoremap <buffer> <silent> <LocalLeader>c :call IdrisCaseSplit()<ENTER> +nnoremap <buffer> <silent> <LocalLeader>d 0:call search(":")<ENTER>b:call IdrisAddClause(0)<ENTER>w +nnoremap <buffer> <silent> <LocalLeader>b 0:call IdrisAddClause(0)<ENTER> +nnoremap <buffer> <silent> <LocalLeader>m :call IdrisAddMissing()<ENTER> +nnoremap <buffer> <silent> <LocalLeader>md 0:call search(":")<ENTER>b:call IdrisAddClause(1)<ENTER>w +nnoremap <buffer> <silent> <LocalLeader>f :call IdrisRefine()<ENTER> +nnoremap <buffer> <silent> <LocalLeader>o :call IdrisProofSearch(0)<ENTER> +nnoremap <buffer> <silent> <LocalLeader>p :call IdrisProofSearch(1)<ENTER> +nnoremap <buffer> <silent> <LocalLeader>l :call IdrisMakeLemma()<ENTER> +nnoremap <buffer> <silent> <LocalLeader>e :call IdrisEval()<ENTER> +nnoremap <buffer> <silent> <LocalLeader>w 0:call IdrisMakeWith()<ENTER> +nnoremap <buffer> <silent> <LocalLeader>mc :call IdrisMakeCase()<ENTER> +nnoremap <buffer> <silent> <LocalLeader>i 0:call IdrisResponseWin()<ENTER> +nnoremap <buffer> <silent> <LocalLeader>h :call IdrisShowDoc()<ENTER> + +menu Idris.Reload <LocalLeader>r +menu Idris.Show\ Type <LocalLeader>t +menu Idris.Evaluate <LocalLeader>e +menu Idris.-SEP0- : +menu Idris.Add\ Clause <LocalLeader>d +menu Idris.Add\ with <LocalLeader>w +menu Idris.Case\ Split <LocalLeader>c +menu Idris.Add\ missing\ cases <LocalLeader>m +menu Idris.Proof\ Search <LocalLeader>o +menu Idris.Proof\ Search\ with\ hints <LocalLeader>p + +au BufHidden idris-response call IdrisHideResponseWin() +au BufEnter idris-response call IdrisShowResponseWin() diff --git a/indent/idris.vim b/indent/idris.vim new file mode 100644 index 00000000..b7b9015d --- /dev/null +++ b/indent/idris.vim @@ -0,0 +1,148 @@ +if exists('g:polyglot_disabled') && index(g:polyglot_disabled, 'idris') != -1 + finish +endif + +" indentation for idris (idris-lang.org) +" +" Based on haskell indentation by motemen <motemen@gmail.com> +" +" author: raichoo (raichoo@googlemail.com) +" +" Modify g:idris_indent_if and g:idris_indent_case to +" change indentation for `if'(default 3) and `case'(default 5). +" Example (in .vimrc): +" > let g:idris_indent_if = 2 + +if exists('b:did_indent') + finish +endif + +let b:did_indent = 1 + +if !exists('g:idris_indent_if') + " if bool + " >>>then ... + " >>>else ... + let g:idris_indent_if = 3 +endif + +if !exists('g:idris_indent_case') + " case xs of + " >>>>>[] => ... + " >>>>>(y::ys) => ... + let g:idris_indent_case = 5 +endif + +if !exists('g:idris_indent_let') + " let x : Nat = O in + " >>>>x + let g:idris_indent_let = 4 +endif + +if !exists('g:idris_indent_rewrite') + " rewrite prf in expr + " >>>>>>>>x + let g:idris_indent_rewrite = 8 +endif + +if !exists('g:idris_indent_where') + " where f : Nat -> Nat + " >>>>>>f x = x + let g:idris_indent_where = 6 +endif + +if !exists('g:idris_indent_do') + " do x <- a + " >>>y <- b + let g:idris_indent_do = 3 +endif + +setlocal indentexpr=GetIdrisIndent() +setlocal indentkeys=!^F,o,O,} + +function! GetIdrisIndent() + let prevline = getline(v:lnum - 1) + + if prevline =~ '\s\+(\s*.\+\s\+:\s\+.\+\s*)\s\+->\s*$' + return match(prevline, '(') + elseif prevline =~ '\s\+{\s*.\+\s\+:\s\+.\+\s*}\s\+->\s*$' + return match(prevline, '{') + endif + + if prevline =~ '[!#$%&*+./<>?@\\^|~-]\s*$' + let s = match(prevline, '[:=]') + if s > 0 + return s + 2 + else + return match(prevline, '\S') + endif + endif + + if prevline =~ '[{([][^})\]]\+$' + return match(prevline, '[{([]') + endif + + if prevline =~ '\<let\>\s\+.\+\<in\>\s*$' + return match(prevline, '\<let\>') + g:idris_indent_let + endif + + if prevline =~ '\<rewrite\>\s\+.\+\<in\>\s*$' + return match(prevline, '\<rewrite\>') + g:idris_indent_rewrite + endif + + if prevline !~ '\<else\>' + let s = match(prevline, '\<if\>.*\&.*\zs\<then\>') + if s > 0 + return s + endif + + let s = match(prevline, '\<if\>') + if s > 0 + return s + g:idris_indent_if + endif + endif + + if prevline =~ '\(\<where\>\|\<do\>\|=\|[{([]\)\s*$' + return match(prevline, '\S') + &shiftwidth + endif + + if prevline =~ '\<where\>\s\+\S\+.*$' + return match(prevline, '\<where\>') + g:idris_indent_where + endif + + if prevline =~ '\<do\>\s\+\S\+.*$' + return match(prevline, '\<do\>') + g:idris_indent_do + endif + + if prevline =~ '^\s*\<\(co\)\?data\>\s\+[^=]\+\s\+=\s\+\S\+.*$' + return match(prevline, '=') + endif + + if prevline =~ '\<with\>\s\+([^)]*)\s*$' + return match(prevline, '\S') + &shiftwidth + endif + + if prevline =~ '\<case\>\s\+.\+\<of\>\s*$' + return match(prevline, '\<case\>') + g:idris_indent_case + endif + + if prevline =~ '^\s*\(\<namespace\>\|\<\(co\)\?data\>\)\s\+\S\+\s*$' + return match(prevline, '\(\<namespace\>\|\<\(co\)\?data\>\)') + &shiftwidth + endif + + if prevline =~ '^\s*\(\<using\>\|\<parameters\>\)\s*([^(]*)\s*$' + return match(prevline, '\(\<using\>\|\<parameters\>\)') + &shiftwidth + endif + + if prevline =~ '^\s*\<mutual\>\s*$' + return match(prevline, '\<mutual\>') + &shiftwidth + endif + + let line = getline(v:lnum) + + if (line =~ '^\s*}\s*' && prevline !~ '^\s*;') + return match(prevline, '\S') - &shiftwidth + endif + + return match(prevline, '\S') +endfunction diff --git a/syntax/idris.vim b/syntax/idris.vim new file mode 100644 index 00000000..6a86f386 --- /dev/null +++ b/syntax/idris.vim @@ -0,0 +1,93 @@ +if exists('g:polyglot_disabled') && index(g:polyglot_disabled, 'idris') != -1 + finish +endif + +" syntax highlighting for idris (idris-lang.org) +" +" Heavily modified version of the haskell syntax +" highlighter to support idris. +" +" author: raichoo (raichoo@googlemail.com) + +if exists("b:current_syntax") + finish +endif + +syn match idrisTypeDecl "[a-zA-Z][a-zA-z0-9_']*\s\+:\s\+" + \ contains=idrisIdentifier,idrisOperators +syn region idrisParens matchgroup=idrisDelimiter start="(" end=")" contains=TOP,idrisTypeDecl +syn region idrisBrackets matchgroup=idrisDelimiter start="\[" end="]" contains=TOP,idrisTypeDecl +syn region idrisBlock matchgroup=idrisDelimiter start="{" end="}" contains=TOP,idrisTypeDecl +syn keyword idrisModule module namespace +syn keyword idrisImport import +syn keyword idrisRefl refl +syn keyword idrisDeprecated class instance +syn keyword idrisStructure codata data record dsl interface implementation +syn keyword idrisWhere where +syn keyword idrisVisibility public abstract private export +syn keyword idrisBlock parameters mutual postulate using +syn keyword idrisTotality total partial covering +syn keyword idrisImplicit implicit +syn keyword idrisAnnotation auto impossible static constructor +syn keyword idrisStatement do case of rewrite with proof +syn keyword idrisLet let in +syn match idrisSyntax "\(pattern \+\|term \+\)\?syntax" +syn keyword idrisConditional if then else +syn match idrisTactic contained "\<\(intros\?\|rewrite\|exact\|refine\|trivial\|let\|focus\|try\|compute\|solve\|attack\|reflect\|fill\|applyTactic\)\>" +syn match idrisNumber "\<[0-9]\+\>\|\<0[xX][0-9a-fA-F]\+\>\|\<0[oO][0-7]\+\>" +syn match idrisFloat "\<[0-9]\+\.[0-9]\+\([eE][-+]\=[0-9]\+\)\=\>" +syn match idrisDelimiter "[,;]" +syn keyword idrisInfix prefix infix infixl infixr +syn match idrisOperators "\([-!#$%&\*\+./<=>\?@\\^|~:]\|\<_\>\)" +syn match idrisType "\<[A-Z][a-zA-Z0-9_']*\>" +syn keyword idrisTodo TODO FIXME XXX HACK contained +syn match idrisLineComment "---*\([^-!#$%&\*\+./<=>\?@\\^|~].*\)\?$" contains=idrisTodo,@Spell +syn match idrisDocComment "|||\([^-!#$%&\*\+./<=>\?@\\^|~].*\)\?$" contains=idrisTodo,@Spell +syn match idrisMetaVar "?[a-z][A-Za-z0-9_']*" +syn match idrisLink "%\(lib\|link\|include\)" +syn match idrisDirective "%\(access\|assert_total\|default\|elim\|error_reverse\|hide\|name\|reflection\|error_handlers\|language\|flag\|dynamic\|provide\|inline\|used\|no_implicit\|hint\|extern\|unqualified\|error_handler\)" +syn keyword idrisDSL lambda variable index_first index_next +syn match idrisChar "'[^'\\]'\|'\\.'\|'\\u[0-9a-fA-F]\{4}'" +syn match idrisBacktick "`[A-Za-z][A-Za-z0-9_']*`" +syn region idrisString start=+"+ skip=+\\\\\|\\"+ end=+"+ contains=@Spell +syn region idrisBlockComment start="{-" end="-}" contains=idrisBlockComment,idrisTodo,@Spell +syn region idrisProofBlock start="\(default\s\+\)\?\(proof\|tactics\) *{" end="}" contains=idrisTactic +syn match idrisIdentifier "[a-zA-Z][a-zA-z0-9_']*" contained + +highlight def link idrisDeprecated Error +highlight def link idrisIdentifier Identifier +highlight def link idrisImport Structure +highlight def link idrisModule Structure +highlight def link idrisStructure Structure +highlight def link idrisStatement Statement +highlight def link idrisDSL Statement +highlight def link idrisBlock Statement +highlight def link idrisAnnotation Statement +highlight def link idrisWhere Structure +highlight def link idrisLet Structure +highlight def link idrisTotality Statement +highlight def link idrisImplicit Statement +highlight def link idrisSyntax Statement +highlight def link idrisVisibility Statement +highlight def link idrisConditional Conditional +highlight def link idrisProofBlock Macro +highlight def link idrisRefl Macro +highlight def link idrisTactic Identifier +highlight def link idrisLink Statement +highlight def link idrisDirective Statement +highlight def link idrisNumber Number +highlight def link idrisFloat Float +highlight def link idrisDelimiter Delimiter +highlight def link idrisInfix PreProc +highlight def link idrisOperators Operator +highlight def link idrisType Include +highlight def link idrisDocComment Comment +highlight def link idrisLineComment Comment +highlight def link idrisBlockComment Comment +highlight def link idrisTodo Todo +highlight def link idrisMetaVar Macro +highlight def link idrisString String +highlight def link idrisChar String +highlight def link idrisBacktick Operator + +let b:current_syntax = "idris" diff --git a/syntax/lidris.vim b/syntax/lidris.vim new file mode 100644 index 00000000..d4e55efb --- /dev/null +++ b/syntax/lidris.vim @@ -0,0 +1,26 @@ +if exists('g:polyglot_disabled') && index(g:polyglot_disabled, 'idris') != -1 + finish +endif + +" Vim syntax file +" Language: Literate Idris +" Maintainer: Idris Hackers (https://github.com/idris-hackers/idris-vim) +" Last Change: 2014 Mar 4 +" Version: 0.1 +" +" This is just a minimal adaption of the Literate Haskell syntax file. + + +" Read Idris highlighting. +if version < 600 + syntax include @idrisTop <sfile>:p:h/idris.vim +else + syntax include @idrisTop syntax/idris.vim +endif + +" Recognize blocks of Bird tracks, highlight as Idris. +syntax region lidrisBirdTrackBlock start="^>" end="\%(^[^>]\)\@=" contains=@idrisTop,lidrisBirdTrack +syntax match lidrisBirdTrack "^>" contained +hi def link lidrisBirdTrack Comment + +let b:current_syntax = "lidris" |