diff --git a/src/Lean/Data/Lsp/InitShutdown.lean b/src/Lean/Data/Lsp/InitShutdown.lean
index a953115926..e964ff5307 100644
--- a/src/Lean/Data/Lsp/InitShutdown.lean
+++ b/src/Lean/Data/Lsp/InitShutdown.lean
@@ -73,8 +73,7 @@ structure InitializationOptions where
 structure InitializeParams where
   processId? : Option Int := none
   clientInfo? : Option ClientInfo := none
-  /- We don't support the deprecated rootPath
-  (rootPath? : Option String) -/
+  /-- Not used by the language server. We use the cwd of the server process instead. -/
   rootUri? : Option String := none
   initializationOptions? : Option InitializationOptions := none
   capabilities : ClientCapabilities
diff --git a/src/Lean/Server/ProtocolOverview.lean b/src/Lean/Server/ProtocolOverview.lean
index c270e7c50f..4f493fc900 100644
--- a/src/Lean/Server/ProtocolOverview.lean
+++ b/src/Lean/Server/ProtocolOverview.lean
@@ -29,7 +29,7 @@ inductive ProtocolExtensionKind
 structure RequestOverview where
   method : String
   direction : MessageDirection
-  kind : ProtocolExtensionKind
+  kinds : Array ProtocolExtensionKind
   parameterType : Type
   responseType : Type
   description : String
@@ -43,7 +43,7 @@ structure RpcRequestOverview where
 structure NotificationOverview where
   method : String
   direction : MessageDirection
-  kind : ProtocolExtensionKind
+  kinds : Array ProtocolExtensionKind
   parameterType : Type
   description : String
 
@@ -68,14 +68,18 @@ def protocolOverview : Array MessageOverview := #[
   .notification {
     method := "$/cancelRequest"
     direction := .clientToServer
-    kind := .standard
+    kinds := #[.standard]
     parameterType := CancelParams
     description := "Emitted in VS Code when a running request is cancelled, e.g. when the document state has changed."
   },
   .request {
     method := "initialize"
     direction := .clientToServer
-    kind := .extendedParameterType #[``InitializeParams.initializationOptions?, ``InitializeParams.capabilities, ``ClientCapabilities.lean?]
+    kinds := #[
+      .standardViolation "The Lean language server currently ignores almost all standard client capabilities and expects clients to be sufficiently fully-featured.",
+      .standardViolation "The `InitializeParams.rootUri?` field is not used by the language server - it instead uses the cwd of the language server process.",
+      .extendedParameterType #[``InitializeParams.initializationOptions?, ``InitializeParams.capabilities, ``ClientCapabilities.lean?]
+    ]
     parameterType := InitializeParams
     responseType := InitializeResult
     description := "Emitted when the language server is being initialized. The server is only started once an `initialized` notification is emitted after the `initialize` request."
@@ -83,14 +87,14 @@ def protocolOverview : Array MessageOverview := #[
   .notification {
     method := "initialized"
     direction := .clientToServer
-    kind := .standard
+    kinds := #[.standard]
     parameterType := InitializedParams
     description := "Emitted after a response to the `initialize` request to start the server."
   },
   .request {
     method := "shutdown"
     direction := .clientToServer
-    kind := .standard
+    kinds := #[.standard]
     parameterType := Option Empty
     responseType := Option Empty
     description := "Emitted when the language server is being asked to shut down and deliver responses for all pending requests."
@@ -98,14 +102,14 @@ def protocolOverview : Array MessageOverview := #[
   .notification {
     method := "exit"
     direction := .clientToServer
-    kind := .standard
+    kinds := #[.standard]
     parameterType := Option Empty
     description := "Emitted once the language server should shut down after a `shutdown` request."
   },
   .request {
     method := "client/registerCapability"
     direction := .serverToClient
-    kind := .standard
+    kinds := #[.standard]
     parameterType := NestedType #[Option RegistrationParams, DidChangeWatchedFilesRegistrationOptions]
     responseType := Option Empty
     description := "Emitted by the language server after receiving the `initialized` notification to register file watchers for `.lean` and `.ilean` files using the `workspace/didChangeWatchedFiles` registration."
@@ -113,56 +117,56 @@ def protocolOverview : Array MessageOverview := #[
   .notification {
     method := "textDocument/didOpen"
     direction := .clientToServer
-    kind := .extendedParameterType #[``LeanDidOpenTextDocumentParams.dependencyBuildMode?]
+    kinds := #[.extendedParameterType #[``LeanDidOpenTextDocumentParams.dependencyBuildMode?]]
     parameterType := LeanDidOpenTextDocumentParams
     description := "Emitted in VS Code when a text document is opened. VS Code may sometimes emit this notification for files that were not opened in an editor."
   },
   .notification {
     method := "textDocument/didClose"
     direction := .clientToServer
-    kind := .standard
+    kinds := #[.standard]
     parameterType := DidCloseTextDocumentParams
     description := "Emitted in VS Code when a text document is closed. VS Code may sometimes emit this notification for files that were not opened in an editor."
   },
   .notification {
     method := "textDocument/didChange"
     direction := .clientToServer
-    kind := .standard
+    kinds := #[.standard]
     parameterType := DidChangeTextDocumentParams
     description := "Emitted in VS Code when a text document is edited."
   },
   .notification {
     method := "textDocument/didSave"
     direction := .clientToServer
-    kind := .standard
+    kinds := #[.standard]
     parameterType := DidSaveTextDocumentParams
     description := "Emitted in VS Code when a text document is saved."
   },
   .notification {
     method := "workspace/didChangeWatchedFiles"
     direction := .clientToServer
-    kind := .standard
+    kinds := #[.standard]
     parameterType := DidChangeWatchedFilesParams
     description := "Emitted in VS Code when one of the files that the language server registered a file watcher for changes."
   },
   .notification {
     method := "textDocument/publishDiagnostics"
     direction := .serverToClient
-    kind := .extendedParameterType #[``PublishDiagnosticsParams.diagnostics, ``DiagnosticWith.fullRange?, ``DiagnosticWith.isSilent?, ``DiagnosticWith.leanTags?]
+    kinds := #[.extendedParameterType #[``PublishDiagnosticsParams.diagnostics, ``DiagnosticWith.fullRange?, ``DiagnosticWith.isSilent?, ``DiagnosticWith.leanTags?]]
     parameterType := PublishDiagnosticsParams
     description := "Emitted by the language server whenever a new set of diagnostics becomes available for a file. Unlike most language servers, the Lean language server emits this notification incrementally while processing the file, not only when the full file has been processed."
   },
   .notification {
     method := "$/lean/fileProgress"
     direction := .serverToClient
-    kind := .leanSpecificMethod
+    kinds := #[.leanSpecificMethod]
     parameterType := LeanFileProgressParams
     description := "Emitted by the language server whenever the elaboration progress of a file changes."
   },
   .request {
     method := "textDocument/completion"
     direction := .clientToServer
-    kind := .standard
+    kinds := #[.standard]
     parameterType := CompletionParams
     responseType := CompletionList
     description := "Emitted in VS Code when auto-completion is triggered, e.g. automatically while typing or after hitting Ctrl+Space."
@@ -170,7 +174,7 @@ def protocolOverview : Array MessageOverview := #[
   .request {
     method := "completionItem/resolve"
     direction := .clientToServer
-    kind := .standard
+    kinds := #[.standard]
     parameterType := CompletionItem
     responseType := CompletionItem
     description := "Emitted in VS Code when an auto-completion entry is selected."
@@ -178,7 +182,7 @@ def protocolOverview : Array MessageOverview := #[
   .request {
     method := "textDocument/codeAction"
     direction := .clientToServer
-    kind := .standard
+    kinds := #[.standard]
     parameterType := CodeActionParams
     responseType := Array CodeAction
     description := "Emitted in VS Code when code actions are triggered, e.g. automatically while typing, moving the text cursor or when hovering over a diagnostic."
@@ -186,7 +190,7 @@ def protocolOverview : Array MessageOverview := #[
   .request {
     method := "codeAction/resolve"
     direction := .clientToServer
-    kind := .standard
+    kinds := #[.standard]
     parameterType := CodeAction
     responseType := CodeAction
     description := "Emitted in VS Code when a code action in the light bulb menu is selected."
@@ -194,7 +198,7 @@ def protocolOverview : Array MessageOverview := #[
   .request {
     method := "textDocument/signatureHelp"
     direction := .clientToServer
-    kind := .standard
+    kinds := #[.standard]
     parameterType := SignatureHelpParams
     responseType := Option SignatureHelp
     description := "Emitted in VS Code when the signature help is triggered, e.g. automatically while typing or after hitting Ctrl+Shift+Space."
@@ -202,7 +206,7 @@ def protocolOverview : Array MessageOverview := #[
   .request {
     method := "textDocument/hover"
     direction := .clientToServer
-    kind := .standard
+    kinds := #[.standard]
     parameterType := HoverParams
     responseType := Option Hover
     description := "Emitted in VS Code when hovering over an identifier in the editor."
@@ -210,7 +214,7 @@ def protocolOverview : Array MessageOverview := #[
   .request {
     method := "textDocument/documentHighlight"
     direction := .clientToServer
-    kind := .standard
+    kinds := #[.standard]
     parameterType := DocumentHighlightParams
     responseType := DocumentHighlightResult
     description := "Emitted in VS Code when the text cursor is on an identifier."
@@ -218,7 +222,7 @@ def protocolOverview : Array MessageOverview := #[
   .request {
     method := "textDocument/documentSymbol"
     direction := .clientToServer
-    kind := .standard
+    kinds := #[.standard]
     parameterType := DocumentSymbolParams
     responseType := DocumentSymbolResult
     description := "Emitted in VS Code when a file is first opened or when it is changed."
@@ -226,7 +230,7 @@ def protocolOverview : Array MessageOverview := #[
   .request {
     method := "textDocument/foldingRange"
     direction := .clientToServer
-    kind := .standard
+    kinds := #[.standard]
     parameterType := FoldingRangeParams
     responseType := Array FoldingRange
     description := "Emitted in VS Code when a file is first opened or when it is changed."
@@ -234,7 +238,7 @@ def protocolOverview : Array MessageOverview := #[
   .request {
     method := "textDocument/documentColor"
     direction := .clientToServer
-    kind := .standard
+    kinds := #[.standard]
     parameterType := DocumentColorParams
     responseType := Array ColorInformation
     description := "Emitted in VS Code when a file is first opened or when it is changed. The language server defines this handler to override the default document color handler of VS Code with an empty one."
@@ -242,7 +246,7 @@ def protocolOverview : Array MessageOverview := #[
   .request {
     method := "textDocument/semanticTokens/range"
     direction := .clientToServer
-    kind := .standard
+    kinds := #[.standard]
     parameterType := SemanticTokensRangeParams
     responseType := SemanticTokens
     description := "Emitted in VS Code when a file is changed."
@@ -250,7 +254,7 @@ def protocolOverview : Array MessageOverview := #[
   .request {
     method := "textDocument/semanticTokens/full"
     direction := .clientToServer
-    kind := .standardViolation "Instead of reporting the full semantic tokens for the full file as specified by LSP, the Lean language server will only report the semantic tokens for the part of the file that has been processed so far. If the response is incomplete, the language server periodically emits `workspace/semanticTokens/refresh` to request another `textDocument/semanticTokens/full` request from the client. This process is repeated until the file has been fully processed and all semantic tokens have been reported. We use this trick to stream semantic tokens to VS Code, despite the fact that VS Code does not support result streaming."
+    kinds := #[.standardViolation "Instead of reporting the full semantic tokens for the full file as specified by LSP, the Lean language server will only report the semantic tokens for the part of the file that has been processed so far. If the response is incomplete, the language server periodically emits `workspace/semanticTokens/refresh` to request another `textDocument/semanticTokens/full` request from the client. This process is repeated until the file has been fully processed and all semantic tokens have been reported. We use this trick to stream semantic tokens to VS Code, despite the fact that VS Code does not support result streaming."]
     parameterType := SemanticTokensParams
     responseType := SemanticTokens
     description := "Emitted in VS Code when a file is first opened, when it is changed or when VS Code receives a `workspace/semanticTokens/refresh` request from the server."
@@ -258,7 +262,7 @@ def protocolOverview : Array MessageOverview := #[
   .request {
     method := "workspace/semanticTokens/refresh"
     direction := .serverToClient
-    kind := .standard
+    kinds := #[.standard]
     parameterType := Option Empty
     responseType := Option Empty
     description := "Emitted by the language server to request another `textDocument/semanticTokens/full` request from the client."
@@ -266,7 +270,7 @@ def protocolOverview : Array MessageOverview := #[
   .request {
     method := "textDocument/inlayHint"
     direction := .clientToServer
-    kind := .standardViolation "Instead of reporting the full inlay hints for the full file as specified by LSP, the Lean language server will only report the inlay hints for the part of the file that has been processed so far. If the response is incomplete, the language server periodically emits `workspace/inlayHint/refresh` to request another `textDocument/inlayHint` request from the client. This process is repeated until the file has been fully processed and all inlay hints have been reported. We use this trick to stream inlay hints to VS Code, despite the fact that VS Code does not support result streaming."
+    kinds := #[.standardViolation "Instead of reporting the full inlay hints for the full file as specified by LSP, the Lean language server will only report the inlay hints for the part of the file that has been processed so far. If the response is incomplete, the language server periodically emits `workspace/inlayHint/refresh` to request another `textDocument/inlayHint` request from the client. This process is repeated until the file has been fully processed and all inlay hints have been reported. We use this trick to stream inlay hints to VS Code, despite the fact that VS Code does not support result streaming."]
     parameterType := InlayHintParams
     responseType := Array InlayHint
     description := "Emitted in VS Code when a file is first opened, when it is changed or when VS Code receives a `workspace/inlayHint/refresh` request from the server."
@@ -274,7 +278,7 @@ def protocolOverview : Array MessageOverview := #[
   .request {
     method := "workspace/inlayHint/refresh"
     direction := .serverToClient
-    kind := .standard
+    kinds := #[.standard]
     parameterType := Option Empty
     responseType := Option Empty
     description := "Emitted by the language server to request another `textDocument/inlayHint` request from the client."
@@ -282,7 +286,7 @@ def protocolOverview : Array MessageOverview := #[
   .request {
     method := "textDocument/definition"
     direction := .clientToServer
-    kind := .standard
+    kinds := #[.standard]
     parameterType := DefinitionParams
     responseType := Array LocationLink
     description := "Emitted in VS Code when clicking 'Go to Definition' in the context menu or using Ctrl+Click."
@@ -290,7 +294,7 @@ def protocolOverview : Array MessageOverview := #[
   .request {
     method := "textDocument/declaration"
     direction := .clientToServer
-    kind := .standard
+    kinds := #[.standard]
     parameterType := DefinitionParams
     responseType := Array LocationLink
     description := "Emitted in VS Code when clicking 'Go to Declaration' in the context menu."
@@ -298,7 +302,7 @@ def protocolOverview : Array MessageOverview := #[
   .request {
     method := "textDocument/typeDefinition"
     direction := .clientToServer
-    kind := .standard
+    kinds := #[.standard]
     parameterType := DefinitionParams
     responseType := Array LocationLink
     description := "Emitted in VS Code when clicking 'Go to Type Definition' in the context menu."
@@ -306,7 +310,7 @@ def protocolOverview : Array MessageOverview := #[
   .request {
     method := "textDocument/references"
     direction := .clientToServer
-    kind := .standard
+    kinds := #[.standard]
     parameterType := ReferenceParams
     responseType := Array Location
     description := "Emitted in VS Code when clicking 'Find All References' or 'Go to References' in the context menu."
@@ -314,7 +318,7 @@ def protocolOverview : Array MessageOverview := #[
   .request {
     method := "textDocument/prepareCallHierarchy"
     direction := .clientToServer
-    kind := .standard
+    kinds := #[.standard]
     parameterType := CallHierarchyPrepareParams
     responseType := Array CallHierarchyItem
     description := "Emitted in VS Code when clicking 'Show Call Hierarchy' in the context menu."
@@ -322,7 +326,7 @@ def protocolOverview : Array MessageOverview := #[
   .request {
     method := "callHierarchy/incomingCalls"
     direction := .clientToServer
-    kind := .standard
+    kinds := #[.standard]
     parameterType := CallHierarchyIncomingCallsParams
     responseType := Array CallHierarchyIncomingCall
     description := "Emitted in VS Code when expanding a node in the call hierarchy in 'incoming calls' mode."
@@ -330,7 +334,7 @@ def protocolOverview : Array MessageOverview := #[
   .request {
     method := "callHierarchy/outgoingCalls"
     direction := .clientToServer
-    kind := .standard
+    kinds := #[.standard]
     parameterType := CallHierarchyOutgoingCallsParams
     responseType := Array CallHierarchyOutgoingCall
     description := "Emitted in VS Code when expanding a node in the call hierarchy in 'outgoing calls' mode."
@@ -338,7 +342,7 @@ def protocolOverview : Array MessageOverview := #[
   .request {
     method := "$/lean/prepareModuleHierarchy"
     direction := .clientToServer
-    kind := .leanSpecificMethod
+    kinds := #[.leanSpecificMethod]
     parameterType := LeanPrepareModuleHierarchyParams
     responseType := Option LeanModule
     description := "Emitted in VS Code when clicking 'Show Module Hierarchy' or 'Show Inverse Module Hierarchy' in the context menu."
@@ -346,7 +350,7 @@ def protocolOverview : Array MessageOverview := #[
   .request {
     method := "$/lean/moduleHierarchy/imports"
     direction := .clientToServer
-    kind := .leanSpecificMethod
+    kinds := #[.leanSpecificMethod]
     parameterType := LeanModuleHierarchyImportsParams
     responseType := Array LeanImport
     description := "Emitted in VS Code when expanding a node in the module hierarchy."
@@ -354,7 +358,7 @@ def protocolOverview : Array MessageOverview := #[
   .request {
     method := "$/lean/moduleHierarchy/importedBy"
     direction := .clientToServer
-    kind := .leanSpecificMethod
+    kinds := #[.leanSpecificMethod]
     parameterType := LeanModuleHierarchyImportedByParams
     responseType := Array LeanImport
     description := "Emitted in VS Code when expanding a node in the inverse module hierarchy."
@@ -362,7 +366,7 @@ def protocolOverview : Array MessageOverview := #[
   .request {
     method := "textDocument/prepareRename"
     direction := .clientToServer
-    kind := .standard
+    kinds := #[.standard]
     parameterType := PrepareRenameParams
     responseType := Option Range
     description := "Emitted in VS Code when clicking 'Rename Symbol' in the context menu."
@@ -370,7 +374,7 @@ def protocolOverview : Array MessageOverview := #[
   .request {
     method := "textDocument/rename"
     direction := .clientToServer
-    kind := .standard
+    kinds := #[.standard]
     parameterType := RenameParams
     responseType := WorkspaceEdit
     description := "Emitted in VS Code when entering an identifier after clicking 'Rename Symbol' in the context menu."
@@ -378,7 +382,7 @@ def protocolOverview : Array MessageOverview := #[
   .request {
     method := "workspace/symbol"
     direction := .clientToServer
-    kind := .standard
+    kinds := #[.standard]
     parameterType := WorkspaceSymbolParams
     responseType := Array SymbolInformation
     description := "Emitted in VS Code when opening the command prompt and entering a `#` prefix with a query after it."
@@ -386,7 +390,7 @@ def protocolOverview : Array MessageOverview := #[
   .request {
     method := "$/lean/plainGoal"
     direction := .clientToServer
-    kind := .leanSpecificMethod
+    kinds := #[.leanSpecificMethod]
     parameterType := PlainGoalParams
     responseType := Option PlainGoal
     description := "Not used in VS Code. Emitted in editors that do not support an interactive InfoView (e.g. Emacs) and interactive tests."
@@ -394,7 +398,7 @@ def protocolOverview : Array MessageOverview := #[
   .request {
     method := "$/lean/plainTermGoal"
     direction := .clientToServer
-    kind := .leanSpecificMethod
+    kinds := #[.leanSpecificMethod]
     parameterType := PlainTermGoalParams
     responseType := Option PlainTermGoal
     description := "Not used in VS Code. Emitted in editors that do not support an interactive InfoView (e.g. Emacs) and interactive tests."
@@ -402,7 +406,7 @@ def protocolOverview : Array MessageOverview := #[
   .request {
     method := "textDocument/waitForDiagnostics"
     direction := .clientToServer
-    kind := .leanSpecificMethod
+    kinds := #[.leanSpecificMethod]
     parameterType := WaitForDiagnosticsParams
     responseType := WaitForDiagnostics
     description := "Not used in the editor. Emitted in interactive tests to wait for all diagnostics up to a given point."
@@ -410,7 +414,7 @@ def protocolOverview : Array MessageOverview := #[
   .request {
     method := "$/lean/waitForILeans"
     direction := .clientToServer
-    kind := .leanSpecificMethod
+    kinds := #[.leanSpecificMethod]
     parameterType := WaitForILeansParams
     responseType := WaitForILeans
     description := "Not used in the editor. Emitted in interactive tests to wait for all .ileans in the project and the .ilean of the given file to be loaded."
@@ -418,7 +422,7 @@ def protocolOverview : Array MessageOverview := #[
   .request {
     method := "$/lean/rpc/connect"
     direction := .clientToServer
-    kind := .leanSpecificMethod
+    kinds := #[.leanSpecificMethod]
     parameterType := RpcConnectParams
     responseType := RpcConnected
     description := "Emitted in VS Code when an RPC session for InfoView interactivity is initially set up."
@@ -426,21 +430,21 @@ def protocolOverview : Array MessageOverview := #[
   .notification {
     method := "$/lean/rpc/release"
     direction := .clientToServer
-    kind := .leanSpecificMethod
+    kinds := #[.leanSpecificMethod]
     parameterType := RpcReleaseParams
     description := "Emitted in VS Code when an RPC object in the server (the lifecycle of which is managed by the client) is freed by the client."
   },
   .notification {
     method := "$/lean/rpc/keepAlive"
     direction := .clientToServer
-    kind := .leanSpecificMethod
+    kinds := #[.leanSpecificMethod]
     parameterType := RpcKeepAliveParams
     description := "Emitted periodically in VS Code to signal that the RPC client has not disconnected yet to keep the RPC session alive."
   },
   .request {
     method := "$/lean/rpc/call"
     direction := .clientToServer
-    kind := .leanSpecificMethod
+    kinds := #[.leanSpecificMethod]
     parameterType := RpcCallParams
     responseType := Json
     description := "Emitted in VS Code when an RPC method is called. `RpcCallParams.method` and `RpcCallParams.params` can be any of the builtin `.rpcRequest`s described in this overview or any custom RPC methods tagged with `@[server_rpc_method]` that can be set up for use in the widget system."