+ static docstring const label = _("Vertical Space");
+ return label + " (" + space_.asGUIName() + ')';
+}
+
+
+namespace {
+int const arrow_size = 4;
+}
+
+
+bool InsetVSpace::metrics(MetricsInfo & mi, Dimension & dim) const
+{
+ int height = 3 * arrow_size;
+ if (space_.length().len().value() >= 0.0)
+ height = max(height, space_.inPixels(*mi.base.bv));