Changeset 16961 in josm


Ignore:
Timestamp:
2020-08-29T13:33:27+02:00 (4 years ago)
Author:
simon04
Message:

see #8334 - Add advanced option to scale the list font

Advanced preference key gui.scale.list.font

File:
1 edited

Legend:

Unmodified
Added
Removed
  • trunk/src/org/openstreetmap/josm/gui/MainApplication.java

    r16913 r16961  
    6262import javax.swing.UIManager;
    6363import javax.swing.UnsupportedLookAndFeelException;
     64import javax.swing.plaf.FontUIResource;
    6465
    6566import org.openstreetmap.josm.actions.DeleteAction;
     
    11101111        }
    11111112
    1112         double menuFontFactor = Config.getPref().getDouble("gui.scale.menu.font", 1.0);
    1113         if (menuFontFactor != 1.0) {
    1114             for (String key : Arrays.asList(
    1115                     "Menu.font", "MenuItem.font", "CheckBoxMenuItem.font", "RadioButtonMenuItem.font", "MenuItem.acceleratorFont")) {
    1116                 Font font = UIManager.getFont(key);
    1117                 if (font != null) {
    1118                     UIManager.put(key, font.deriveFont(font.getSize2D() * (float) menuFontFactor));
    1119                 }
     1113        scaleFonts(Config.getPref().getDouble("gui.scale.menu.font", 1.0),
     1114                "Menu.font", "MenuItem.font", "CheckBoxMenuItem.font", "RadioButtonMenuItem.font", "MenuItem.acceleratorFont");
     1115        scaleFonts(Config.getPref().getDouble("gui.scale.list.font", 1.0),
     1116                "List.font");
     1117        // "Table.font" see org.openstreetmap.josm.gui.util.TableHelper.setFont
     1118    }
     1119
     1120    private static void scaleFonts(double factor, String... fonts) {
     1121        if (factor == 1.0) {
     1122            return;
     1123        }
     1124        for (String key : fonts) {
     1125            Font font = UIManager.getFont(key);
     1126            if (font != null) {
     1127                font = font.deriveFont((float) (font.getSize2D() * factor));
     1128                UIManager.put(key, new FontUIResource(font));
    11201129            }
    11211130        }
Note: See TracChangeset for help on using the changeset viewer.