max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove semantic highlighting timeout (#7130)

Browse source 
Shot in the dark to resolve semantic highlighting issues. We don't
really need the timeout for semantic tokens anyways.
This commit is contained in:
Marc Huisinga 2025-02-18 11:24:49 +01:00 • committed by GitHub
parent 403e942f37
commit 0929cb3902
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Server/FileWorker/SemanticHighlighting.lean
View file

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