You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository was archived by the owner on Apr 2, 2025. It is now read-only.
Currently the extension is set to activate and open the info view when a Markdown document is opened. I presume this is because Lean code can be embedded in Markdown (although I haven't ever used this).
Unfortunately, this setup means that the info view is opened when any Markdown file in any project is opened, even in projects that have nothing to do with Lean. Since Markdown is widely used, this means the info view is opening a lot when it's not at all relevant.
Is it possible to change things so that the info view is only opened for a Markdown file when that file resides in a Lean project?
Currently the extension is set to activate and open the info view when a Markdown document is opened. I presume this is because Lean code can be embedded in Markdown (although I haven't ever used this).
Unfortunately, this setup means that the info view is opened when any Markdown file in any project is opened, even in projects that have nothing to do with Lean. Since Markdown is widely used, this means the info view is opening a lot when it's not at all relevant.
Is it possible to change things so that the info view is only opened for a Markdown file when that file resides in a Lean project?