From 570ffd88a12c8b62bdeda23b70a5203de666da80 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Tue, 12 Dec 2023 21:32:13 +0100 Subject: [PATCH 1/3] feat: support extended WorkspaceEdit --- vscode-lean4/src/utils/converters.ts | 94 +++++++++++++++++++++++++--- 1 file changed, 84 insertions(+), 10 deletions(-) diff --git a/vscode-lean4/src/utils/converters.ts b/vscode-lean4/src/utils/converters.ts index 85a11d433..89a7693ac 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, p2cConverter.asDiagnostic, 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, c2pConverter.asDiagnostic, token) + + 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]) + } + + const oldP2cAsCodeAction = p2cConverter.asCodeAction + p2cConverter.asCodeAction = async function (item: ls.CodeAction | null | undefined, token?: code.CancellationToken) { + // if (item.diagnostics !== undefined) { result.diagnostics = asDiagnosticsSync(item.diagnostics); } + // if (item.edit !== undefined) { result.edit = await asWorkspaceEdit(item.edit, 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) + } + 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) From fd5bff1deb34aa9d67e065ed09feaa38e30a4faf Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Tue, 12 Dec 2023 21:51:39 +0100 Subject: [PATCH 2/3] chore: lint --- .eslintrc.js | 2 +- lean4-infoview/src/infoview/messages.tsx | 4 ++-- vscode-lean4/src/utils/converters.ts | 6 ++++-- 3 files changed, 7 insertions(+), 5 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 89a7693ac..6fd575028 100644 --- a/vscode-lean4/src/utils/converters.ts +++ b/vscode-lean4/src/utils/converters.ts @@ -55,7 +55,7 @@ export function patchConverters(p2cConverter: Protocol2CodeConverter, c2pConvert // 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, p2cConverter.asDiagnostic, token) + p2cConverter.asDiagnostics = async (diags, token) => async.map(diags, d => p2cConverter.asDiagnostic(d), token) // eslint-disable-next-line @typescript-eslint/unbound-method const oldC2pAsDiagnostic = c2pConverter.asDiagnostic @@ -64,8 +64,9 @@ export function patchConverters(p2cConverter: Protocol2CodeConverter, c2pConvert protDiag.fullRange = c2pConverter.asRange(diag.fullRange) return protDiag } - c2pConverter.asDiagnostics = async (diags, token) => async.map(diags, c2pConverter.asDiagnostic, token) + 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 @@ -104,6 +105,7 @@ export function patchConverters(p2cConverter: Protocol2CodeConverter, c2pConvert 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.diagnostics !== undefined) { result.diagnostics = asDiagnosticsSync(item.diagnostics); } From 93d22fae627136a653a7c4fef7875c82e63fef98 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Tue, 12 Dec 2023 23:20:07 +0100 Subject: [PATCH 3/3] chore: comment --- vscode-lean4/src/utils/converters.ts | 2 -- 1 file changed, 2 deletions(-) diff --git a/vscode-lean4/src/utils/converters.ts b/vscode-lean4/src/utils/converters.ts index 6fd575028..e6998cd4c 100644 --- a/vscode-lean4/src/utils/converters.ts +++ b/vscode-lean4/src/utils/converters.ts @@ -108,8 +108,6 @@ export function patchConverters(p2cConverter: Protocol2CodeConverter, c2pConvert // 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.diagnostics !== undefined) { result.diagnostics = asDiagnosticsSync(item.diagnostics); } - // if (item.edit !== undefined) { result.edit = await asWorkspaceEdit(item.edit, token); } if (item === undefined || item === null) return undefined if (item.edit || item.diagnostics) { const result: code.CodeAction = await oldP2cAsCodeAction.apply(this, [item, token])