Zulip Chat Archive

Stream: new members

Topic: VSCode multiple cursor


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 ?

Mario Carneiro (Aug 09 2020 at 20:19):

no

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.

Anatole Dedecker (Aug 09 2020 at 20:21):

Ok thanks !

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!

Anatole Dedecker (Aug 11 2020 at 14:30):

Wow great news !

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: Dec 20 2023 at 11:08 UTC