diff --git a/app/src/processing/app/platform/DefaultPlatform.java b/app/src/processing/app/platform/DefaultPlatform.java index e80adac32..e87c4230b 100644 --- a/app/src/processing/app/platform/DefaultPlatform.java +++ b/app/src/processing/app/platform/DefaultPlatform.java @@ -25,8 +25,11 @@ package processing.app.platform; import java.awt.Desktop; import java.awt.Font; +import java.awt.font.TextAttribute; import java.io.File; import java.net.URI; +import java.util.HashMap; +import java.util.Map; import javax.swing.UIManager; import javax.swing.plaf.FontUIResource; @@ -117,6 +120,10 @@ public class DefaultPlatform { int fontSize = Preferences.getInteger("ui.font.size"); if (!"Dialog".equals(fontName) || fontSize != 12) { setUIFont(new FontUIResource(fontName, Font.PLAIN, fontSize)); +// Map attributes = new HashMap<>(); +// attributes.put(TextAttribute.KERNING, TextAttribute.KERNING_ON); +// Font font = new Font(fontName, Font.PLAIN, fontSize).deriveFont(attributes); +// setUIFont(new FontUIResource(font)); } }