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 =>