rhi/idris2-vim
1
0
Fork 0
Code Issues Pull requests Releases Activity

add type search on \s (since proof search is ALSO \o)

Browse source
This commit is contained in:
rhiannon morris 2023-05-28 14:45:18 +02:00
parent 504979fe07
commit 1cb34ab5d6
1 changed files with 9 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
ftplugin/idris2.vim
View file

@ -262,6 +262,13 @@ function! IdrisEval()
call IWrite(expr . " =\n" . result) call IWrite(expr . " =\n" . result)
endfunction 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(0)<ENTER>
nnoremap <buffer> <silent> <LocalLeader>T :call IdrisShowType(1)<ENTER> nnoremap <buffer> <silent> <LocalLeader>T :call IdrisShowType(1)<ENTER>
nnoremap <buffer> <silent> <LocalLeader>r :call IdrisReload(0)<ENTER> nnoremap <buffer> <silent> <LocalLeader>r :call IdrisReload(0)<ENTER>
@ -269,15 +276,15 @@ 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>a 0:call search(":")<ENTER>b:call IdrisAddClause()<ENTER>w
nnoremap <buffer> <silent> <LocalLeader>f :call IdrisRefine()<ENTER> nnoremap <buffer> <silent> <LocalLeader>f :call IdrisRefine()<ENTER>
nnoremap <buffer> <silent> <LocalLeader>o :call IdrisProofSearch(0)<ENTER> nnoremap <buffer> <silent> <LocalLeader>o :call IdrisProofSearch(0)<ENTER>
nnoremap <buffer> <silent> <LocalLeader>s :call IdrisProofSearch(0)<ENTER>
nnoremap <buffer> <silent> <LocalLeader>g :call IdrisGenerateDef()<ENTER>
nnoremap <buffer> <silent> <LocalLeader>p :call IdrisProofSearch(1)<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>l :call IdrisMakeLemma()<ENTER>
nnoremap <buffer> <silent> <LocalLeader>e :call IdrisEval()<ENTER> nnoremap <buffer> <silent> <LocalLeader>e :call IdrisEval()<ENTER>
nnoremap <buffer> <silent> <LocalLeader>w 0:call IdrisMakeWith()<ENTER> nnoremap <buffer> <silent> <LocalLeader>w 0:call IdrisMakeWith()<ENTER>
nnoremap <buffer> <silent> <LocalLeader>mc :call IdrisMakeCase()<ENTER> nnoremap <buffer> <silent> <LocalLeader>mc :call IdrisMakeCase()<ENTER>
nnoremap <buffer> <silent> <LocalLeader>i 0:call IdrisResponseWin()<ENTER> nnoremap <buffer> <silent> <LocalLeader>i 0:call IdrisResponseWin()<ENTER>
nnoremap <buffer> <silent> <LocalLeader>h :call IdrisShowDoc()<ENTER> nnoremap <buffer> <silent> <LocalLeader>h :call IdrisShowDoc()<ENTER>
nnoremap <buffer> <silent> <LocalLeader>s :call IdrisSearch()<ENTER>
au BufHidden idris-response call IdrisHideResponseWin() au BufHidden idris-response call IdrisHideResponseWin()
au BufEnter idris-response call IdrisShowResponseWin() au BufEnter idris-response call IdrisShowResponseWin()