Summary
Receive and store Lean diagnostics published by the language server.
Tasks
- Handle
textDocument/publishDiagnostics notifications.
- Normalize diagnostics into Elixir structs or maps.
- Associate diagnostics with document URIs.
- Add tests for diagnostic payload parsing.
Acceptance criteria
- The session can return the latest diagnostics for an opened document.
- Diagnostic severity, range, and message are preserved.
Summary
Receive and store Lean diagnostics published by the language server.
Tasks
textDocument/publishDiagnosticsnotifications.Acceptance criteria