Fixed minimum size for a bunch of GUI elements

app/src/processing/app/Editor.java

@@ -350,8 +350,9 @@ public class Editor extends JFrame implements RunnerListener {
 
 
     // Set the minimum size for the editor window
-    setMinimumSize(new Dimension(PreferencesData.getInteger("editor.window.width.min"),
+    setMinimumSize(scale(new Dimension(
-                                 PreferencesData.getInteger("editor.window.height.min")));
+        PreferencesData.getInteger("editor.window.width.min"),
+        PreferencesData.getInteger("editor.window.height.min"))));
 //    System.out.println("t3");
 
     // Bring back the general options for the editor
@@ -468,18 +469,6 @@ public class Editor extends JFrame implements RunnerListener {
   }
 
 
-  /**
-   * Hack for #@#)$(* Mac OS X 10.2.
-   * <p/>
-   * This appears to only be required on OS X 10.2, and is not
-   * even being called on later versions of OS X or Windows.
-   */
-//  public Dimension getMinimumSize() {
-//    //System.out.println("getting minimum size");
-//    return new Dimension(500, 550);
-//  }
-
-
   // . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
 
 

app/src/processing/app/EditorHeader.java

@@ -75,7 +75,8 @@ public class EditorHeader extends JComponent {
   static final int PIECE_HEIGHT = scale(33);
 
   // value for the size bars, buttons, etc
-  static final int GRID_SIZE = scale(33);
+  // TODO: Should be a Theme value?
+  static final int GRID_SIZE = 33;
 
   static Image[][] pieces;
   static Image menuButtons[];
@@ -341,17 +342,17 @@ public class EditorHeader extends JComponent {
 
 
   public Dimension getMinimumSize() {
-    if (OSUtils.isMacOS()) {
+    Dimension size = scale(new Dimension(300, GRID_SIZE));
-      return new Dimension(300, GRID_SIZE);
+    if (OSUtils.isMacOS())
-    }
+      size.height--;
-    return new Dimension(300, GRID_SIZE - 1);
+    return size;
   }
 
 
   public Dimension getMaximumSize() {
-    if (OSUtils.isMacOS()) {
+    Dimension size = scale(new Dimension(3000, GRID_SIZE));
-      return new Dimension(3000, GRID_SIZE);
+    if (OSUtils.isMacOS())
-    }
+      size.height--;
-    return new Dimension(3000, GRID_SIZE - 1);
+    return size;
   }
 }

app/src/processing/app/EditorLineStatus.java

@@ -47,7 +47,7 @@ public class EditorLineStatus extends JComponent {
   Color messageForeground;
   
   Font font;
-  int high;
+  int height;
 
   String text = "";
   String name = "";
@@ -57,7 +57,7 @@ public class EditorLineStatus extends JComponent {
     background = Theme.getColor("linestatus.bgcolor");
     font = Theme.getFont("linestatus.font");
     foreground = Theme.getColor("linestatus.color");
-    high = scale(Theme.getInteger("linestatus.height"));
+    height = Theme.getInteger("linestatus.height");
 
     if (OSUtils.isMacOS()) {
       resize = Theme.getThemeImage("resize", this, RESIZE_IMAGE_SIZE, RESIZE_IMAGE_SIZE);
@@ -105,7 +105,7 @@ public class EditorLineStatus extends JComponent {
 
     g.setFont(font);
     g.setColor(foreground);
-    int baseline = (high + g.getFontMetrics().getAscent()) / 2;
+    int baseline = (size.height + g.getFontMetrics().getAscent()) / 2;
     g.drawString(text, scale(6), baseline);
 
     g.setColor(messageForeground);
@@ -130,7 +130,7 @@ public class EditorLineStatus extends JComponent {
   }
 
   public Dimension getPreferredSize() {
-    return new Dimension(300, high);
+    return scale(new Dimension(300, height));
   }
 
   public Dimension getMinimumSize() {
@@ -138,6 +138,6 @@ public class EditorLineStatus extends JComponent {
   }
 
   public Dimension getMaximumSize() {
-    return new Dimension(3000, high);
+    return scale(new Dimension(3000, height));
   }
 }

app/src/processing/app/EditorStatus.java

@@ -33,7 +33,7 @@ import java.awt.event.KeyAdapter;
 import java.awt.event.KeyEvent;
 
 import static processing.app.I18n.tr;
-
+import static processing.app.Theme.scale;
 
 /**
  * Panel just below the editing area that contains status messages.
@@ -68,7 +68,8 @@ public class EditorStatus extends JPanel {
   }
 
   // value for the size bars, buttons, etc
-  static final int GRID_SIZE = Theme.scale(33);
+  // TODO: Should be a Theme value?
+  static final int GRID_SIZE = 33;
 
   private final Editor editor;
   private final Font font;
@@ -398,11 +399,11 @@ public class EditorStatus extends JPanel {
   }
 
   public Dimension getMinimumSize() {
-    return new Dimension(300, GRID_SIZE);
+    return scale(new Dimension(300, GRID_SIZE));
   }
 
   public Dimension getMaximumSize() {
-    return new Dimension(3000, GRID_SIZE);
+    return scale(new Dimension(3000, GRID_SIZE));
   }
 
   public boolean isErr() {

app/src/processing/app/EditorToolbar.java

@@ -31,7 +31,7 @@ import java.awt.event.KeyListener;
 import java.awt.event.MouseEvent;
 
 import static processing.app.I18n.tr;
-
+import static processing.app.Theme.scale;
 
 /**
  * run/stop/etc buttons for the ide
@@ -56,19 +56,19 @@ public class EditorToolbar extends JComponent implements MouseInputListener, Key
   /**
    * Width of each toolbar button.
    */
-  private static final int BUTTON_WIDTH = Theme.scale(27);
+  private static final int BUTTON_WIDTH = scale(27);
   /**
    * Height of each toolbar button.
    */
-  private static final int BUTTON_HEIGHT = Theme.scale(32);
+  private static final int BUTTON_HEIGHT = scale(32);
   /**
    * The amount of space between groups of buttons on the toolbar.
    */
-  private static final int BUTTON_GAP = Theme.scale(5);
+  private static final int BUTTON_GAP = scale(5);
   /**
    * Size of the button image being chopped up.
    */
-  private static final int BUTTON_IMAGE_SIZE = Theme.scale(33);
+  private static final int BUTTON_IMAGE_SIZE = scale(33);
 
 
   private static final int RUN = 0;
@@ -441,7 +441,7 @@ public class EditorToolbar extends JComponent implements MouseInputListener, Key
 
 
   public Dimension getMaximumSize() {
-    return new Dimension(Theme.scale(3000), BUTTON_HEIGHT);
+    return new Dimension(scale(3000), BUTTON_HEIGHT);
   }
 
 

app/src/processing/app/Theme.java

@@ -31,6 +31,7 @@ import java.awt.Graphics;
 import java.awt.Graphics2D;
 import java.awt.Image;
 import java.awt.MediaTracker;
+import java.awt.Rectangle;
 import java.awt.RenderingHints;
 import java.awt.SystemColor;
 import java.awt.Toolkit;
@@ -132,6 +133,15 @@ public class Theme {
     return new Dimension(scale(dim.width), scale(dim.height));
   }
 
+  static public Rectangle scale(Rectangle rect) {
+    Rectangle res = new Rectangle(rect);
+    res.x = scale(res.x);
+    res.y = scale(res.y);
+    res.width = scale(res.width);
+    res.height = scale(res.height);
+    return res;
+  }
+
   static public Color getColorCycleColor(String name, int i) {
     int cycleSize = getInteger(name + ".size");
     name = String.format("%s.%02d", name, i % cycleSize);