search

ejgallego / coq-lsp

Visual Studio Code Extension and Language Server Protocol for Coq
GNU Lesser General Public License v2.1
143 stars 31 forks source link

[vscode] Provide generic user goal request hook. #672

Closed ejgallego closed 4 months ago

ejgallego commented 5 months ago

This allows extensions to register without having to modify ours; it should subsume previous hooks for VIXZ and VIZCAR visualizers.

There are many more improvements we can do to this API.

Fixes #538

ejgallego commented 5 months ago

@bhaktishh can you review this and see if that would work?

Extensions should be ported easily, basically they can recover the previous semantics by doing:

// ensure coq-lsp is activated, etc....
let coqLspAPI = extensions.getExtension('coq-lsp')?.export;
let hook = coqLSPAPI.onUserGoals((goals) => commands.executeCommand("vizx.lspRender", goals));

or any other code they may want, no need to pass via a command actually.

Don't forget to call hook.dispose() to remove the binding in the extension's deactivate method.

ejgallego commented 4 months ago

@bhaktishh merging this as I plan to release ASAP, I did some testing and it worked fine locally. If there is any problem let me know and I'll be quick to fix it.