+ /// Height of the hover arrow in multiples of the text height
+ static const float HoverArrowSize;
+
+ static const int Padding;
+
+ /**
+ * The vertical offset, relative to the bottom line of the widget,
+ * where the arrows of the cursor labels end.
+ */
+ static const int BaselineOffset;