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

fix: make applyEdit optional in WorkspaceClientCapabilities of LSP (#5224)

Browse source 
The `applyEdit` field should be optional in
`WorkspaceClientCapabilities` by the LSP spec and some clients don't
populate it in requests

Closes #4541
This commit is contained in:
Jerry Wu 2024-10-16 16:38:11 +08:00 • committed by GitHub
parent 19e06acc65
commit b333de1a36
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 17 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Data/Lsp/Capabilities.lean
View file

@ -54,7 +54,7 @@ structure WorkspaceEditClientCapabilities where
deriving ToJson, FromJson
structure WorkspaceClientCapabilities where
applyEdit: Bool
applyEdit? : Option Bool := none
workspaceEdit? : Option WorkspaceEditClientCapabilities := none
deriving ToJson, FromJson

13
tests/lean/server/init_exit_with_zed.lean Normal file
View file

@ -0,0 +1,13 @@
import Lean.Data.Lsp
open IO Lean Lsp
def main : IO Unit := do
Ipc.runWith (←IO.appPath) #["--server"] do
let hIn ← Ipc.stdin
hIn.write (←FS.readBinFile "init_zed_0_150_4.log")
hIn.flush
let initResp ← Ipc.readResponseAs 0 InitializeResult
Ipc.writeNotification ⟨"initialized", InitializedParams.mk⟩
Ipc.shutdown 1
discard Ipc.waitForExit

3
tests/lean/server/init_zed_0_150_4.log Normal file
View file

@ -0,0 +1,3 @@
Content-Length: 1858
{"params":{"workspaceFolders":[{"uri":"file:///tmp","name":""}],"rootUri":"file:///tmp","processId":null,"clientInfo":{"version":"0.150.4","name":"Zed"},"capabilities":{"workspace":{"workspaceFolders":true,"workspaceEdit":{"snippetEditSupport":true,"resourceOperations":["create","rename","delete"],"documentChanges":true},"symbol":{},"inlayHint":{"refreshSupport":true},"didChangeWatchedFiles":{"relativePatternSupport":true,"dynamicRegistration":true},"didChangeConfiguration":{"dynamicRegistration":true},"diagnostic":{},"configuration":true},"window":{"workDoneProgress":true},"textDocument":{"synchronization":{"didSave":true},"signatureHelp":{"signatureInformation":{"parameterInformation":{"labelOffsetSupport":true},"documentationFormat":["markdown","plaintext"],"activeParameterSupport":true}},"rename":{"prepareSupport":true},"rangeFormatting":{"dynamicRegistration":true},"publishDiagnostics":{"relatedInformation":true},"onTypeFormatting":{"dynamicRegistration":true},"inlayHint":{"resolveSupport":{"properties":["textEdits","tooltip","label.tooltip","label.location","label.command"]},"dynamicRegistration":false},"hover":{"contentFormat":["markdown"]},"formatting":{"dynamicRegistration":true},"definition":{"linkSupport":true},"completion":{"contextSupport":true,"completionList":{"itemDefaults":["commitCharacters","editRange","insertTextMode","data"]},"completionItem":{"snippetSupport":true,"resolveSupport":{"properties":["documentation","additionalTextEdits"]},"labelDetailsSupport":true,"insertReplaceSupport":true}},"codeAction":{"resolveSupport":{"properties":["kind","diagnostics","isPreferred","disabled","edit","command"]},"dataSupport":true,"codeActionLiteralSupport":{"codeActionKind":{"valueSet":["refactor","quickfix","source"]}}}},"experimental":{"serverStatusNotification":true}}},"method":"initialize","jsonrpc":"2.0","id":0}