From ad1f389de60ac83e6210230bb54e3311992b5fd4 Mon Sep 17 00:00:00 2001 From: Dan Doel Date: Sat, 24 Aug 2019 10:12:29 -0400 Subject: [PATCH] Minimal changes necessary for having an async Agda process - An autoload script manages the job with vim's async job control - The function to send commands to the process is wrapped into python - The response interpreter becomes a callback that runs as Agda sends output - The `Agda>` prompt is used as a trigger for loading highlighting files, since there is no longer an obvious synchronous point for doing so. --- agda.py | 28 +++---------- autoload/agda/job.vim | 96 +++++++++++++++++++++++++++++++++++++++++++ ftplugin/agda.vim | 21 ++++++---- 3 files changed, 116 insertions(+), 29 deletions(-) create mode 100644 autoload/agda/job.vim diff --git a/agda.py b/agda.py index 9ac0c29..8f47406 100644 --- a/agda.py +++ b/agda.py @@ -59,11 +59,6 @@ def vim_bool(s): return True return bool(int(s)) - -# start Agda -# TODO: I'm pretty sure this will start an agda process per buffer which is less than desirable... -agda = subprocess.Popen(["agda", "--interaction"], bufsize = 1, stdin = subprocess.PIPE, stdout = subprocess.PIPE, universal_newlines = True) - goals = {} annotations = [] @@ -93,10 +88,6 @@ def promptUser(msg): vim.command('call inputrestore()') return result -def AgdaRestart(): - global agda - agda = subprocess.Popen(["agda", "--interaction"], bufsize = 1, stdin = subprocess.PIPE, stdout = subprocess.PIPE, universal_newlines = True) - def findGoals(goalList): global goals @@ -264,12 +255,13 @@ def interpretResponse(responses, quiet = False): else: pass # print(response) +@vim_func +def AgdaInterpretResponse(responses, quiet = False): + interpretResponse(responses, False) + def sendCommand(arg, quiet=False): - vim.command('silent! write') - f = vim.current.buffer.name - # The x is a really hacky way of getting a consistent final response. Namely, "cannot read" - agda.stdin.write('IOTCM "%s" None Direct (%s)\nx\n' % (escape(f), arg)) - interpretResponse(getOutput(), quiet) + cmd = 'call agda#job#send(\'%s\',%s)' % (arg, '1' if quiet else '0') + vim.command(cmd) def sendCommandLoadHighlightInfo(file, quiet): sendCommand('Cmd_load_highlighting_info "%s"' % escape(file), quiet = quiet) @@ -340,14 +332,6 @@ def AgdaVersion(quiet): sendCommand('Cmd_show_version', quiet=quiet) -@vim_func(conv={'quiet': vim_bool}) -def AgdaLoad(quiet): - f = vim.current.buffer.name - sendCommandLoad(f, quiet) - if vim.vars['agdavim_enable_goto_definition']: - sendCommandLoadHighlightInfo(f, quiet) - - @vim_func(conv={'quiet': vim_bool}) def AgdaLoadHighlightInfo(quiet): f = vim.current.buffer.name diff --git a/autoload/agda/job.vim b/autoload/agda/job.vim new file mode 100644 index 0000000..0bb7b82 --- /dev/null +++ b/autoload/agda/job.vim @@ -0,0 +1,96 @@ +let s:agda_version = [0,0,0,0] + +let s:quiet = v:false + +function! agda#job#set_version(version) + let s:agda_version = a:version +endfunction + +" define a common interface to differing vim/nvim job control +if has('nvim') + function! s:interp(on_out, job, dat, ...) + for l:line in a:dat + if l:line =~ 'Agda2>.*' + call AgdaReloadSyntax() + endif + endfor + call a:on_out(a:dat, s:quiet) + endfunction + + function! s:job_start(cmd, on_out) + let l:opts = {} + let l:opts.on_stdout = function('s:interp', [a:on_out]) + let l:opts.on_stderr = function('s:interp', [a:on_out]) + + let s:job = jobstart(a:cmd, l:opts) + return s:job + endfunction + + function! s:job_send(txt) + call jobsend(s:job, a:txt) + endfunction + +else " vim 8 + function! s:interp(on_out, job, dat, ...) + call a:on_out([a:dat], s:quiet) + endfunction + function! s:job_start(cmd, on_out) + let l:opts = {} + let l:opts.callback = function('s:interp', [a:on_out]) + + let s:job = job_start(a:cmd, l:opts) + if job_status(s:job) == 'fail' + return -1 + else + return 1 + endif + endfunction + + function! s:job_send(txt) + call ch_sendraw(job_getchannel(s:job), a:txt) + endfunction +endif + +function! agda#job#start(interp) + if exists('s:job') + echom 'Agda already started' + return + endif + + let l:result = s:job_start(['agda', '--interaction', '--vim'], a:interp) + + if l:result == -1 + echom 'Failed to start agda' + elseif l:result == 0 + echom 'agda#job#start: invalid arguments' + endif +endfunction + +function! s:escape(arg) + return escape(a:arg, "\n\r\\'\"\t") +endfunction + +function! agda#job#send(arg, quiet) + let s:quiet = a:quiet + if !exists('s:job') + echom 'Agda not started' + return + end + silent! write + let l:file = s:escape(expand('%')) + let l:cmd = printf('IOTCM "%s" None Direct (%s)' . "\n", l:file, a:arg) + call s:job_send(l:cmd) +endfunction + +function! agda#job#sendLoadHighlightInfo(file, quiet) + let l:cmd = printf('Cmd_load_highlighting_info "%s"', s:escape(a:file)) + call agda#job#send(l:cmd, a:quiet) +endfunction + +function! agda#job#sendLoad(file, quiet) + " Pre 2.5 + " l:incpaths_str = join(g:agdavim_agda_includepathlist, ',') + let l:incpaths_str = '"-i",' . join(g:agdavim_agda_includepathlist, ',"-i",') + let l:cmd = printf('Cmd_load "%s" [%s]', s:escape(a:file), l:incpaths_str) + call agda#job#send(l:cmd, a:quiet) +endfunction diff --git a/ftplugin/agda.vim b/ftplugin/agda.vim index 9af172e..ca94a88 100644 --- a/ftplugin/agda.vim +++ b/ftplugin/agda.vim @@ -21,10 +21,6 @@ function! AgdaReloadSyntax() endfunction call AgdaReloadSyntax() -function! AgdaLoad(quiet) - " Do nothing. Overidden below with a Python function if python is supported. -endfunction - autocmd QuickfixCmdPost make call AgdaReloadSyntax()|call AgdaVersion(v:true)|call AgdaLoad(v:true) setlocal autowrite @@ -229,9 +225,19 @@ endfunction execute s:python_loadfile . resolve(expand(':p:h') . '/../agda.py') +call agda#job#start(function('AgdaInterpretResponse')) + +function! AgdaLoad(quiet) + let l:bufname = expand('%') + call agda#job#sendLoad(l:bufname, a:quiet) + if g:agdavim_enable_goto_definition + call agda#job#sendLoadHighlightInfo(l:bufname, a:quiet) + endif +endfunction + command! -buffer -nargs=0 AgdaLoad call AgdaLoad(v:false) command! -buffer -nargs=0 AgdaVersion call AgdaVersion(v:false) -command! -buffer -nargs=0 AgdaReload silent! make!|redraw! +" command! -buffer -nargs=0 AgdaReload silent! make!|redraw! command! -buffer -nargs=0 AgdaRestartAgda exec s:python_cmd 'RestartAgda()' command! -buffer -nargs=0 AgdaShowImplicitArguments exec s:python_cmd "sendCommand('ShowImplicitArgs True')" command! -buffer -nargs=0 AgdaHideImplicitArguments exec s:python_cmd "sendCommand('ShowImplicitArgs False')" @@ -248,7 +254,7 @@ command! -buffer -nargs=0 AgdaSetRewriteModeSimplified exec s:python_cmd "setRew command! -buffer -nargs=0 AgdaSetRewriteModeHeadNormal exec s:python_cmd "setRewriteMode('HeadNormal')" command! -buffer -nargs=0 AgdaSetRewriteModeInstantiated exec s:python_cmd "setRewriteMode('Instantiated')" -nnoremap l :AgdaReload +nnoremap l :AgdaLoad nnoremap t :call AgdaInfer() nnoremap r :call AgdaRefine("False") nnoremap R :call AgdaRefine("True") @@ -275,7 +281,8 @@ inoremap :let _s=@// {!\\| ?:let nnoremap 2h:let _s=@/? {!\\| \?:let @/=_s2l inoremap 2h:let _s=@/? {!\\| \?:let @/=_s2l -AgdaReload +" AgdaReload +AgdaVersion endif