fix: CodeAction converters (#777)

Vtec234 · web-flow · commit 0b629572b71d · 2026-04-27T10:06:21.000-04:00
This PR ensures completeness of `patchConverters` - all conversion functions that touch Lean-specific data are now patched. Fixes an issue with snippet edits [reported on Zulip](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Snippets.20in.20code.20actions.3F). Also adds a `prebuild` step that ensures we don't bump `vscode-languageclient` without first fixing up the converters.
diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json
@@ -1843,6 +1843,7 @@
     "main": "./dist/extension",
     "scripts": {
         "vscode:prepublish": "webpack --env production",
+        "prebuild": "node -e \"if (require('vscode-languageclient/package.json').version !== '9.0.1') { console.error('To update vscode-languageclient, fix converters.ts and then require the new version here.'); process.exit(1) }\"",
         "build": "webpack --env production",
         "build:dev": "webpack --env development",
         "watch": "webpack --env development --watch",
@@ -1862,7 +1863,7 @@
         "markdown-it": "^14.1.0",
         "markdown-it-anchor": "^9.0.1",
         "semver": "^7.6.0",
-        "vscode-languageclient": "^9.0.1",
+        "vscode-languageclient": "9.0.1",
         "zod": "^3.22.4"
     },
     "devDependencies": {
diff --git a/vscode-lean4/src/utils/converters.ts b/vscode-lean4/src/utils/converters.ts
@@ -95,10 +95,20 @@ export function setDependencyBuildMode(
 export const p2cConverter = createP2CConverter(undefined, true, true)
 export const c2pConverter = createC2PConverter(undefined)
 
+/** Patch the given converters to support Lean-specific extensions to LSP datatypes.
+ *
+ * Patches need to be updated when bumping vscode-languageclient. */
 export function patchConverters(p2cConverter: Protocol2CodeConverter, c2pConverter: Code2ProtocolConverter) {
+    // Although converters are objects,
+    // their methods refer to other methods by closure-captured local binding rather than via `this`,
+    // so it doesn't suffice to patch a method: we must also patch any callers.
+    // For example, we patch `asDiagnostics` to invoke our version of `asDiagnostic`.
+
     // eslint-disable-next-line @typescript-eslint/unbound-method
     const oldP2cAsDiagnostic = p2cConverter.asDiagnostic
-    p2cConverter.asDiagnostic = function (protDiag: LeanDiagnostic): code.Diagnostic {
+    p2cConverter.asDiagnostic = function (
+        protDiag: LeanDiagnostic,
+    ): code.Diagnostic & { fullRange?: code.Range; isSilent?: boolean; leanTags?: LeanTag[] } {
         if (!protDiag.message) {
             // Fixes: Notification handler 'textDocument/publishDiagnostics' failed with message: message must be set
             protDiag.message = ' '
@@ -109,9 +119,6 @@ export function patchConverters(p2cConverter: Protocol2CodeConverter, c2pConvert
         diag.isSilent = protDiag.isSilent
         return diag
     }
-    // The original definition refers to `asDiagnostic` as a local function
-    // rather than as a member of `Protocol2CodeConverter`,
-    // so we need to overwrite it, too.
     p2cConverter.asDiagnostics = async (diags, token) => async.map(diags, d => p2cConverter.asDiagnostic(d), token)
 
     // eslint-disable-next-line @typescript-eslint/unbound-method
@@ -126,20 +133,18 @@ export function patchConverters(p2cConverter: Protocol2CodeConverter, c2pConvert
         return protDiag
     }
     c2pConverter.asDiagnostics = async (diags, token) => async.map(diags, d => c2pConverter.asDiagnostic(d), token)
+    c2pConverter.asDiagnosticsSync = diags => diags.map(d => c2pConverter.asDiagnostic(d))
 
     // eslint-disable-next-line @typescript-eslint/unbound-method
     const oldC2pAsOpenTextDocumentParams = c2pConverter.asOpenTextDocumentParams
-    c2pConverter.asOpenTextDocumentParams = doc => {
+    c2pConverter.asOpenTextDocumentParams = function (doc) {
         const params = oldC2pAsOpenTextDocumentParams.apply(this, [doc])
         return setDependencyBuildMode(params, 'never')
     }
 
     // eslint-disable-next-line @typescript-eslint/unbound-method
     const oldP2CAsWorkspaceEdit = p2cConverter.asWorkspaceEdit
-    p2cConverter.asWorkspaceEdit = async function (
-        item: ls.WorkspaceEdit | null | undefined,
-        token?: code.CancellationToken,
-    ) {
+    p2cConverter.asWorkspaceEdit = async function (item, token) {
         if (item === undefined || item === null) return undefined
         if (item.documentChanges) {
             // 1. Preprocess `documentChanges` by filtering out snippet edits
@@ -151,52 +156,94 @@ export function patchConverters(p2cConverter: Protocol2CodeConverter, c2pConvert
             // so users cannot rely on it;
             // but a mix of both doesn't seem to work in VSCode anyway as of 1.84.2.
             const snippetChanges: [code.Uri, code.SnippetTextEdit[]][] = []
-            const documentChanges = await async.map(
-                item.documentChanges,
-                change => {
-                    if (!ls.TextDocumentEdit.is(change)) return true
-                    const uri = code.Uri.parse(change.textDocument.uri)
-                    const snippetEdits: code.SnippetTextEdit[] = []
-                    const edits = change.edits.filter(edit => {
-                        if (!SnippetTextEdit.is(edit)) return true
-                        const range = p2cConverter.asRange(edit.range)
-                        snippetEdits.push(
-                            new code.SnippetTextEdit(range, new code.SnippetString(edit.leanExtSnippet.value)),
-                        )
-                        return false
-                    })
-                    snippetChanges.push([uri, snippetEdits])
-                    return { ...change, edits }
-                },
-                token,
-            )
+            const documentChanges: (ls.TextDocumentEdit | ls.CreateFile | ls.RenameFile | ls.DeleteFile)[] =
+                await async.map(
+                    item.documentChanges,
+                    change => {
+                        if (!ls.TextDocumentEdit.is(change)) return change
+                        const uri = code.Uri.parse(change.textDocument.uri)
+                        const snippetEdits: code.SnippetTextEdit[] = []
+                        const edits = change.edits.filter(edit => {
+                            if (!SnippetTextEdit.is(edit)) return true
+                            const range = p2cConverter.asRange(edit.range)
+                            snippetEdits.push(
+                                new code.SnippetTextEdit(range, new code.SnippetString(edit.leanExtSnippet.value)),
+                            )
+                            return false
+                        })
+                        snippetChanges.push([uri, snippetEdits])
+                        return { ...change, edits }
+                    },
+                    token,
+                )
             const newItem = { ...item, documentChanges }
             const result: code.WorkspaceEdit = await oldP2CAsWorkspaceEdit.apply(this, [newItem, token])
+            // Despite the name and docstring,
+            // `WorkspaceEdit.set` appends `snippetEdits` rather than replacing what's already there.
             for (const [uri, snippetEdits] of snippetChanges) result.set(uri, snippetEdits)
             return result
         }
         return oldP2CAsWorkspaceEdit.apply(this, [item, token])
     }
 
+    // Note: as of vscode-languageclient 9.0.1, there is no c2pConverter.asWorkspaceEdit.
+    // This is possibly because code.WorkspaceEdit supports features
+    // that cannot be encoded in ls.WorkspaceEdit.
+
     // eslint-disable-next-line @typescript-eslint/unbound-method
     const oldP2cAsCodeAction = p2cConverter.asCodeAction
-    p2cConverter.asCodeAction = async function (
-        item: ls.CodeAction | null | undefined,
-        token?: code.CancellationToken,
-    ) {
+    p2cConverter.asCodeAction = async function (item, token) {
         if (item === undefined || item === null) return undefined
-        if (item.edit || item.diagnostics) {
-            const result: code.CodeAction = await oldP2cAsCodeAction.apply(this, [item, token])
-            if (item.diagnostics !== undefined)
-                result.diagnostics = await p2cConverter.asDiagnostics(item.diagnostics, token)
-            if (item.edit) result.edit = await p2cConverter.asWorkspaceEdit(item.edit, token)
+        const result: code.CodeAction = await oldP2cAsCodeAction.apply(this, [item, token])
+        if (item.diagnostics !== undefined)
+            // Call our modified asDiagnostics, defined above. Upstream calls `asDiagnosticsSync`.
+            result.diagnostics = await p2cConverter.asDiagnostics(item.diagnostics, token)
+        if (item.edit !== undefined) result.edit = await p2cConverter.asWorkspaceEdit(item.edit, token)
+        return result as any /* tsc incompleteness */
+    }
+    p2cConverter.asCodeActionResult = async (items, token) =>
+        async.mapAsync(
+            items,
+            async item => (ls.Command.is(item) ? p2cConverter.asCommand(item) : p2cConverter.asCodeAction(item, token)),
+            token,
+        )
+
+    // eslint-disable-next-line @typescript-eslint/unbound-method
+    const oldC2pAsCodeAction = c2pConverter.asCodeAction
+    c2pConverter.asCodeAction = async function (item, token) {
+        const result: ls.CodeAction = await oldC2pAsCodeAction.apply(this, [item, token])
+        if (item.diagnostics !== undefined)
+            result.diagnostics = await c2pConverter.asDiagnostics(item.diagnostics, token)
+        return result
+    }
+
+    // eslint-disable-next-line @typescript-eslint/unbound-method
+    const oldC2pAsCodeActionSync = c2pConverter.asCodeActionSync
+    c2pConverter.asCodeActionSync = function (item) {
+        const result: ls.CodeAction = oldC2pAsCodeActionSync.apply(this, [item])
+        if (item.diagnostics !== undefined) result.diagnostics = c2pConverter.asDiagnosticsSync(item.diagnostics)
+        return result
+    }
+
+    // eslint-disable-next-line @typescript-eslint/unbound-method
+    const oldC2pAsCodeActionContext = c2pConverter.asCodeActionContext
+    c2pConverter.asCodeActionContext = async function (context, token) {
+        const result = await oldC2pAsCodeActionContext.apply(this, [context, token])
+        if (context.diagnostics !== undefined) {
+            result.diagnostics = await c2pConverter.asDiagnostics(context.diagnostics as code.Diagnostic[], token)
         }
-        return oldP2cAsCodeAction.apply(this, [item, token])
+        return result
     }
 
-    // Note: as of 2023-12-10, there is no c2pConverter.asWorkspaceEdit.
-    // This is possibly because code.WorkspaceEdit supports features
-    // that cannot be encoded in ls.WorkspaceEdit.
+    // eslint-disable-next-line @typescript-eslint/unbound-method
+    const oldC2pAsCodeActionContextSync = c2pConverter.asCodeActionContextSync
+    c2pConverter.asCodeActionContextSync = function (context) {
+        const result = oldC2pAsCodeActionContextSync.apply(this, [context])
+        if (context.diagnostics !== undefined) {
+            result.diagnostics = c2pConverter.asDiagnosticsSync(context.diagnostics as code.Diagnostic[])
+        }
+        return result
+    }
 }
 
 patchConverters(p2cConverter, c2pConverter)
