From 31767aa8358ce2b7f4f367a11df7c530e6534236 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Thu, 21 Mar 2024 15:34:22 +0100 Subject: [PATCH] fix: use sticky diags in `getInteractiveDiagnostics` (#3730) I forgot to use the sticky diagnostics in `getInteractiveDiagnostics` in #3247, leading to them not consistently showing up in the "Messages" panel of the InfoView. --- src/Lean/Server/FileWorker.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index 0a92e43517..61aa20130b 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -512,15 +512,17 @@ section MessageHandling open Widget RequestM Language in def handleGetInteractiveDiagnosticsRequest (params : GetInteractiveDiagnosticsParams) : WorkerM (Array InteractiveDiagnostic) := do + let ctx ← read let st ← get -- NOTE: always uses latest document (which is the only one we can retrieve diagnostics for); -- any race should be temporary as the client should re-request interactive diagnostics when -- they receive the non-interactive diagnostics for the new document + let stickyDiags ← ctx.stickyDiagnosticsRef.get let diags ← st.doc.diagnosticsRef.get -- NOTE: does not wait for `lineRange?` to be fully elaborated, which would be problematic with -- fine-grained incremental reporting anyway; instead, the client is obligated to resend the -- request when the non-interactive diagnostics of this range have changed - return diags.filter fun diag => + return (stickyDiags.toArray ++ diags).filter fun diag => let r := diag.fullRange let diagStartLine := r.start.line let diagEndLine :=