meraymond2 / idris-vscode

Idris front-end for VS Code
MIT License
59 stars 10 forks source link

Markdown blocks #64

Closed meraymond2 closed 3 years ago

meraymond2 commented 3 years ago

Added

Aside from quoting the changelog, I'll mention that as far as I can tell, there is no way to activate an extension based on an embedded language. I'm also not willing to activate this extension on every markdown file. I experimented with making a separate languageId for .lidr.md files, but then you lose the normal markdown behaviour.

The least-bad option I've come up with is to add a manual activation command, so if you want to write Idris in markdown files, and the extension hasn't already been activated you can do so. (I checked out the Agda extension's behaviour, per https://github.com/meraymond2/idris-vscode/issues/53, and they appear to do something similar.)

I've been writing unit tests over in https://github.com/meraymond2/idris-ide-client, and all the commands work perfectly fine for markdown files, with a few quirks.