Extension "Open Documentation of Current Project"

Stream: lean4

[Gihan Marasingha]

I'm returning to a teaching repo I haven't worked on in some time. The Lean 4 extension used to have an "Open Documentation of Current Project" command that I used with my repo. I can't seem to find that command. Has it been removed?

[Marc Huisinga]

The 'Docview: Open Docview' command used to do this (IIRC it would simply render html/index.html in a VS Code webview), but the functionality was removed a couple of months ago. I didn't think anyone even knew about this feature, let alone used it :-)

The documentation infrastructure will be reworked in the coming months, and something similar to this feature may be re-implemented then.

[Patrick Massot]

It was used by #mil.

[Marc Huisinga]

Patrick Massot said:

It was used by #mil.

You can still read the online version of MiL in the DocView. Is it important that it loads the contents of html?

[Patrick Massot]

Being able to work offline is a nice bonus. But of course it is not crucial (and people can also open the pdf version offline).

[Marc Huisinga]

Patrick Massot said:

Being able to work offline is a nice bonus. But of course it is not crucial (and people can also open the pdf version offline).

Thanks, I'll keep that in mind when reworking the DocView in the future.

[Eric Wieser]

Even without any lean extension support, you can open the index.html file in an editor, and then I think vscode (or possibly a first-party extension) will give you a preview webview