Expose tooltip capabilities in @leanprover/infoview?

Stream: lean4

[Thomas Murrills]

When writing (java|type)script for widgets, it would be useful to be able to employ standard lean tooltips. For example, if some graphical element in a widget represents an Expr, we could show that Expr on hover. In my case, I'd like to typeset lean expressions as math, and show the original expression on hover.

Am I right in thinking that this would be achievable by adding export * from './infoview/tooltips' to the extension's index.tsx? Are any of these exports unnecessary, and should the set be restricted? (The exports would be TooltipProps, Tooltip, HoverState, DetectHoverSpan, and WithTooltipOnHover.) Also, would this work as expected when not hovering over code, or are any assumptions made of the hovered-over content that could break in a custom widget?

If adding the above export is reasonable, I'd be happy to PR the extension if it's convenient. :)

[Wojciech Nawrocki]

Also, would this work as expected when not hovering over code, or are any assumptions made of the hovered-over content that could break in a custom widget?

Good question. The hover components are built to be reasonably composable with each other and with other components, but there may be assumptions that are true in the infoview that wouldn't be true of arbitrary widgets. It would be a test for the code at least!

I would suggest the following thing: add the export in your local copy of the extension, and try to develop a widget using the new exported functionality. If it works as expected, we can add it to the published version of @leanprover/infoview.

[Thomas Murrills]

Sounds good! :) I’ll try to test it out that way over the next few days (I might not have a chance until after Sunday or Monday).