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