Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix: Ensure large tooltip popups are not clipped and stay within the inforview viewport #289

Merged
merged 9 commits into from
Jun 28, 2023

Conversation

tnaoi
Copy link
Contributor

@tnaoi tnaoi commented Mar 14, 2023

Summary

This fix resolves #280, and #210.

Changes

  • Replaced popper 2 with floating-ui.
  • Update CSS for tooltip to allow for markdown comment scrolling when tooltip exceeds a certain height.
  • Ensure tooltip stays within the infoview viewport by implementing custom flip logic as a floating-ui middleware. Tooltip position is based on pointer position instead of the size and position of the reference element - the element that is being hovered over. This allows for proper tooltip placement, regardless of the shape and size of the reference element. The default position of the tooltip is above and to the right of the pointer. The direction of the flip and the level of offset is based on the quadrant - within the viewport - in which the pointer was located when the hover event was triggered. Viewport quadrants are recalculated every time the hover event is triggered.

Below is a gif which exemplifies the typical behavior of the tooltip:
input mov

@Vtec234 Vtec234 self-requested a review March 30, 2023 14:13
@Vtec234
Copy link
Member

Vtec234 commented Mar 30, 2023

Thank you for the contribution @tnaoi! I like the idea, but I think it needs some improvement to be workable:

  • Pointer-based positioning works well when the reference element is huge (like in your gif), but it's not great when the reference is small, i.e. in the majority of cases. In those cases the popup tends to obscure the reference; it would be better if it appeared next to the reference, as it does now.
    • I would suggest the following approach. Use the standard visibility optimizers like in the tutorial, and a standard placement strategy. I don't think we should be computing flips/quadrants/positioning (i.e. most of pointer ourselves) -- floating-ui can already do it for us! Instead, we should detect whether the tooltip is positioned "well" (this is intentionally fuzzy as I'm not certain what the check should be; perhaps whether the anchor point is within the viewport?), and only use pointer-based positioning when it is not. To implement pointer-based positioning, rather than writing the logic ourselves we should use a virtual element set to the pointer coordinates as the reference.
  • Good riddance to TooltipPlacementContext, it was not that useful.
  • But let's not remove the arrow and offset middlewares.

Are you okay with making those changes?

lean4-infoview/src/infoview/tooltips.tsx Outdated Show resolved Hide resolved
@tnaoi
Copy link
Contributor Author

tnaoi commented Apr 4, 2023

Thank you for the contribution @tnaoi! I like the idea, but I think it needs some improvement to be workable:

  • Pointer-based positioning works well when the reference element is huge (like in your gif), but it's not great when the reference is small, i.e. in the majority of cases. In those cases the popup tends to obscure the reference; it would be better if it appeared next to the reference, as it does now.

    • I would suggest the following approach. Use the standard visibility optimizers like in the tutorial, and a standard placement strategy. I don't think we should be computing flips/quadrants/positioning (i.e. most of pointer ourselves) -- floating-ui can already do it for us! Instead, we should detect whether the tooltip is positioned "well" (this is intentionally fuzzy as I'm not certain what the check should be; perhaps whether the anchor point is within the viewport?), and only use pointer-based positioning when it is not. To implement pointer-based positioning, rather than writing the logic ourselves we should use a virtual element set to the pointer coordinates as the reference.
  • Good riddance to TooltipPlacementContext, it was not that useful.

  • But let's not remove the arrow and offset middlewares.

Are you okay with making those changes?

Thank you for the feedback @Vtec234, I'll try to implement the changes.

@Vtec234
Copy link
Member

Vtec234 commented May 15, 2023

Hi @tnaoi, are you still planning to make the changes? If not, I am happy to do them.

@tnaoi
Copy link
Contributor Author

tnaoi commented May 16, 2023

Hi @tnaoi, are you still planning to make the changes? If not, I am happy to do them.

Unfortunately, I haven't managed to carve out time to make the updates. I'll do my best to make it a priority.

@tnaoi
Copy link
Contributor Author

tnaoi commented Jun 21, 2023

@Vtec234 Sorry I've been neglecting this issue. Not sure if recent changes and requests require different solutions to the problem, so please make whatever changes necessary to address the issue.

@Vtec234
Copy link
Member

Vtec234 commented Jun 21, 2023

@tnaoi no problem at all, your contribution so far has already been helpful. I am building on it now with the new changes in order to address the issues I raised.

@Vtec234
Copy link
Member

Vtec234 commented Jun 28, 2023

@tnaoi in the end I wasn't sure how to incorporate the at-pointer positioning logic in a usable way. This leaves #281 unsolved, but is best to get the scrollability out now. If you figure out a nice way to incorporate it, a follow-up PR would be welcome!

@Vtec234
Copy link
Member

Vtec234 commented Jun 28, 2023

The Documentation View Example Test is failing consistently but none of that code changed in this PR, and it also failed in #307.

@Vtec234 Vtec234 merged commit 7f23b33 into leanprover:master Jun 28, 2023
0 of 4 checks passed
@tnaoi tnaoi deleted the issue-280 branch June 30, 2023 03:23
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Large popups are clipped
2 participants