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

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("<cword>")
-
-  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("<cword>")
 
-  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
 
@@ -292,41 +259,32 @@ function! IdrisEval()
   w
   let expr = input ("Expression: ")
   let result = s:IdrisCommand(expr)
-  call IWrite(" = " . result)
+  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 <buffer> <silent> <LocalLeader>t :call IdrisShowType(0)<ENTER>
 nnoremap <buffer> <silent> <LocalLeader>T :call IdrisShowType(1)<ENTER>
 nnoremap <buffer> <silent> <LocalLeader>r :call IdrisReload(0)<ENTER>
 nnoremap <buffer> <silent> <LocalLeader>c :call IdrisCaseSplit()<ENTER>
-nnoremap <buffer> <silent> <LocalLeader>a 0:call search(":")<ENTER>b:call IdrisAddClause(0)<ENTER>w
-nnoremap <buffer> <silent> <LocalLeader>d 0:call search(":")<ENTER>b:call IdrisAddClause(0)<ENTER>w
-nnoremap <buffer> <silent> <LocalLeader>b 0:call IdrisAddClause(0)<ENTER>
-nnoremap <buffer> <silent> <LocalLeader>m :call IdrisAddMissing()<ENTER>
-nnoremap <buffer> <silent> <LocalLeader>md 0:call search(":")<ENTER>b:call IdrisAddClause(1)<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>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>g :call IdrisGenerateDef()<ENTER>
 nnoremap <buffer> <silent> <LocalLeader>l :call IdrisMakeLemma()<ENTER>
 nnoremap <buffer> <silent> <LocalLeader>e :call IdrisEval()<ENTER>
 nnoremap <buffer> <silent> <LocalLeader>w 0:call IdrisMakeWith()<ENTER>
 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
+nnoremap <buffer> <silent> <LocalLeader>s :call IdrisSearch()<ENTER>
 
 au BufHidden idris-response call IdrisHideResponseWin()
 au BufEnter idris-response call IdrisShowResponseWin()