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 ff0b6df + 5c38356 commit b1827b3
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 b1827b3

Please sign in to comment.