Module Constants.Toplayer

type t = {
  1. tooltips_have_arrows : [ `No | `Yes_with_length_px of float ];
  2. tooltip_offset_px : float;
  3. tooltip_show_delay : Core.Time_ns.Span.t;
  4. tooltip_hide_grace_period : Core.Time_ns.Span.t;
  5. hoverable_tooltip_hide_grace_period : Core.Time_ns.Span.t;
  6. popover_default_offset_px : float;
  7. popover_with_arrow_default_offset_px : float;
  8. popover_with_arrow_default_arrow_length_px : float;
}

hoverable_tooltip_hide_grace_period should be sufficiently long for the user to move their cursor from the anchor to the tooltip.

If tooltips_have_arrows, tooltip_offset_px should be big enough that the arrow doesn't overlap with the anchor. The same applies to popover_with_arrow_default_offset_px.