490 |
{ |
{ |
491 |
// if the viewport changed, we should update the VSB / HSB |
// if the viewport changed, we should update the VSB / HSB |
492 |
// models according to the new vertical and horizontal sizes |
// models according to the new vertical and horizontal sizes |
493 |
|
|
494 |
Rectangle vr = vp.getViewRect(); |
Rectangle vr = vp.getViewRect(); |
495 |
Dimension vs = vp.getViewSize(); |
Dimension vs = vp.getViewSize(); |
|
// System.err.println("got change from viewport, vr=" + vr + ", vs=" + vs); |
|
496 |
if (vsb != null |
if (vsb != null |
497 |
&& (vsb.getMinimum() != 0 |
&& (vsb.getMinimum() != 0 |
498 |
|| vsb.getMaximum() != vs.height |
|| vsb.getMaximum() != vs.height |
499 |
|| vsb.getValue() != vr.y |
|| vsb.getValue() != vr.y |
500 |
|| vsb.getVisibleAmount() != vr.height)) |
|| vsb.getVisibleAmount() != vr.height)) |
|
{ |
|
|
// System.err.println("setting vsb to " |
|
|
// + "pos=" + vr.y |
|
|
// + ", ext=" + vr.height |
|
|
// + ", min=0" |
|
|
// + ", max=" + vs.height); |
|
501 |
vsb.setValue(vr.y, vr.height, 0, vs.height); |
vsb.setValue(vr.y, vr.height, 0, vs.height); |
|
} |
|
502 |
|
|
503 |
if (hsb != null |
if (hsb != null |
504 |
&& (hsb.getMinimum() != 0 |
&& (hsb.getMinimum() != 0 |