add a preference to set the font size for icon names

[florian.schmitt@…]

Hi, i think it would be fine to have a way to set the font size (maybe the font familiy, too) using a preference. This would mean to:

• add a preference, for example font.iconname.size holding a positive integer;

• modify ​MapPaintVisitor.java: don't initialize the font on definition (line 48), move the initialization to visitAll() (line 318), for example with:

orderFont = new Font(
                "Helvetica",
                Font.PLAIN,
                Main.pref.getInteger("font.iconname.size", 8)
);

[anonymous]

Fixed in r992.