Fix font size calculation issue in the editor console.

Responding to benfry#19, there appears to be an issue with calculating the bounds of text inside JTextPane within EditorConsole for specific font family and size combinations. This may be related to https://bugs.openjdk.java.net/browse/JDK-8158370 or https://bugs.openjdk.java.net/browse/JDK-8156217 but resolves when changing Editor.LEFT_GUTTER from 45 to basically anything else.
sampottinger · Nov 7, 2019 · b3051b2 · b3051b2
1 parent ddb8224
commit b3051b2
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/app/src/processing/app/ui/Editor.java b/app/src/processing/app/ui/Editor.java
@@ -79,7 +79,7 @@ public abstract class Editor extends JFrame implements RunnerListener {
   protected EditorState state;
   protected Mode mode;
 
-  static public final int LEFT_GUTTER = Toolkit.zoom(44);
+  static public final int LEFT_GUTTER = Toolkit.zoom(45);
   static public final int RIGHT_GUTTER = Toolkit.zoom(12);
   static public final int GUTTER_MARGIN = Toolkit.zoom(3);