VSCode annoyance

Stream: general

[Trebor Huang]

I noticed when I press the keys \, r and space, sometimes the space is inserted after the cursor, so I'm left with →| instead of → |. This is getting annoying when I type fast. Is this a known problem? What might be the cause, and how can I fix it?

[Martin Dvořák]

Press tab if you want to type just the symbol.

[Reid Barton]

Presumably Trebor also wants the space.

[Martin Dvořák]

Then I cannot help. On my computer, the keypress sequence \r always leaves me with → | afair.

[Trebor Huang]

I can circumvent the problem if I type \ r tab and then space. It's just a little annoying, and certainly a bug.

[Martin Dvořák]

Yes, it sounds annoying.

[Damiano Testa]

Could it be that your tab is set to print one or two spaces, depending on whether you are on an even/odd column? Like Martin, I get pretty consistent results with typing \r , in that the space seems to always be there, but seem to get a dependency on position with tab (that I usually do not use).
EDIT: sorry, I see that you use space already, I misunderstood.

[Reid Barton]

Is it possible some other input method is competing to process your input?

[Arthur Paulino]

I confirm this bug. This is a new bug. I've been experiencing it for the past 3 weeks or so

[Eric Wieser]

Is this for lean 3 or lean 4?

[Logan Murphy]

I've noticed it for Lean4 for various greek letters

[Wojciech Nawrocki]

I am not sure if this is what you are experiencing, but in remote setups this is a known issue. Latency on a local setup should not be bad enough to trigger it, but in general yes, the abbreviations provider could use a refactoring.

[Andrew Shulaev]

I have an attempt for a fix: https://github.com/leanprover/vscode-lean/compare/master...ddrone:vscode-lean:replacement-fix
This unfortunately does not handle correctly the case of "abbreviations" like \- that expand into strings that are shorter than the original character sequence. I don't really have enough context about VSCode plugin development in order to complete it; but if someone has more experience and will be willing to walk me through the existing code I can try to do another attempt.

[Gabriel Ebner]

I'm now running into this constantly as well. From what I can tell, it appeared after a recent vscode upgrade.

[Gabriel Ebner]

(I can repro the issue with both local and "remote" (container) connections.)

[Arthur Paulino]

Here's a cue: I use Patrick's trick and my escaping key is ,. And I can reproduce the issue even without any unicode substitution taking place. Hitting , and then spacebar does this weird behavior of putting the cursor after the comma but also inputting an empty space after the caret:

abcd|.
    ^ caret here

After the bug:

      v empty space here
abcd,| .
     ^ caret here

[Andrew Shulaev]

So I haven't been able to get a proper fix, but I did find a workaround that leads to less annoying experience: if you're used to type \lam and then press Space to get annoyed at the fact that the space character is going to appear on the right side of the cursor, you can change the keyboard shortcut of lean.input.convert to Space. Now the Space input is going to be considered as triggering the explicit action of replacement, and the space character would not appear at all, and you'll have to press it twice. Still annoying, but IMO less annoying than the status quo.