diff options
author | bors[bot] <26634292+bors[bot]@users.noreply.github.com> | 2021-04-19 16:12:49 +0100 |
---|---|---|
committer | GitHub <[email protected]> | 2021-04-19 16:12:49 +0100 |
commit | 9b853435d3bc7e30226ed149daddb2d472bf4fbd (patch) | |
tree | 40c45c9da338be9823d4a9279bcff211dd78266f /docs/dev | |
parent | 2cdc83af93fab15ca6d0a8e90a320140f18e6425 (diff) | |
parent | dcb759b7278615e55eeb20433a7e1a8464871538 (diff) |
Merge #8580
8580: Remove confusion around serverStatusNotification r=matklad a=matklad
bors r+
🤖
Co-authored-by: Aleksey Kladov <[email protected]>
Diffstat (limited to 'docs/dev')
-rw-r--r-- | docs/dev/lsp-extensions.md | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/docs/dev/lsp-extensions.md b/docs/dev/lsp-extensions.md index fff11e12e..f0f981802 100644 --- a/docs/dev/lsp-extensions.md +++ b/docs/dev/lsp-extensions.md | |||
@@ -433,11 +433,13 @@ interface ServerStatusParams { | |||
433 | /// `ok` means that the server is completely functional. | 433 | /// `ok` means that the server is completely functional. |
434 | /// | 434 | /// |
435 | /// `warning` means that the server is partially functional. | 435 | /// `warning` means that the server is partially functional. |
436 | /// It can server requests, but some results might be wrong due to, | 436 | /// It can answer correctly to most requests, but some results |
437 | /// for example, some missing dependencies. | 437 | /// might be wrong due to, for example, some missing dependencies. |
438 | /// | 438 | /// |
439 | /// `error` means that the server is not functional. For example, | 439 | /// `error` means that the server is not functional. For example, |
440 | /// there's a fatal build configuration problem. | 440 | /// there's a fatal build configuration problem. The server might |
441 | /// still give correct answers to simple requests, but most results | ||
442 | /// will be incomplete or wrong. | ||
441 | health: "ok" | "warning" | "error", | 443 | health: "ok" | "warning" | "error", |
442 | /// Is there any pending background work which might change the status? | 444 | /// Is there any pending background work which might change the status? |
443 | /// For example, are dependencies being downloaded? | 445 | /// For example, are dependencies being downloaded? |
@@ -451,6 +453,9 @@ This notification is sent from server to client. | |||
451 | The client can use it to display *persistent* status to the user (in modline). | 453 | The client can use it to display *persistent* status to the user (in modline). |
452 | It is similar to the `showMessage`, but is intended for stares rather than point-in-time events. | 454 | It is similar to the `showMessage`, but is intended for stares rather than point-in-time events. |
453 | 455 | ||
456 | Note that this functionality is intended primarily to inform the end user about the state of the server. | ||
457 | In particular, it's valid for the client to completely ignore this extension. | ||
458 | Clients are discouraged from but are allowed to use the `health` status to decide if it's worth sending a request to the server. | ||
454 | 459 | ||
455 | ## Syntax Tree | 460 | ## Syntax Tree |
456 | 461 | ||