Abbreviations leave trailing spaces/don't advance cursor about vscode-lean4

[mhuisi]

#391 should mitigate the Vim plugin issue.

[Vtec234]

This might be a different issue, but possibly related to #241.

[PatrickMassot]

I don't know about #241 but I can reproduce this issue on a fully local setup. I has been annoying me for some time but, as Andrew says, it is no fully deterministic. I think it happens more often if you type slowly. And it has nothing to do with space. Let me record an example where I keep typing ,a+ (knowing that , is my input leader).

[girving]

Now that this is fixed, I have much worse cursor position problems when using the v0.0.125 plugin: the cursor position often goes several steps to the right on top of other text.

vscode-lean-bug.mov

Zulip thread

Should I file this as a separate bug? The timing is suspicious, so it's possible this new bug is related to the fixes.

[girving]

The difference seems to be that I am also using the Vim plugin, specifically Vim plugin v1.27.2.

[girving]

Switching to the Neovim vscode plugin fixes it.