The layout jumps for a split second every time a tooltip is displayed

[noamraph]

When hovering over an element and a tooltip appears, the layout changes for a fraction of a second, and then returns to normal. To me this is quite distracting. This can be seen here:

https://github.com/leanprover-community/lean4game/assets/1553464/a26e1a47-da63-43d6-8340-c4f205fbc049

I think I found the source. The tooltip starts at the bottom, and then it's moved to its position. The problem is that the arrow goes beyond the bottom of the page, and cause the layout to change - a scrollbar is added, which causes the available horizontal space to shrink, which causes everything to change.

As a simple workaround, I tried to hide the arrow, by adding this to node_modules/lean4-infoview/src/infoview/index.css:

.tooltip-arrow {
    display: none;
}

and now the layout doesn't jump:

https://github.com/leanprover-community/lean4game/assets/1553464/7136b5df-c09f-4ef4-8317-77fb48a78030

I think this is a reasonable solution, which improves the experience quite a bit. However, I like the arrow, and in addition, you still see the tooltip appearing for a split second in the corner and then jumping to its place (this isn't visible in the screen recording, but is visible). I also noticed that it doesn't always prevent the jump. An even better solution would be to just not show the tooltip in the corner, and show it only when it's in its final position. I know very little about React, so I didn't manage to do it in the time I had.

Cheers, Noam

[joneugster]

Thank you for the detailed analysis! I will add your fix next week!

[joneugster]

That should be fixed on the test server from tomorrow on.

(Did not test it myself)

[joneugster]

(I'll leave the issue open still to maybe come back and try to find a better fix)