clientDividerSizeSet = true;
  public void setDividerSize(int newSize)  {    if (newSize != dividerSize)      {	int oldSize = dividerSize;	dividerSize = newSize;	firePropertyChange(DIVIDER_SIZE_PROPERTY, oldSize, dividerSize);      }  }