From 3f8f2b09afc44386e5d16937338fa0d7677a0562 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Fri, 22 Mar 2024 14:13:20 +0100 Subject: [PATCH] chore: more generic import out of date diagnostic (#3739) The concrete dependency that is stale isn't really actionable information for users (ideally we'd like something like "amount of dependencies that will be rebuilt when you restart file"). This also makes the diagnostic an "information" diagnostic so that non-infoview users can still see it. Since we are moving away from using notifications for stale dependency information, we don't need to provide an ID anymore, either. --- src/Lean/Server/FileWorker.lean | 25 ++++++++++--------------- 1 file changed, 10 insertions(+), 15 deletions(-) diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index 61aa20130b..304cb92c7f 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -435,26 +435,21 @@ section NotificationHandling /-- Received from the watchdog when a dependency of this file is detected as being stale. - Issues a `LanguageServer_ImportOutOfDate` sticky diagnostic to the client. + Issues a sticky diagnostic to the client that it should run "Restart File". -/ - def handleStaleDependency (p : LeanStaleDependencyParams) : WorkerM Unit := do + def handleStaleDependency (_ : LeanStaleDependencyParams) : WorkerM Unit := do let ctx ← read let s ← get let text := s.doc.meta.text - let _ ← IO.mapTask (t := s.srcSearchPathTask) fun srcSearchPath => do - let some staleDependencyName ← moduleFromDocumentUri srcSearchPath p.staleDependency - | return - let diagnostic := { - range := ⟨⟨0, 0⟩, ⟨1, 0⟩⟩ - fullRange? := some ⟨⟨0, 0⟩, text.utf8PosToLspPos text.source.endPos⟩ - severity? := DiagnosticSeverity.hint - code? := some <| .string "LanguageServer_ImportOutOfDate" - message := .text s!"Import '{staleDependencyName}' is out of date; \ - use the \"Restart File\" command in your editor." - data? := some staleDependencyName.toString + 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." } - ctx.stickyDiagnosticsRef.modify fun stickyDiagnostics => stickyDiagnostics.insert diagnostic - publishDiagnostics ctx s.doc.toEditableDocumentCore + ctx.stickyDiagnosticsRef.modify fun stickyDiagnostics => stickyDiagnostics.insert diagnostic + publishDiagnostics ctx s.doc.toEditableDocumentCore def handleRpcRelease (p : Lsp.RpcReleaseParams) : WorkerM Unit := do -- NOTE(WN): when the worker restarts e.g. due to changed imports, we may receive `rpc/release`