From 0929cb3902de70332b7292694bd587bc248d89b1 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Tue, 18 Feb 2025 11:24:49 +0100 Subject: [PATCH] chore: remove semantic highlighting timeout (#7130) Shot in the dark to resolve semantic highlighting issues. We don't really need the timeout for semantic tokens anyways. --- src/Lean/Server/FileWorker/SemanticHighlighting.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Lean/Server/FileWorker/SemanticHighlighting.lean b/src/Lean/Server/FileWorker/SemanticHighlighting.lean index d9d666b66e..979b3fc7fe 100644 --- a/src/Lean/Server/FileWorker/SemanticHighlighting.lean +++ b/src/Lean/Server/FileWorker/SemanticHighlighting.lean @@ -139,7 +139,6 @@ def collectInfoBasedSemanticTokens (i : Elab.InfoTree) : Array LeanSemanticToken /-- Computes the semantic tokens in the range [beginPos, endPos?). -/ def handleSemanticTokens (beginPos : String.Pos) (endPos? : Option String.Pos) : RequestM (RequestTask (LspResponse SemanticTokens)) := do - let ctx ← read let doc ← readDoc match endPos? with | none => @@ -147,7 +146,7 @@ def handleSemanticTokens (beginPos : String.Pos) (endPos? : Option String.Pos) -- for the full file before sending a response. This means that the response will be incomplete, -- which we mitigate by regularly sending `workspace/semanticTokens/refresh` requests in the -- `FileWorker` to tell the client to re-compute the semantic tokens. - let (snaps, _, isComplete) ← doc.cmdSnaps.getFinishedPrefixWithTimeout 3000 (cancelTk? := ctx.cancelTk.cancellationTask) + let (snaps, _, isComplete) ← doc.cmdSnaps.getFinishedPrefix asTask <| do return { response := ← run doc snaps, isComplete } | some endPos =>