fix: abbreviation rewriter disposal race condition (#492)

leanprover · Jul 1, 2024 · 3a4e4bb · 3a4e4bb
1 parent a6bd9cf
commit 3a4e4bb
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 5 deletions.
diff --git 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
@@ -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
     }