Changeset 16960 in josm for trunk/src/org/openstreetmap/josm/gui/preferences/imagery/ImageryProvidersPanel.java

Timestamp:

2020-08-29T13:33:25+02:00 (4 years ago)

Author:

simon04

Message:

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

Advanced preference keys gui.scale.table.*

File:

• trunk/src/org/openstreetmap/josm/gui/preferences/imagery/ImageryProvidersPanel.java (modified) (2 diffs)

trunk/src/org/openstreetmap/josm/gui/preferences/imagery/ImageryProvidersPanel.java

@@ -62 +62 @@
 import org.openstreetmap.josm.gui.preferences.PreferenceTabbedPane;
 import org.openstreetmap.josm.gui.util.GuiHelper;
+import org.openstreetmap.josm.gui.util.TableHelper;
 import org.openstreetmap.josm.gui.widgets.FilterField;
 import org.openstreetmap.josm.gui.widgets.HtmlPanel;
@@ -224 +225 @@
             }
         };
+        TableHelper.setFont(activeTable, getClass());
         activeTable.putClientProperty("terminateEditOnFocusLost", Boolean.TRUE);
 
         defaultModel = new ImageryDefaultLayerTableModel();
         defaultTable = new JTable(defaultModel);
+        TableHelper.setFont(defaultTable, getClass());
         defaultTable.setAutoCreateRowSorter(true);
         defaultFilter = new FilterField().filter(defaultTable, defaultModel);