fix: duplicate "import out of date" messages

src/Lean/Server/FileWorker.lean

@@ -60,7 +60,6 @@ open Snapshots
 open JsonRpc
 
 open Widget in
-abbrev StickyDiagnostics := RBTree InteractiveDiagnostic InteractiveDiagnostic.compareAsDiagnostics
 
 structure WorkerContext where
   /-- Synchronized output channel for LSP messages. Notifications for outdated versions are
@@ -80,7 +79,7 @@ structure WorkerContext where
   /--
   Diagnostics that are included in every single `textDocument/publishDiagnostics` notification.
   -/
-  stickyDiagnosticsRef : IO.Ref StickyDiagnostics
+  stickyDiagnosticsRef : IO.Ref (Array InteractiveDiagnostic)
   hLog                 : FS.Stream
   initParams           : InitializeParams
   processor            : Parser.InputContext → BaseIO Lean.Language.Lean.InitialSnapshot
@@ -155,7 +154,7 @@ This option can only be set on the command line, not in the lakefile or via `set
     let stickyInteractiveDiagnostics ← ctx.stickyDiagnosticsRef.get
     let docInteractiveDiagnostics ← doc.diagnosticsRef.get
     let diagnostics :=
-      stickyInteractiveDiagnostics.toArray ++ docInteractiveDiagnostics
+      stickyInteractiveDiagnostics ++ docInteractiveDiagnostics
       |>.map (·.toDiagnostic)
     let notification := mkPublishDiagnosticsNotification doc.meta diagnostics
     ctx.chanOut.send notification
@@ -463,14 +462,18 @@ section NotificationHandling
     let ctx ← read
     let s ← get
     let text := s.doc.meta.text
+    let importOutOfDataMessage := .text s!"Imports are out of date and should be rebuilt; \
+      use the \"Restart File\" command in your editor."
     let diagnostic := {
       range      := ⟨⟨0, 0⟩, ⟨1, 0⟩⟩
       fullRange? := some ⟨⟨0, 0⟩, text.utf8PosToLspPos text.source.endPos⟩
       severity?  := DiagnosticSeverity.information
-      message    := .text s!"Imports are out of date and should be rebuilt; \
-        use the \"Restart File\" command in your editor."
+      message := importOutOfDataMessage
     }
-    ctx.stickyDiagnosticsRef.modify fun stickyDiagnostics => stickyDiagnostics.insert diagnostic
+    ctx.stickyDiagnosticsRef.modify fun stickyDiagnostics =>
+      let stickyDiagnostics := stickyDiagnostics.filter
+        (·.message.stripTags != importOutOfDataMessage.stripTags)
+      stickyDiagnostics.push diagnostic
     publishDiagnostics ctx s.doc.toEditableDocumentCore
 
 def handleRpcRelease (p : Lsp.RpcReleaseParams) : WorkerM Unit := do
@@ -539,7 +542,7 @@ section MessageHandling
     -- 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 (stickyDiags.toArray ++ diags).filter fun diag =>
+    return (stickyDiags ++ diags).filter fun diag =>
       let r := diag.fullRange
       let diagStartLine := r.start.line
       let diagEndLine   :=