This fixes #9928 by invalidating the tooltip on mouse scroll.
I think _ideally_ we'd have a solution that only invalidates it if,
after mouse scroll, we're not hovering over the element. But I tried
that (by essentially duplicating the code for `MouseMoveEvent` but that
lead to some inconsistencies. I think we don't redraw when we finish
scrolling.
This now behaves exactly like tooltips in Chrome: invalidate on scroll,
move mouse again to trigger the tooltip.
It also behaves like the hover tooltips in the editor.
https://github.com/zed-industries/zed/assets/1185253/05b9170e-414c-4453-84e5-90510b943c15
Release Notes:
- N/A
ad03a7e72cThorsten Ball committed on 4/2/2024, 12:10:51 PM· committed by GitHubparent84cca62