From 3a4e4bb94ebd02d40b56eef3effe891af49f01e5 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Mon, 1 Jul 2024 11:53:09 +0200 Subject: [PATCH] fix: abbreviation rewriter disposal race condition (#492) --- .../src/abbreviation/AbbreviationRewriterFeature.ts | 12 ++++++++---- .../src/abbreviation/VSCodeAbbreviationRewriter.ts | 6 +++++- 2 files changed, 13 insertions(+), 5 deletions(-) diff --git a/vscode-lean4/src/abbreviation/AbbreviationRewriterFeature.ts b/vscode-lean4/src/abbreviation/AbbreviationRewriterFeature.ts index 745cae19f..748fa4a93 100644 --- a/vscode-lean4/src/abbreviation/AbbreviationRewriterFeature.ts +++ b/vscode-lean4/src/abbreviation/AbbreviationRewriterFeature.ts @@ -61,12 +61,16 @@ export class AbbreviationRewriterFeature { } private async disposeActiveAbbreviationRewriter() { - if (this.activeAbbreviationRewriter === undefined) { + // This is necessary to prevent `disposeActiveAbbreviationRewriter` from racing with + // other assignments to `this.activeAbbreviationRewriter`. + const abbreviationRewriterToDispose = this.activeAbbreviationRewriter + this.activeAbbreviationRewriter = undefined + if (abbreviationRewriterToDispose === undefined) { return } - await this.activeAbbreviationRewriter.replaceAllTrackedAbbreviations() - this.activeAbbreviationRewriter.dispose() - this.activeAbbreviationRewriter = undefined + + await abbreviationRewriterToDispose.replaceAllTrackedAbbreviations() + abbreviationRewriterToDispose.dispose() } private async changedActiveTextEditor(activeTextEditor: TextEditor | undefined) { diff --git a/vscode-lean4/src/abbreviation/VSCodeAbbreviationRewriter.ts b/vscode-lean4/src/abbreviation/VSCodeAbbreviationRewriter.ts index 55601f701..d9b302fc5 100644 --- a/vscode-lean4/src/abbreviation/VSCodeAbbreviationRewriter.ts +++ b/vscode-lean4/src/abbreviation/VSCodeAbbreviationRewriter.ts @@ -123,7 +123,11 @@ export class VSCodeAbbreviationRewriter implements AbbreviationTextSource { retries++ } } catch (e) { - this.writeError('Error while replacing abbreviation: ' + e) + // The 'not possible on closed editors' error naturally occurs when we attempt to replace abbreviations as the user + // is switching away from the active tab. + if (!(e instanceof Error) || e.message !== 'TextEditor#edit not possible on closed editors') { + this.writeError('Error while replacing abbreviation: ' + e) + } } return ok }