diff --git a/ftplugin/idris2.vim b/ftplugin/idris2.vim index ed5287a..b7617f7 100644 --- a/ftplugin/idris2.vim +++ b/ftplugin/idris2.vim @@ -107,17 +107,6 @@ function! IdrisReload(q) 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(imp) w let word = s:currentQueryObject() @@ -202,21 +191,6 @@ function! IdrisRefine() endif endfunction -function! IdrisAddMissing() - let view = winsaveview() - w - let cline = line(".") - let word = expand("") - - let result = s:IdrisCommand(":am!", cline, word) - if (! (result is "")) - call IWrite(result) - else - e - call winrestview(view) - endif -endfunction - function! IdrisCaseSplit() w let view = winsaveview() @@ -265,26 +239,19 @@ function! IdrisMakeCase() endif endfunction -function! IdrisAddClause(proof) +function! IdrisAddClause() let view = winsaveview() w let cline = line(".") let word = expand("") - if (a:proof==0) - let fn = ":ac!" - else - let fn = ":apc!" - endif - - let result = s:IdrisCommand(fn, cline, word) + let result = s:IdrisCommand(":ac!", cline, word) if (! (result is "")) call IWrite(result) else e call winrestview(view) call search(word) - endif endfunction @@ -299,11 +266,7 @@ nnoremap t :call IdrisShowType(0) nnoremap T :call IdrisShowType(1) nnoremap r :call IdrisReload(0) nnoremap c :call IdrisCaseSplit() -nnoremap a 0:call search(":")b:call IdrisAddClause(0)w -nnoremap d 0:call search(":")b:call IdrisAddClause(0)w -nnoremap b 0:call IdrisAddClause(0) -nnoremap m :call IdrisAddMissing() -nnoremap md 0:call search(":")b:call IdrisAddClause(1)w +nnoremap a 0:call search(":")b:call IdrisAddClause()w nnoremap f :call IdrisRefine() nnoremap o :call IdrisProofSearch(0) nnoremap s :call IdrisProofSearch(0)