coq-lsp icon indicating copy to clipboard operation
coq-lsp copied to clipboard

[lsp] Preliminary support for pull diagnostics

Open ejgallego opened this issue 2 years ago • 2 comments

  • added progress and partialResult support to the core layer of the protocol
  • pull diagnostics: wip

Note that VS Code won't set the partial progress token for textDocument/diagnostic, so this is not very useful for VS Code yet, but may be for other clients.

ejgallego avatar Feb 16 '23 19:02 ejgallego

Did you mean to title it pull diagnostics?

Alizter avatar Feb 17 '23 00:02 Alizter

Did you mean to title it pull diagnostics?

Yes, thanks!

ejgallego avatar Feb 17 '23 01:02 ejgallego