Minimal changes necessary for having an async Agda process

[dolio]

• 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.

[dolio]

Yo. I'm not sure this is completely ready to be merged, but I thought I'd create the pull request to spark discussion. It's the bare minimum of what it takes to make this plugin asynchronous but still work. Here are some discussion points:

1. I just wrapped the job send into python and left most of the logic, but some of it might live more naturally in the Vim job file.
2. Agda can send JSON instead of lisp responses, and Vim can easily parse those into dictionaries for us. Should this plugin move to that? I imagine most other front ends that people are playing with will be using the JSON interaction.
   • This probably raises a sub-question of how committed you are to supporting the old Agda versions in some of the version checks. I think the JSON was at least 2.5+.
3. If stuff has to be rewritten to use structured dictionaries from JSON, should it be written in python again? I'm not sure it would be much worse to use viml at this point, and then there wouldn't have to be as much weird marshalling of stuff by parsing and formatting strings.

[dolio]

Oh, one thing I didn't do yet (and why it probably shouldn't be merged) is set up any kind of 'command running' mutex like the emacs mode has. That'd probably make for a better way of figuring out when to reload highlighting. Right now you can send commands to agda while it's still working on the previous one. I haven't thought through how things should work, though, since the response interpreter sends some of its own commands right now.

[ghost]

I’m implementing a vim plugin for agda too.
https://github.com/ray851107/vim-agda-async
It uses the json api and is written in pure vim script. The author of json api told me that the DisplayInfo part of the api may be removed in the next version, though.

[dolio]

@ray851107 I see. In that case I won't duplicate work, since that's the sort of implementation I would probably aim toward personally.

I'm a little confused about the DisplayInfo thing, though. If I log JSON messages those always seem to have null information. Is that the only thing that's going away?

[ghost]

@dolio In the latest release (v2.6.0.1) it returns warnings, error messages etc.
https://github.com/agda/agda/blob/48c9d8fe35adca8c2e309bf64e99b26b25a90169/src/full/Agda/Interaction/JSONTop.hs#L48

In current master it always returns null.
https://github.com/agda/agda/blob/a09aa4e3e343bb48be60d6cdfce4c85a0f8d39d3/src/full/Agda/Interaction/JSONTop.hs#L45