Changeset 12923 in josm

Timestamp:

2017-10-04T19:01:26+02:00 (7 years ago)

Author:

bastiK

Message:

see #9995 - add advanced option to scale the menu font (gui.scale.menu.font)

File:

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

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

@@ -8 +8 @@
 import java.awt.Container;
 import java.awt.Dimension;
+import java.awt.Font;
 import java.awt.GraphicsEnvironment;
 import java.awt.GridBagLayout;
@@ -1173 +1174 @@
             UIManager.put(p+".caretForeground", UIManager.getColor(p+".foreground"));
         }
+
+        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));
+                }
+            }
+        }
     }