Add idris support, closes #265
This commit is contained in:
Adam Stankiewicz
parent
0cd0b7f894
commit
63922a1d1e
@ -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)
|
||||
|
||||
5
after/ftplugin/idris.vim
Normal file
5
after/ftplugin/idris.vim
Normal file
@ -0,0 +1,5 @@
|
||||
if exists('g:polyglot_disabled') && index(g:polyglot_disabled, 'idris') != -1
|
||||
finish
|
||||
endif
|
||||
|
||||
setlocal iskeyword+='
|
||||
82
after/syntax/idris.vim
Normal file
82
after/syntax/idris.vim
Normal file
@ -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
|
||||
|
||||
1
build
1
build
@ -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
|
||||
|
||||
@ -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
|
||||
|
||||
346
ftplugin/idris.vim
Normal file
346
ftplugin/idris.vim
Normal file
@ -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()
|
||||
148
indent/idris.vim
Normal file
148
indent/idris.vim
Normal file
@ -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
|
||||
93
syntax/idris.vim
Normal file
93
syntax/idris.vim
Normal file
@ -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"
|
||||
26
syntax/lidris.vim
Normal file
26
syntax/lidris.vim
Normal file
@ -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"
|
||||
Loading…
Reference in New Issue
Block a user