From ddff87f7f5fd3800ee9a9f0b6381f8a9613edbfa Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 11 Mar 2021 18:41:10 +0100 Subject: [PATCH] feat: server: also implement full semantic token requests because lsp-mode freaks out without them --- src/Lean/Data/Lsp/LanguageFeatures.lean | 4 ++++ src/Lean/Server/FileSource.lean | 3 +++ src/Lean/Server/FileWorker.lean | 18 +++++++++++++++--- src/Lean/Server/Watchdog.lean | 3 ++- 4 files changed, 24 insertions(+), 4 deletions(-) diff --git a/src/Lean/Data/Lsp/LanguageFeatures.lean b/src/Lean/Data/Lsp/LanguageFeatures.lean index d16f5e5ac8..0db31fefaf 100644 --- a/src/Lean/Data/Lsp/LanguageFeatures.lean +++ b/src/Lean/Data/Lsp/LanguageFeatures.lean @@ -200,6 +200,10 @@ structure SemanticTokensOptions where } -/ deriving FromJson, ToJson +structure SemanticTokensParams where + textDocument : TextDocumentIdentifier + deriving FromJson, ToJson + structure SemanticTokensRangeParams where textDocument : TextDocumentIdentifier range : Range diff --git a/src/Lean/Server/FileSource.lean b/src/Lean/Server/FileSource.lean index efd99cc035..3f48e2f7e9 100644 --- a/src/Lean/Server/FileSource.lean +++ b/src/Lean/Server/FileSource.lean @@ -61,6 +61,9 @@ instance DocumentHighlightParams.hasFileSource : FileSource DocumentHighlightPar instance DocumentSymbolParams.hasFileSource : FileSource DocumentSymbolParams := ⟨fun p => fileSource p.textDocument⟩ +instance SemanticTokensParams.hasFileSource : FileSource SemanticTokensParams := + ⟨fun p => fileSource p.textDocument⟩ + instance SemanticTokensRangeParams.hasFileSource : FileSource SemanticTokensRangeParams := ⟨fun p => fileSource p.textDocument⟩ diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index d275d061c0..d27bd55142 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -528,13 +528,11 @@ section RequestHandling children? := syms.toArray } :: syms', stxs'') - def handleSemanticTokensRange (p : SemanticTokensRangeParams) : + def handleSemanticTokens (beginPos endPos : String.Pos) : ServerM (Task (Except IO.Error (Except RequestError SemanticTokens))) := do let st ← read let doc ← st.docRef.get let text := doc.meta.text - let beginPos := text.lspPosToUtf8Pos p.range.start - let endPos := text.lspPosToUtf8Pos p.range.end let t ← doc.cmdSnaps.waitAll (·.beginPos < endPos) IO.mapTask (t := t) fun (snaps, _) => do let mut data := #[] @@ -556,6 +554,19 @@ section RequestHandling lspPos := lspPos' return Except.ok { data := data } + def handleSemanticTokensFull (p : SemanticTokensParams) : + ServerM (Task (Except IO.Error (Except RequestError SemanticTokens))) := do + handleSemanticTokens 0 (1 <<< 16) + + def handleSemanticTokensRange (p : SemanticTokensRangeParams) : + ServerM (Task (Except IO.Error (Except RequestError SemanticTokens))) := do + let st ← read + let doc ← st.docRef.get + let text := doc.meta.text + let beginPos := text.lspPosToUtf8Pos p.range.start + let endPos := text.lspPosToUtf8Pos p.range.end + handleSemanticTokens beginPos endPos + partial def handleWaitForDiagnostics (p : WaitForDiagnosticsParams) : ServerM (Task (Except IO.Error (Except RequestError WaitForDiagnostics))) := do let st ← read @@ -617,6 +628,7 @@ section MessageHandling | "textDocument/typeDefinition" => handle TextDocumentPositionParams (Array LocationLink) <| handleDefinition (goToType? := true) | "textDocument/documentHighlight" => handle DocumentHighlightParams DocumentHighlightResult handleDocumentHighlight | "textDocument/documentSymbol" => handle DocumentSymbolParams DocumentSymbolResult handleDocumentSymbol + | "textDocument/semanticTokens/full" => handle SemanticTokensParams SemanticTokens handleSemanticTokensFull | "textDocument/semanticTokens/range" => handle SemanticTokensRangeParams SemanticTokens handleSemanticTokensRange | "$/lean/plainGoal" => handle PlainGoalParams (Option PlainGoal) handlePlainGoal | _ => throwServerError s!"Got unsupported request: {method}" diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index 134586ad69..d2b6461331 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -389,6 +389,7 @@ section MessageHandling | "textDocument/documentHighlight" => handle DocumentHighlightParams | "textDocument/documentSymbol" => handle DocumentSymbolParams | "textDocument/semanticTokens/range" => handle SemanticTokensRangeParams + | "textDocument/semanticTokens/full" => handle SemanticTokensParams | "$/lean/plainGoal" => handle PlainGoalParams | _ => (←read).hOut.writeLspResponseError @@ -506,7 +507,7 @@ def mkLeanServerCapabilities : ServerCapabilities := { tokenTypes := SemanticTokenType.names tokenModifiers := #[] } - full := false + full := true range := true } }