max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: describe non-standard requests and notifications

Browse source
This commit is contained in:
Gabriel Ebner 2021-06-05 10:21:29 +02:00 • committed by Sebastian Ullrich
parent 501c31da4d
commit f50647e1c2
1 changed files with 8 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Lean/Data/Lsp/Extra.lean
View file

@ -10,11 +10,17 @@ import Lean.Data.Lsp.Basic
/-!
This file contains Lean-specific extensions to LSP.
The following additional packets are supported:
- "textDocument/waitForDiagnostics": Yields a response when all the diagnostics for a version of the document
The following additional requests and notifications are supported:
- `textDocument/waitForDiagnostics`: Yields a response when all the diagnostics for a version of the document
greater or equal to the specified one have been emitted. If the request specifies a version above the most
recently processed one, the server will delay the response until it does receive the specified version.
Exists for synchronization purposes, e.g. during testing or when external tools might want to use our LSP server.
- `$/lean/fileProgress`: Notification that contains the ranges of the document that are still being processed
by the server.
- `$/lean/plainGoal`: Returns the goal(s) at the specified position, pretty-printed as a string.
-/
namespace Lean.Lsp