From b333de1a36df296b434d14132ffc736dfac4a420 Mon Sep 17 00:00:00 2001
From: Jerry Wu <netfirewall@gmail.com>
Date: Wed, 16 Oct 2024 16:38:11 +0800
Subject: [PATCH] fix: make applyEdit optional in WorkspaceClientCapabilities
 of LSP (#5224)

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

Closes #4541
---
 src/Lean/Data/Lsp/Capabilities.lean       |  2 +-
 tests/lean/server/init_exit_with_zed.lean | 13 +++++++++++++
 tests/lean/server/init_zed_0_150_4.log    |  3 +++
 3 files changed, 17 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/server/init_exit_with_zed.lean
 create mode 100644 tests/lean/server/init_zed_0_150_4.log

diff --git a/src/Lean/Data/Lsp/Capabilities.lean b/src/Lean/Data/Lsp/Capabilities.lean
index d4eb3c4409..6e07b2740f 100644
--- a/src/Lean/Data/Lsp/Capabilities.lean
+++ b/src/Lean/Data/Lsp/Capabilities.lean
@@ -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
 
diff --git a/tests/lean/server/init_exit_with_zed.lean b/tests/lean/server/init_exit_with_zed.lean
new file mode 100644
index 0000000000..3e3b42fd6a
--- /dev/null
+++ b/tests/lean/server/init_exit_with_zed.lean
@@ -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
diff --git a/tests/lean/server/init_zed_0_150_4.log b/tests/lean/server/init_zed_0_150_4.log
new file mode 100644
index 0000000000..538132a4a1
--- /dev/null
+++ b/tests/lean/server/init_zed_0_150_4.log
@@ -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}
\ No newline at end of file