+ /** returns the actual font that should be used to render this box */
+ private String font() {
+ if (font != null) return font;
+ if (font == null && cachedFont != null) return cachedFont;
+ if (getParent() != null) return cachedFont = getParent().font();
+ return cachedFont = Platform.getDefaultFont();
+ }
+
+ /** this must be called when a box's font changes */
+ void fontChanged() {
+ textupdate();
+ for(Box b = getChild(0); b != null; b = b.nextSibling())
+ if (b.font == null) {
+ b.cachedFont = font();
+ b.fontChanged();
+ }
+ }
+