Zulip Chat Archive

Stream: new members

Topic: VSCode multiple cursor


view this post on Zulip Anatole Dedecker (Aug 09 2020 at 20:19):

Is it voluntary that we can't type unicode characters using \... while in multiple cursor mode in VSCode ?

view this post on Zulip Mario Carneiro (Aug 09 2020 at 20:19):

no

view this post on Zulip Bryan Gin-ge Chen (Aug 09 2020 at 20:20):

There's an open issue: https://github.com/leanprover/vscode-lean/issues/160

Presumably it's fixable but no one has had the time to yet.

view this post on Zulip Anatole Dedecker (Aug 09 2020 at 20:21):

Ok thanks !

view this post on Zulip Bryan Gin-ge Chen (Aug 11 2020 at 14:29):

Update: thanks to @Alex Peattie, version 0.16.7 of vscode-lean now supports Unicode input with multiple cursors!

view this post on Zulip Anatole Dedecker (Aug 11 2020 at 14:30):

Wow great news !

view this post on Zulip Kevin Buzzard (Aug 11 2020 at 17:04):

That's great! This has annoyed me forever and was annoying me over the weekend.


Last updated: May 16 2021 at 05:21 UTC