Skip to content

Commit

Permalink
Merge branch 'spacefix' into monaco
Browse files Browse the repository at this point in the history
  • Loading branch information
joneugster committed Jan 13, 2025
2 parents 6867d67 + 5c38356 commit 7273f20
Showing 1 changed file with 4 additions and 0 deletions.
4 changes: 4 additions & 0 deletions vscode-lean4/src/abbreviation/VSCodeAbbreviationRewriter.ts
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,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()
Expand Down

0 comments on commit 7273f20

Please sign in to comment.