could recursive hover work here in vscode?

Stream: lean4

[Alok Singh]

If I hover over a term, I get its type. But I can't hover over that.

2025-03-28-02-44-50.png

but I can do it in the info view

2025-03-28-02-45-46.png

Is it possible to support nested popup hover?

[Mario Carneiro]

Pretty sure the answer is no, this is a limitation of the hover interface vscode provides. It's possible in the infoview because that's totally custom code in the extension, but vscode hovers are basically just markdown

[Mario Carneiro]

there may also be security reasons vscode is very careful to avoid unapproved html or js inside those markdown bits

[Alok Singh]

sad. in related vein, i thought of a partial applier for abstract functions like pure that would replace the abstract types with more concrete inferred ones (so the \alpha in the picture would be filled in with Unit in the hover.

2025-03-28-02-59-31.png

[Floris van Doorn]

I have also wished that this were possible.

[Marc Huisinga]

See also #general > Showing two doc-string @ 💬.

We could provide some limited HTML support in hovers (nothing as powerful as anything in the InfoView), but the hover UI doesn't play nicely with anything that can change size, and nested tooltips are definitely out of scope.