From 23c9571ea6e1893bf64617900f9f987818021203 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Wed, 20 Dec 2023 10:09:10 +0100 Subject: [PATCH] Support snippet edits in code actions and workspace edits (#375) * feat: support extended WorkspaceEdit * chore: lint * chore: comment --- .eslintrc.js | 2 +- lean4-infoview/src/infoview/messages.tsx | 4 +- vscode-lean4/src/utils/converters.ts | 94 +++++++++++++++++++++--- 3 files changed, 87 insertions(+), 13 deletions(-) diff --git a/.eslintrc.js b/.eslintrc.js index 2b9c136c0..3d62910a3 100644 --- a/.eslintrc.js +++ b/.eslintrc.js @@ -61,7 +61,7 @@ module.exports = { "@typescript-eslint/no-explicit-any": "off", "@typescript-eslint/no-misused-new": "error", "@typescript-eslint/no-unused-vars": "off", - "@typescript-eslint/no-namespace": "error", + "@typescript-eslint/no-namespace": "off", "@typescript-eslint/no-parameter-properties": "off", "@typescript-eslint/no-inferrable-types": "off", "@typescript-eslint/no-use-before-define": "off", diff --git a/lean4-infoview/src/infoview/messages.tsx b/lean4-infoview/src/infoview/messages.tsx index 97fa034a2..398153302 100644 --- a/lean4-infoview/src/infoview/messages.tsx +++ b/lean4-infoview/src/infoview/messages.tsx @@ -175,8 +175,8 @@ function AllMessagesBody({uri, messages, setNumDiags}: AllMessagesBodyProps) { setNumDiags(msgs.length) } void fn() - }, [messages]) - React.useEffect(() => () => /* Called on unmount. */ setNumDiags(undefined), []) + }, [messages, setNumDiags]) + React.useEffect(() => () => /* Called on unmount. */ setNumDiags(undefined), [setNumDiags]) if (msgs === undefined) return <>Loading messages... else return } diff --git a/vscode-lean4/src/utils/converters.ts b/vscode-lean4/src/utils/converters.ts index 85a11d433..e6998cd4c 100644 --- a/vscode-lean4/src/utils/converters.ts +++ b/vscode-lean4/src/utils/converters.ts @@ -10,42 +10,116 @@ * @module */ -import { createConverter as createP2CConverter } from 'vscode-languageclient/lib/common/protocolConverter'; -import { createConverter as createC2PConverter } from 'vscode-languageclient/lib/common/codeConverter'; +import { createConverter as createP2CConverter } from 'vscode-languageclient/lib/common/protocolConverter' +import { createConverter as createC2PConverter } from 'vscode-languageclient/lib/common/codeConverter' +import * as async from 'vscode-languageclient/lib/common/utils/async' import * as ls from 'vscode-languageserver-protocol' import * as code from 'vscode' -import { Code2ProtocolConverter, Protocol2CodeConverter } from 'vscode-languageclient'; +import { Code2ProtocolConverter, Protocol2CodeConverter } from 'vscode-languageclient' interface Lean4Diagnostic extends ls.Diagnostic { fullRange: ls.Range; } +interface SnippetTextEdit extends ls.TextEdit { + leanExtSnippet: { value: string } +} + +namespace SnippetTextEdit { + export function is(value: any): value is SnippetTextEdit { + if (!ls.TextEdit.is(value)) return false + if (!('leanExtSnippet' in value)) return false + const snip = value.leanExtSnippet + if (snip === null || typeof snip !== 'object') return false + if (!('value' in snip)) return false + if (typeof snip.value !== 'string' && !(snip.value instanceof String)) return false + return true + } +} + export const p2cConverter = createP2CConverter(undefined, true, true) export const c2pConverter = createC2PConverter(undefined) export function patchConverters(p2cConverter: Protocol2CodeConverter, c2pConverter: Code2ProtocolConverter) { // eslint-disable-next-line @typescript-eslint/unbound-method - const oldAsDiagnostic = p2cConverter.asDiagnostic + const oldP2cAsDiagnostic = p2cConverter.asDiagnostic p2cConverter.asDiagnostic = function (protDiag: Lean4Diagnostic): code.Diagnostic { if (!protDiag.message) { // Fixes: Notification handler 'textDocument/publishDiagnostics' failed with message: message must be set protDiag.message = ' '; } - const diag = oldAsDiagnostic.apply(this, [protDiag]) + const diag = oldP2cAsDiagnostic.apply(this, [protDiag]) diag.fullRange = p2cConverter.asRange(protDiag.fullRange) return diag } - p2cConverter.asDiagnostics = async (diags) => diags.map(d => p2cConverter.asDiagnostic(d)) - + // 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 - const c2pAsDiagnostic = c2pConverter.asDiagnostic + const oldC2pAsDiagnostic = c2pConverter.asDiagnostic c2pConverter.asDiagnostic = function (diag: code.Diagnostic & {fullRange: code.Range}): Lean4Diagnostic { - const protDiag = c2pAsDiagnostic.apply(this, [diag]) + const protDiag = oldC2pAsDiagnostic.apply(this, [diag]) protDiag.fullRange = c2pConverter.asRange(diag.fullRange) return protDiag } - c2pConverter.asDiagnostics = async (diags) => diags.map(d => c2pConverter.asDiagnostic(d)) + c2pConverter.asDiagnostics = async (diags, token) => async.map(diags, d => c2pConverter.asDiagnostic(d), token) + + // eslint-disable-next-line @typescript-eslint/unbound-method + const oldP2CAsWorkspaceEdit = p2cConverter.asWorkspaceEdit + p2cConverter.asWorkspaceEdit = async function (item: ls.WorkspaceEdit | null | undefined, token?: code.CancellationToken) { + if (item === undefined || item === null) return undefined + if (item.documentChanges) { + // 1. Preprocess `documentChanges` by filtering out snippet edits + // which we support as a Lean-specific extension. + // 2. Create a `WorkspaceEdit` using the default function + // which does not take snippet edits into account. + // 3. Append the snippet edits. + // Note that this may permute the relative ordering of snippet edits and text edits, + // 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 newItem = { ...item, documentChanges } + const result: code.WorkspaceEdit = await oldP2CAsWorkspaceEdit.apply(this, [newItem, token]) + for (const [uri, snippetEdits] of snippetChanges) + result.set(uri, snippetEdits) + return result + } + return oldP2CAsWorkspaceEdit.apply(this, [item, token]) + } + + // eslint-disable-next-line @typescript-eslint/unbound-method + const oldP2cAsCodeAction = p2cConverter.asCodeAction + p2cConverter.asCodeAction = async function (item: ls.CodeAction | null | undefined, token?: code.CancellationToken) { + 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) + } + return oldP2cAsCodeAction.apply(this, [item, token]) + } + + // 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. } patchConverters(p2cConverter, c2pConverter)