}
-void InsetSpace::metrics(MetricsInfo & mi, Dimension & dim) const
+bool InsetSpace::metrics(MetricsInfo & mi, Dimension & dim) const
{
frontend::FontMetrics const & fm =
theFontMetrics(mi.base.font);
dim.wid = 10;
break;
}
+ bool const changed = dim_ != dim;
dim_ = dim;
+ return changed;
}