diff --git a/ftplugin/idris2.vim b/ftplugin/idris2.vim index 22aa93f..9a5b1e5 100644 --- a/ftplugin/idris2.vim +++ b/ftplugin/idris2.vim @@ -262,6 +262,13 @@ function! IdrisEval() 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 t :call IdrisShowType(0) nnoremap T :call IdrisShowType(1) nnoremap r :call IdrisReload(0) @@ -269,15 +276,15 @@ nnoremap c :call IdrisCaseSplit() nnoremap a 0:call search(":")b:call IdrisAddClause()w nnoremap f :call IdrisRefine() nnoremap o :call IdrisProofSearch(0) -nnoremap s :call IdrisProofSearch(0) -nnoremap g :call IdrisGenerateDef() nnoremap p :call IdrisProofSearch(1) +nnoremap g :call IdrisGenerateDef() nnoremap l :call IdrisMakeLemma() nnoremap e :call IdrisEval() nnoremap w 0:call IdrisMakeWith() nnoremap mc :call IdrisMakeCase() nnoremap i 0:call IdrisResponseWin() nnoremap h :call IdrisShowDoc() +nnoremap s :call IdrisSearch() au BufHidden idris-response call IdrisHideResponseWin() au BufEnter idris-response call IdrisShowResponseWin()