- // if the window size changed as a result of a user action, we have to update the root box's size
- if (root.size(0) != width || root.size(1) != height) {
-
- // since the scar will be moving, dirty the place it used to be
- if (scarred) dirty(hscar,
- root.size(1) - 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._size_0 = (short)width;
- root._size_1 = (short)height;
-
- root.mark_for_prerender();
- root.put("SizeChange", null, Boolean.TRUE);
- }
-
- while (root.needs_prerender || abort) {