remove ui.font from prefs and to streamline font use

This commit is contained in:
Ben Fry
2022-07-31 18:10:59 -04:00
parent a97a0008c1
commit 899a717ce3
2 changed files with 18 additions and 12 deletions
@@ -65,6 +65,7 @@ public class DefaultPlatform {
"CheckBox",
"CheckBoxMenuItem",
"ComboBox",
"Label",
"List",
"Menu",
"MenuBar",
@@ -80,6 +81,7 @@ public class DefaultPlatform {
"Table",
"TableHeader",
"TextArea",
"TextField",
"TextPane",
"TitledBorder",
"ToggleButton",
@@ -115,14 +117,11 @@ public class DefaultPlatform {
// dummy font call so that it's registered for FlatLaf
Font defaultFont = Toolkit.getSansFont(14, Font.PLAIN);
UIManager.put("defaultFont", defaultFont);
// pull in FlatLaf.properties from the processing.app.laf folder
FlatLaf.registerCustomDefaultsSource("processing.app.laf");
// defaultFont = 14 "Processing Sans", "Open Sans", "Noto Sans", Roboto, Arial
//UIManager.put("defaultFont", "14 \"Processing Sans\", \"Open Sans\", \"Noto Sans\", Roboto, Arial");
UIManager.put("defaultFont", defaultFont);
// start with Light, but updateTheme() will be called soon
UIManager.setLookAndFeel(new FlatLightLaf());
@@ -133,6 +132,7 @@ public class DefaultPlatform {
}
*/
/*
// If the default has been overridden in the preferences, set the font
String fontName = Preferences.get("ui.font.family");
int fontSize = Preferences.getInteger("ui.font.size");
@@ -148,6 +148,7 @@ public class DefaultPlatform {
// Font font = new Font(fontName, Font.PLAIN, fontSize).deriveFont(attributes);
// setUIFont(new FontUIResource(font));
}
*/
}
// // Adapted from https://stackoverflow.com/a/64667581/18247494
@@ -161,6 +162,7 @@ public class DefaultPlatform {
// }
// }
/*
// Rewritten from https://stackoverflow.com/a/7434935
static private void setUIFont(FontUIResource f) {
for (Object key : UIManager.getLookAndFeelDefaults().keySet()) {
@@ -170,6 +172,7 @@ public class DefaultPlatform {
}
}
}
*/
public void setInterfaceZoom() throws Exception {
@@ -179,11 +182,14 @@ public class DefaultPlatform {
scaleDefaultFont(widgetName);
}
String fontName = Preferences.get("ui.font.family");
int fontSize = Preferences.getInteger("ui.font.size");
FontUIResource uiFont = new FontUIResource(fontName, Font.PLAIN, Toolkit.zoom(fontSize));
UIManager.put("Label.font", uiFont);
UIManager.put("TextField.font", uiFont);
// Font defaultFont = Toolkit.getSansFont(14, Font.PLAIN);
// UIManager.put("defaultFont", defaultFont);
// String fontName = Preferences.get("ui.font.family");
// int fontSize = Preferences.getInteger("ui.font.size");
// FontUIResource uiFont = new FontUIResource(fontName, Font.PLAIN, Toolkit.zoom(fontSize));
// UIManager.put("Label.font", uiFont);
// UIManager.put("TextField.font", uiFont);
}
}
+3 -3
View File
@@ -95,9 +95,9 @@ platform.auto_file_type_associations = true
# !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
# default font used for UI elements
ui.font.family = Dialog
ui.font.size = 12
# default font used for UI elements (no longer in use as of beta 9)
#ui.font.family = Dialog
#ui.font.size = 12
# default size for the main window
editor.window.width.default = 700