From 45d39422bc57fada6bf281cf2119fdd99de14343 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Thu, 6 Feb 2025 20:26:11 +0100 Subject: [PATCH] fix: inlay hints in untitled files (#6978) This PR fixes a bug where both the inlay hint change invalidation logic and the inlay hint edit delay logic were broken in untitled files. Thanks to @Julian for spotting this! --- src/Lean/Server/FileWorker/InlayHints.lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/Lean/Server/FileWorker/InlayHints.lean b/src/Lean/Server/FileWorker/InlayHints.lean index cae5367370..339b468e3e 100644 --- a/src/Lean/Server/FileWorker/InlayHints.lean +++ b/src/Lean/Server/FileWorker/InlayHints.lean @@ -61,7 +61,10 @@ def applyEditToHint? (hintMod : Name) (ihi : Elab.InlayHintInfo) (range : String let isLabelLocAffectedByEdit := match ihi.label with | .name _ => false - | .parts ps => ps.any (·.location?.any (fun loc => loc.module == hintMod && range.overlaps loc.range (includeFirstStop := true))) + | .parts ps => + ps.any fun p => + p.location?.any fun loc => + loc.module == hintMod && range.overlaps loc.range (includeFirstStop := true) -- We always include the stop of the edit range because insertion edit ranges may be empty, -- but we must still invalidate the inlay hint in this case. let isInlayHintInvalidatedByEdit := @@ -148,13 +151,14 @@ def handleInlayHintsDidChange (p : DidChangeTextDocumentParams) let meta := (← read).doc.meta let text := meta.text let srcSearchPath := (← read).srcSearchPath - let .ok (some modName) ← EIO.toBaseIO <| do + let .ok modName? ← EIO.toBaseIO <| do let some path := System.Uri.fileUriToPath? meta.uri | return none let some mod ← searchModuleNameOfFileName path srcSearchPath | return some <| ← moduleNameOfFileName path none return some mod | return + let modName := modName?.getD .anonymous -- `.anonymous` occurs in untitled files let s ← get let mut updatedOldInlayHints := #[] for ihi in s.oldInlayHints do