You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The current tooltip system does the job but is basic.
While navigating website generated by F# Formatting, I am often frustrated by the inconsistency in the tooltip system.
You can't go inside of the tooltip to select or copy something from it:
CleanShot.2024-12-30.at.21.21.55.mp4
The tooltip placement depends on where you initially place your mouse cursor:
CleanShot.2024-12-30.at.21.23.24.mp4
Working with tooltip is difficult, and could be a good candidate for an external library? Would you be ok with a proposition to use a library like Tippy.js for example?
I am proposing Tippy.js because it was one of the first result from Google and it seems to do what would be needed:
The current tooltip system does the job but is basic.
While navigating website generated by F# Formatting, I am often frustrated by the inconsistency in the tooltip system.
You can't go inside of the tooltip to select or copy something from it:
CleanShot.2024-12-30.at.21.21.55.mp4
The tooltip placement depends on where you initially place your mouse cursor:
CleanShot.2024-12-30.at.21.23.24.mp4
Working with tooltip is difficult, and could be a good candidate for an external library? Would you be ok with a proposition to use a library like Tippy.js for example?
I am proposing Tippy.js because it was one of the first result from Google and it seems to do what would be needed:
top-startto be similar to IDE behavior and it handle screen overflow