prevent enormous console with dpi scaling

benfry · benfry · commit 6922bdf1e247 · 2017-02-11T15:58:57.000-05:00
diff --git a/app/src/processing/app/ui/Editor.java b/app/src/processing/app/ui/Editor.java
@@ -262,6 +262,9 @@ public void paintComponent(Graphics g) {
     textarea = createTextArea();
     textarea.setRightClickPopup(new TextAreaPopup());
     textarea.setHorizontalOffset(JEditTextArea.leftHandGutter);
+    //System.out.println(textarea.getPreferredSize());
+    textarea.setPreferredSize(new Dimension(textarea.getPreferredSize().width,
+                                            Toolkit.zoom(90)));
 
     { // Hack: add Numpad Slash as an alternative shortcut for Comment/Uncomment
       int modifiers = Toolkit.awtToolkit.getMenuShortcutKeyMask();
