vscode input completions for markdown

Stream: general

[Edward Ayers]

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]

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

[Gabriel Ebner]

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.