- // if the window size changed as a result of a user action, we have to update the root box's size
- if (root.width != width || root.height != height) {
-
- // since the scar will be moving, dirty the place it used to be
- if (scarred) dirty(hscar,
- root.height - vscar - scarPicture.getHeight(),
- scarPicture.getWidth(), scarPicture.getHeight());
-
- // sort of ugly; we can't use set() here because it will cause an infinite mutual recursion
- root.width = (int)width;
- root.height = (int)height;
-
- root.needs_reflow = true;
- root.put("SizeChange", Boolean.TRUE);
- }
-