This proxy does some slight adjustment between the messages that Isabelle's LSP
component and neovim exchange (e.g. registering as a code action provider for
inserting proofs when using try or sledgehammer.
See contrib/init.vim for how I've integrated it in my vim setup. Note that not
all plugins might be present. The only reason it's not packaged as a neovim
plugin is that don't have the skills or time to do that - ideas and pull
requests are welcome!
Build using go build main.go and then use the resulting isabelle-lsp binary
as the LSP server launched by neovim. The isabelle-lsp binary will launch the
actual isabelle vscode_server for you.
I think I remembered some issue where you had to wait with moving the cursor because otherwise the isabelle LSP wouldn't like the proxy anymore and stop answering its requests. I've never dug too deep into it, so this might or might not still be a problem.