leanprover/vscode-lean#263

Stream: PR reviews

[Eric Wieser]

It's only a partial fix, but this changes the \-shortcut bug from super-annoying to still-quite-annoying. cc @Henning Dieterichs.

[Eric Wieser]

To summarize, the bug is that if you type \tol too quickly you end up with \t|ol where | is the cursor

[Eric Wieser]

With this fix, you end up with \tol | instead which is at least easier to clean up and try again

[Henning Dieterichs]

Sorry, I never experienced the \-shortcut to be annoying . Is there a good way to reproduce this issue? Is this related to the eager replacement or does it also happen without it? Did it happen in the old version?

[Eric Wieser]

It's only annoying when this bug hits, its otherwise great!

[Eric Wieser]

I find it happens most often when I'm editing a file early in mathlib and lean is trying to use all my CPU to build leaving not very much for vs-code

[Eric Wieser]

I don't think it did happen in the old version, but I'm not really sure and I think that had other bugs

[Eric Wieser]

My hunch is that this is all called by the setTimeout(..., 0)

[Eric Wieser]

I don't think vs-code makes any guarantees about how soon that will run, in particular it may not get a chance to run until after I've typed some more

[Eric Wieser]

Which means that any ranges which you had before the timeout might no longer be valid after the timeout

[Eric Wieser]

If that hunch is correct, you can debug this by replacing that 0 with something like 250 to simulate a slower vs-code