Only open info view for Markdown files in Lean projects

[inkytonik]

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?