[user interaction] Proof-general like mode.

[ejgallego]

I'm opening this issue as a follow up with a discussion with @tabareau and his feedback.

As of today, coq-lsp engine (Flèche) has the capability to work in fully "on-demand" mode.

This can be used to implement different document evaluation strategies.

As of today we support on-demand and continuous, however on-demand is less lazy than we would like due to the way certain LSP calls are setup.

In particular, most calls such as completion or codeAction do register with Flèche as demanding the document node.

Thus, even in full lazy mode, with goals only on user request, VSCode will issue a request for completion, which Flèche will in turn turn into an execution request.

We should both:

• provide a better UI so users can select the different modes available.
• update the handlers for these LSP request so that they depend either on the previous node or on the current one but optionally, so they don't trigger execution
• ensure we are getting the desired amount of execution on our test suite.