+
+void output_font_change(ostream & os, Font const & oldfont,
+ Font const & newfont)
+{
+ if (oldfont.family != newfont.family)
+ os << "\n\\family " << newfont.family << '\n';
+ if (oldfont.series != newfont.series)
+ os << "\n\\series " << newfont.series << '\n';
+ if (oldfont.shape != newfont.shape)
+ os << "\n\\shape " << newfont.shape << '\n';
+ if (oldfont.size != newfont.size)
+ os << "\n\\size " << newfont.size << '\n';