From 297d06fc0c040a48d9f3cb183a8f613ee8d478dd Mon Sep 17 00:00:00 2001
From: "E.W.Ayers" <edward.ayers@outlook.com>
Date: Thu, 29 Sep 2022 15:04:11 +0100
Subject: [PATCH] fix: issue where code action was not running

---
 src/Lean/Data/Lsp/Basic.lean                   | 11 ++++++++++-
 src/Lean/Server/CodeActions.lean               |  3 ---
 src/Lean/Server/Watchdog.lean                  |  5 ++++-
 tests/lean/interactive/codeaction.lean         |  3 +--
 .../interactive/codeaction.lean.expected.out   | 18 +++++++++---------
 5 files changed, 24 insertions(+), 16 deletions(-)

diff --git a/src/Lean/Data/Lsp/Basic.lean b/src/Lean/Data/Lsp/Basic.lean
index 8cb8e799e6..b69e659904 100644
--- a/src/Lean/Data/Lsp/Basic.lean
+++ b/src/Lean/Data/Lsp/Basic.lean
@@ -245,7 +245,16 @@ def ofTextDocumentEdit (e : TextDocumentEdit) : WorkspaceEdit :=
   { documentChanges := #[DocumentChange.edit e]}
 
 def ofTextEdit (uri : DocumentUri) (te : TextEdit) : WorkspaceEdit :=
-  { changes := RBMap.empty.insert uri #[te]}
+  /- [note], there is a bug in vscode where not including the version will cause an error,
+  even though the version field is not used to validate the change.
+
+  References:
+  - [a fix in the wild](https://github.com/stylelint/vscode-stylelint/pull/330/files).
+    Note that the version field needs to be present, even if the value is `undefined`.
+  - [angry comment](https://github.com/tsqllint/tsqllint-vscode-extension/blob/727026fce9f8c6a33d113373666d0776f8f6c23c/server/src/server.ts#L70)
+  -/
+  let doc := {uri, version? := some 0}
+  ofTextDocumentEdit { textDocument := doc, edits := #[te]}
 
 end WorkspaceEdit
 
diff --git a/src/Lean/Server/CodeActions.lean b/src/Lean/Server/CodeActions.lean
index e2870854b5..da8fc88ecd 100644
--- a/src/Lean/Server/CodeActions.lean
+++ b/src/Lean/Server/CodeActions.lean
@@ -36,9 +36,6 @@ Rather than run the heavy ML computation in the CodeActionProvider, you could su
 def CodeActionProvider := CodeActionParams → RequestM (RequestTask (Array CodeAction))
 deriving instance Inhabited for CodeActionProvider
 
-def CodeActionResolver := CodeAction → RequestM (RequestTask CodeAction)
-deriving instance Inhabited for CodeActionResolver
-
 builtin_initialize codeActionProviderExt : SimplePersistentEnvExtension Name NameSet ← registerSimplePersistentEnvExtension {
   name := `codeActionProviderExt,
   addImportedFn := fun nss => nss.foldl (fun acc ns => ns.foldl NameSet.insert acc) ∅
diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean
index ee1627e18b..798624ad09 100644
--- a/src/Lean/Server/Watchdog.lean
+++ b/src/Lean/Server/Watchdog.lean
@@ -690,7 +690,10 @@ def mkLeanServerCapabilities : ServerCapabilities := {
     full  := true
     range := true
   }
-  codeActionProvider? := some {  }
+  codeActionProvider? := some {
+    resolveProvider? := true,
+    codeActionKinds? := some #["quickfix", "refactor"]
+  }
 }
 
 def initAndRunWatchdogAux : ServerM Unit := do
diff --git a/tests/lean/interactive/codeaction.lean b/tests/lean/interactive/codeaction.lean
index 890938f91a..dbc59ccf73 100644
--- a/tests/lean/interactive/codeaction.lean
+++ b/tests/lean/interactive/codeaction.lean
@@ -11,8 +11,7 @@ def helloProvider : CodeActionProvider := fun (params : CodeActionParams) => do
     edit? := WorkspaceEdit.ofTextEdit uri {
       range := params.range,
       newText := "hello!!!",
-    },
-    data := {uri}
+    }
   }]
 
 theorem asdf : (x : Nat) → x = x := by
diff --git a/tests/lean/interactive/codeaction.lean.expected.out b/tests/lean/interactive/codeaction.lean.expected.out
index 1e7d65ab88..941bf4e063 100644
--- a/tests/lean/interactive/codeaction.lean.expected.out
+++ b/tests/lean/interactive/codeaction.lean.expected.out
@@ -1,12 +1,12 @@
 {"title": "hello world",
  "kind": "quickfix",
  "edit":
- {"documentChanges": [],
-  "changes":
-  {"file://codeaction.lean":
-   [{"range":
-     {"start": {"line": 18, "character": 4},
-      "end": {"line": 18, "character": 4}},
-     "newText": "hello!!!"}]},
-  "changeAnnotations": {}},
- "data": {"uri": "file://codeaction.lean"}}
+ {"documentChanges":
+  [{"textDocument": {"version": 0, "uri": "file://codeaction.lean"},
+    "edits":
+    [{"range":
+      {"start": {"line": 17, "character": 4},
+       "end": {"line": 17, "character": 4}},
+      "newText": "hello!!!"}]}],
+  "changes": {},
+  "changeAnnotations": {}}}