Provides an IpcM monad for interacting with an external LSP process. Used for testing the Lean server.
Equations
Instances For
Equations
Instances For
Equations
Instances For
Reads response, discarding notifications and server-to-client requests in between.
This function is meant purely for testing where we use collectDiagnostics
explicitly
if we do care about such notifications.
Waits for the worker to emit all diagnostic notifications for the current document version and returns the last notification, if any.
We used to return all notifications but with debouncing in the server, this would not be deterministic anymore as what messages are dropped depends on wall-clock timing.
Equations
Instances For
Equations
Instances For
Waits for a diagnostic notification with a specific message to be emitted. Discards all received
messages, so should not be combined with collectDiagnostics
.