Compare commits
4 Commits
518e5f0c41
...
1cb34ab5d6
Author | SHA1 | Date |
---|---|---|
rhiannon morris | 1cb34ab5d6 | |
rhiannon morris | 504979fe07 | |
rhiannon morris | 9c35464b69 | |
rhiannon morris | 2c89714506 |
|
@ -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()
|
||||
|
|
Loading…
Reference in New Issue