Sandy Maguire

Cmd_give lets agda update its internal state without requiring a subsequent reload. emacs asks for a refinement and then immediately gives it back. Cornelis should do the same. Can we...

Set a `CmdComplete` `CommandOption`, and then follow the docs: ``` The following example lists user names to a Finger command :com -complete=custom,ListUsers -nargs=1 Finger !finger :fun ListUsers(A,L,P) : return system("cut...

When agda is running slow, it's easy to get ahead of the highlighter, and the resulting big error messages are annoying.

Investigate using line2byte for highlighting

2

Allegedly `line2byte` in vim does the line offsetting that we'd like.

It'd be nice to have a big testsuite here, just to really cement `cornelis` as the one true agda plugin for vim.

The one used for `TypeContext`, `Solve`, `Auto`, `Normalize`, `HelperFunc`. Use a global variable, configurable from vimrc.

If we have multiple values to split inside of a lambda split, subsequent splitting will replace old cases

Don't assume agda is on the path

1

Add some configuration to point at it

The former keeps ext marks if it can