ejgallego / coq-lsp

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

[petanque] Make core protocol independent of Coq env runtime #771

Closed ejgallego closed 3 months ago

ejgallego commented 3 months ago

This will allow us to to embed Agent and the petanque JSON-RPC protocol into LSP directly.

The change is not backwards compatible, as in this model clients aren't supposed to handle Env.t anymore, so this paramater is dropped from petanque/start and from the return type of petanque/setWorkspace.

Instead, clients now have to provide a call-back for the agent to retrieve the document.

As we are breaking the protocol, we profit from doing some other small tweaks. Full list of protocol changes:

cc: @gbdrt