291 lines
6.8 KiB
VimL
291 lines
6.8 KiB
VimL
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))
|
|
" Vim does not support ANSI escape codes natively, so we need to disable
|
|
" automatic colouring
|
|
return system("idris2 --no-color --find-ipkg " . shellescape(expand('%:p')) . " --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"
|
|
setlocal buftype=nofile bufhidden=hide noswapfile
|
|
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)
|
|
let view = winsaveview()
|
|
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
|
|
call winrestview(view)
|
|
endfunction
|
|
|
|
function! IdrisReload(q)
|
|
w
|
|
let file = expand('%:p')
|
|
let tc = system("idris2 --no-color --find-ipkg " . shellescape(file) . " --client ''")
|
|
if (! (tc is ""))
|
|
call IWrite(tc)
|
|
elseif (a:q==0)
|
|
call IWrite("Successfully reloaded " . file)
|
|
endif
|
|
return tc
|
|
endfunction
|
|
|
|
function! IdrisShowType(imp)
|
|
w
|
|
let word = s:currentQueryObject()
|
|
let cline = line(".")
|
|
let ccol = col(".")
|
|
let ty = s:IdrisCommand(a:imp ? ":ti" : ":t", word)
|
|
call IWrite(ty)
|
|
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()
|
|
|
|
if (a:hint==0)
|
|
let hints = ""
|
|
else
|
|
let hints = input ("Hints: ")
|
|
endif
|
|
|
|
let result = s:IdrisCommand(":ps!", cline, word, hints)
|
|
if (! (result is ""))
|
|
call IWrite(result)
|
|
else
|
|
e
|
|
call winrestview(view)
|
|
endif
|
|
endfunction
|
|
|
|
function! IdrisGenerateDef()
|
|
let view = winsaveview()
|
|
w
|
|
let cline = line(".")
|
|
let word = s:currentQueryObject()
|
|
|
|
let result = s:IdrisCommand(":gd!", cline, word)
|
|
if (! (result is ""))
|
|
call IWrite(result)
|
|
else
|
|
e
|
|
call winrestview(view)
|
|
endif
|
|
endfunction
|
|
|
|
function! IdrisMakeLemma()
|
|
let view = winsaveview()
|
|
w
|
|
let cline = line(".")
|
|
let word = s:currentQueryObject()
|
|
|
|
let result = s:IdrisCommand(":ml!", cline, word)
|
|
if (! (result is ""))
|
|
call IWrite(result)
|
|
else
|
|
e
|
|
call winrestview(view)
|
|
call search(word, "b")
|
|
endif
|
|
endfunction
|
|
|
|
function! IdrisRefine()
|
|
let view = winsaveview()
|
|
w
|
|
let cline = line(".")
|
|
let word = s:currentQueryObject()
|
|
let name = input ("Name: ")
|
|
|
|
let result = s:IdrisCommand(":refine!", cline, word, name)
|
|
if (! (result is ""))
|
|
call IWrite(result)
|
|
else
|
|
e
|
|
call winrestview(view)
|
|
endif
|
|
endfunction
|
|
|
|
function! IdrisCaseSplit()
|
|
w
|
|
let view = winsaveview()
|
|
let cline = line(".")
|
|
let ccol = col(".")
|
|
let word = expand("<cword>")
|
|
let result = s:IdrisCommand(":cs!", cline, ccol, word)
|
|
if (! (result is ""))
|
|
call IWrite(result)
|
|
else
|
|
e
|
|
call winrestview(view)
|
|
endif
|
|
endfunction
|
|
|
|
function! IdrisMakeWith()
|
|
let view = winsaveview()
|
|
w
|
|
let cline = line(".")
|
|
let word = s:currentQueryObject()
|
|
let tc = IdrisReload(1)
|
|
|
|
let result = s:IdrisCommand(":mw!", cline, word)
|
|
if (! (result is ""))
|
|
call IWrite(result)
|
|
else
|
|
e
|
|
call winrestview(view)
|
|
call search("_")
|
|
endif
|
|
endfunction
|
|
|
|
function! IdrisMakeCase()
|
|
let view = winsaveview()
|
|
w
|
|
let cline = line(".")
|
|
let word = s:currentQueryObject()
|
|
|
|
let result = s:IdrisCommand(":mc!", cline, word)
|
|
if (! (result is ""))
|
|
call IWrite(result)
|
|
else
|
|
e
|
|
call winrestview(view)
|
|
call search("_")
|
|
endif
|
|
endfunction
|
|
|
|
function! IdrisAddClause()
|
|
let view = winsaveview()
|
|
w
|
|
let cline = line(".")
|
|
let word = expand("<cword>")
|
|
|
|
let result = s:IdrisCommand(":ac!", cline, word)
|
|
if (! (result is ""))
|
|
call IWrite(result)
|
|
else
|
|
e
|
|
call winrestview(view)
|
|
call search(word)
|
|
endif
|
|
endfunction
|
|
|
|
function! IdrisEval()
|
|
w
|
|
let expr = input ("Expression: ")
|
|
let result = s:IdrisCommand(expr)
|
|
call IWrite(expr . " =\n" . result)
|
|
endfunction
|
|
|
|
function! IdrisSearch()
|
|
w
|
|
let expr = input ("Partial type: ")
|
|
let result = s:IdrisCommand(":fs", expr)
|
|
call IWrite(result)
|
|
endfunction
|
|
|
|
nnoremap <buffer> <silent> <LocalLeader>t :call IdrisShowType(0)<ENTER>
|
|
nnoremap <buffer> <silent> <LocalLeader>T :call IdrisShowType(1)<ENTER>
|
|
nnoremap <buffer> <silent> <LocalLeader>r :call IdrisReload(0)<ENTER>
|
|
nnoremap <buffer> <silent> <LocalLeader>c :call IdrisCaseSplit()<ENTER>
|
|
nnoremap <buffer> <silent> <LocalLeader>a 0:call search(":")<ENTER>b:call IdrisAddClause()<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>g :call IdrisGenerateDef()<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>
|
|
nnoremap <buffer> <silent> <LocalLeader>s :call IdrisSearch()<ENTER>
|
|
|
|
au BufHidden idris-response call IdrisHideResponseWin()
|
|
au BufEnter idris-response call IdrisShowResponseWin()
|