Changeset 16961 in josm
- Timestamp:
- 2020-08-29T13:33:27+02:00 (4 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
trunk/src/org/openstreetmap/josm/gui/MainApplication.java
r16913 r16961 62 62 import javax.swing.UIManager; 63 63 import javax.swing.UnsupportedLookAndFeelException; 64 import javax.swing.plaf.FontUIResource; 64 65 65 66 import org.openstreetmap.josm.actions.DeleteAction; … … 1110 1111 } 1111 1112 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)); 1120 1129 } 1121 1130 }
Note:
See TracChangeset
for help on using the changeset viewer.