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 }