feat: server: also implement full semantic token requests

because lsp-mode freaks out without them

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

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⟩
 

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}"

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