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

remove menu bar stuff

This commit is contained in:
rhiannon morris 2023-05-28 14:44:41 +02:00
parent 9c35464b69
commit 504979fe07
1 changed files with 0 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
ftplugin/idris2.vim
View File

@ -279,17 +279,5 @@ 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>a
menu Idris.Generate\ Definition <LocalLeader>g
menu Idris.Add\ with <LocalLeader>w
menu Idris.Case\ Split <LocalLeader>c
menu Idris.Add\ missing\ cases <LocalLeader>m
menu Idris.Proof\ Search <LocalLeader>s
menu Idris.Proof\ Search\ with\ hints <LocalLeader>p
au BufHidden idris-response call IdrisHideResponseWin()
au BufEnter idris-response call IdrisShowResponseWin()