Clickable infoview links

Stream: general

[Bolton Bailey]

I notice that in the InfoView, when I get an error like error: ././././Foo/Bar.lean:13:37: application type mismatch, I would like to be able to click or command-click on the link to go to the file (or even the line) in question, as I would be able to do in the VSCode terminal. Is there some way to enable this?

[Bolton Bailey]

Here is a link to a GitHub issue I have made for this https://github.com/leanprover/vscode-lean4/issues/631