Minimal changes necessary for having an async Agda process

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

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

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('<sfile>: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 <buffer> <LocalLeader>l :AgdaReload<CR>
+nnoremap <buffer> <LocalLeader>l :AgdaLoad<CR>
 nnoremap <buffer> <LocalLeader>t :call AgdaInfer()<CR>
 nnoremap <buffer> <LocalLeader>r :call AgdaRefine("False")<CR>
 nnoremap <buffer> <LocalLeader>R :call AgdaRefine("True")<CR>
@@ -275,7 +281,8 @@ inoremap <buffer> <silent> <C-g>  <C-o>:let _s=@/<CR><C-o>/ {!\\| ?<CR><C-o>:let
 nnoremap <buffer> <silent> <C-y>  2h:let _s=@/<CR>? {!\\| \?<CR>:let @/=_s<CR>2l
 inoremap <buffer> <silent> <C-y>  <C-o>2h<C-o>:let _s=@/<CR><C-o>? {!\\| \?<CR><C-o>:let @/=_s<CR><C-o>2l
 
-AgdaReload
+" AgdaReload
+AgdaVersion
 
 endif