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

fix refine command

Browse source
This commit is contained in:
rhiannon morris 2023-05-27 16:22:20 +02:00
parent ad08ee24f5
commit 518e5f0c41
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
ftplugin/idris2.vim
View file

@ -190,10 +190,10 @@ function! IdrisRefine()
let view = winsaveview() let view = winsaveview()
w w
let cline = line(".") let cline = line(".")
let word = expand("<cword>") let word = s:currentQueryObject()
let name = input ("Name: ") let name = input ("Name: ")
let result = s:IdrisCommand(":ref!", cline, word, name) let result = s:IdrisCommand(":refine!", cline, word, name)
if (! (result is "")) if (! (result is ""))
call IWrite(result) call IWrite(result)
else else