Changeset 16961 in josm

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:

• trunk/src/org/openstreetmap/josm/gui/MainApplication.java (modified) (2 diffs)

trunk/src/org/openstreetmap/josm/gui/MainApplication.java

@@ -62 +62 @@
 import javax.swing.UIManager;
 import javax.swing.UnsupportedLookAndFeelException;
+import javax.swing.plaf.FontUIResource;
 
 import org.openstreetmap.josm.actions.DeleteAction;
@@ -1110 +1111 @@
         }
 
-        double menuFontFactor = Config.getPref().getDouble("gui.scale.menu.font", 1.0);
-        if (menuFontFactor != 1.0) {
-            for (String key : Arrays.asList(
-                    "Menu.font", "MenuItem.font", "CheckBoxMenuItem.font", "RadioButtonMenuItem.font", "MenuItem.acceleratorFont")) {
-                Font font = UIManager.getFont(key);
-                if (font != null) {
-                    UIManager.put(key, font.deriveFont(font.getSize2D() * (float) menuFontFactor));
-                }
+        scaleFonts(Config.getPref().getDouble("gui.scale.menu.font", 1.0),
+                "Menu.font", "MenuItem.font", "CheckBoxMenuItem.font", "RadioButtonMenuItem.font", "MenuItem.acceleratorFont");
+        scaleFonts(Config.getPref().getDouble("gui.scale.list.font", 1.0),
+                "List.font");
+        // "Table.font" see org.openstreetmap.josm.gui.util.TableHelper.setFont
+    }
+
+    private static void scaleFonts(double factor, String... fonts) {
+        if (factor == 1.0) {
+            return;
+        }
+        for (String key : fonts) {
+            Font font = UIManager.getFont(key);
+            if (font != null) {
+                font = font.deriveFont((float) (font.getSize2D() * factor));
+                UIManager.put(key, new FontUIResource(font));
             }
         }