From 5c3835693bd1edd8bed3b51970691dfc53e1f26e Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Mon, 13 Jan 2025 17:38:41 +0100
Subject: [PATCH] wait for changes to take effect before replacing
 abbreviations

---
 vscode-lean4/src/abbreviation/VSCodeAbbreviationRewriter.ts | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/vscode-lean4/src/abbreviation/VSCodeAbbreviationRewriter.ts b/vscode-lean4/src/abbreviation/VSCodeAbbreviationRewriter.ts
index d9b302fc5..7f57ddf71 100644
--- a/vscode-lean4/src/abbreviation/VSCodeAbbreviationRewriter.ts
+++ b/vscode-lean4/src/abbreviation/VSCodeAbbreviationRewriter.ts
@@ -59,6 +59,10 @@ export class VSCodeAbbreviationRewriter implements AbbreviationTextSource {
                     newText: changeEvent.text,
                 }))
                 this.rewriter.changeInput(changes)
+
+                // Wait for changes to take effect
+                await new Promise(resolve => setTimeout(resolve, 0))
+
                 await this.rewriter.triggerAbbreviationReplacement()
 
                 this.updateState()