+ children.remove(child);
+ }
+
+ // ------------------------------------------------------------------------
+ // StretchLayoutManager ---------------------------------------------------
+ // ------------------------------------------------------------------------
+
+ /**
+ * Resize/reposition child widgets based on difference between current
+ * dimensions and the original dimensions.
+ */
+ public void layoutChildren() {
+ double widthRatio = (double) width / originalWidth;
+ if (!Double.isFinite(widthRatio)) {
+ widthRatio = 1;
+ }
+ double heightRatio = (double) height / originalHeight;
+ if (!Double.isFinite(heightRatio)) {
+ heightRatio = 1;
+ }
+ for (TWidget child: children.keySet()) {
+ Rectangle rect = children.get(child);
+ child.setDimensions((int) (rect.getX() * widthRatio),
+ (int) (rect.getY() * heightRatio),
+ (int) (rect.getWidth() * widthRatio),
+ (int) (rect.getHeight() * heightRatio));
+ }