VS code unicode autocompletion without adding space

Stream: new members

[Bryan Gin-ge Chen]

Currently if I want to type α₁ in VS Code, I type \a then hit space, and then hit backspace before typing \1+space again. Is there a way to do this without having to hit backspace all the time?

[Gabriel Ebner]

You can type \a\1 , and (\a\1: Type) works as well.

[Gabriel Ebner]

• Used to work, somehow it doesn't now.

[Patrick Massot]

This is why I tried to ask the same question a while ago. It's clearly the single most annoying thing in VScode

[Patrick Massot]

Do you use this when using the vim plugin?

[Bryan Gin-ge Chen]

Do you use this when using the vim plugin?

Yep, and for me that would be harder to give up than dealing with this annoyance.

[Patrick Massot]

I have this annoyance without the vim plugin

[Patrick Massot]

I once tried the vim plugin and decided it was unusable, but maybe I hesitate to give it another try. Since Gabriel didn't seem to know about this problem I suddenly hoped it wasn't there with the vim plugin

[Gabriel Ebner]

I only use the vim plugin and observe this problem as well.

[Bryan Gin-ge Chen]

An ideal solution for me would be some way to trigger the replacement without moving the cursor. I would like it if either "space" would not add a space when performing a replacement, or if there were some other keybinding that did precisely that.

[Gabriel Ebner]

So, \alpha\1\2\3 works again now. I believe this was silently broken due to an upstream change in vscode. Thanks for pointing it out!

[Gabriel Ebner]

An ideal solution for me would be some way to trigger the replacement without moving the cursor.

I am reluctant to reuse space for this. Ideas for other keybindings?

[Bryan Gin-ge Chen]

I am reluctant to reuse space for this. Ideas for other keybindings?

shift+space maybe?

[Patrick Massot]

why not tab, like in shell completion?

[Gabriel Ebner]

shift+space is crazy enough that hopefully nobody uses it yet. I'll try to add it.

[Gabriel Ebner]

@Patrick Massot tab already produces a... tab.

[Gabriel Ebner]

More seriously, it's hard to hijack a key just when the input mode is active. I can add a global keybinding for tab, but this is probably not what you want.

[Bryan Gin-ge Chen]

I checked the default keybinds and shift+space seems to be unused.

Tab would of course be nicer if you can somehow get it working. However, often the autocomplete menu is active as well, and that would eat the tab as well. My guess is that in most situations, unicode input should win over autocomplete, but dealing with all this might be more trouble than it's worth.

[Patrick Massot]

Gabriel, did you write anything about Lean+vim plugin, or do you simply activate both plugin and there is nothing more to know?

[Gabriel Ebner]

I just install both plugins separately. No configuration required.

[Patrick Massot]

thanks

[Gabriel Ebner]

Since everybody loves tab so much, you get tab. Apparently you can set any property on the vscode "context" and then make keybindings conditional on these properties. The tab keybinding is now conditional on lean.input.isActive. Hope this doesn't break anything...

[Mario Carneiro]

I hope that pressing tab gives you a tab (equivalent) when the underline is not active

[Gabriel Ebner]

I'm not sure. Can you check this?

[Mario Carneiro]

I certainly use tab for indentation and block indentation currently

[Gabriel Ebner]

Yes, of course, it works. Tab produces a tab when there's no underline (at least on Linux)

[Gabriel Ebner]

That was the whole point about the undocumentedsetContext command.

[Bryan Gin-ge Chen]

Thanks again Gabriel!