From 504979fe076f4e612b4dbe5f870d7d29b1e8f687 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Sun, 28 May 2023 14:44:41 +0200 Subject: [PATCH] remove menu bar stuff --- ftplugin/idris2.vim | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/ftplugin/idris2.vim b/ftplugin/idris2.vim index 5cd15e9..22aa93f 100644 --- a/ftplugin/idris2.vim +++ b/ftplugin/idris2.vim @@ -279,17 +279,5 @@ nnoremap mc :call IdrisMakeCase() nnoremap i 0:call IdrisResponseWin() nnoremap h :call IdrisShowDoc() -menu Idris.Reload r -menu Idris.Show\ Type t -menu Idris.Evaluate e -menu Idris.-SEP0- : -menu Idris.Add\ Clause a -menu Idris.Generate\ Definition g -menu Idris.Add\ with w -menu Idris.Case\ Split c -menu Idris.Add\ missing\ cases m -menu Idris.Proof\ Search s -menu Idris.Proof\ Search\ with\ hints p - au BufHidden idris-response call IdrisHideResponseWin() au BufEnter idris-response call IdrisShowResponseWin()