Zulip Chat Archive

Stream: general

Topic: vscode input completions for markdown

Edward Ayers (Sep 17 2018 at 09:44):

I love the way that Lean does unicode completions so much that I copied the vscode-lean project and made it also work for markdown. Could markdown unicode completions be added as a feature to the vscode-lean extension? Or is it better being a separate extension? Happy to submit a PR doing this.

Edward Ayers (Sep 17 2018 at 09:46):

Seems like @Gabriel Ebner is the one to ask about this.

Gabriel Ebner (Sep 17 2018 at 09:55):

I'd prefer to keep it all in one extension if possible. Ideally you could enable the unicode completions for specific file types and also specific files (via a command). I'm happy about a PR for this feature. That said, I'm on vacation until October.

Last updated: Aug 03 2023 at 10:10 UTC