[vscode client] graph-editor integration

[ejgallego]

I'm opening this issue to ensure the next release will have everything needed by @amblafont 's graph-editor

@amblafont , do you have a pointer to the current hooks you are using? TIA!

IMHO, the thing that makes most sense is to place a Graph Editor extension in the Marketplace. Then, the extension registers with coq-lsp. But we don't need to do this at first.

Having a separate extension has some pros and cons:

• pros [in tree]: easy to install and to coordiante changes
• pros [separate]: own release schedule, more freedom in terms of organization, can support other Coq / Lean editors from the same extension.

See also #538 for the case of ViZX

[amblafont]

Here is the commit extending coq-lsp with the two commands I showed. In the new file yade.ts implementing those commands, I rely on the language client declared in client.ts, calling sendRequest with infoReq as a first parameter.

[amblafont]

Do you think it makes sense to implement an extension API that takes a variable cursor of type GoalRequest as argument and calls client.sendRequest(infoReq, cursor)?

[ejgallego]

Thanks @amblafont !

Do you think it makes sense to implement an extension API that takes a variable cursor of type GoalRequest as argument and calls client.sendRequest(infoReq, cursor)?

Sounds good! Let's do that first.

I'll also add an API for #538 that allows clients to listen to each time we are going to display the goals, in case they'd like to enrich them.

[ejgallego]

After some more discussion, we will both expose the GoalRequest call to other extensions, and also add a preprocess parameter so other extensions can use Coq-side tactics to pre-process the goal.