public void setVerticalScrollJump(int jump) {
    int old = myOptions.VERTICAL_SCROLL_JUMP;
    if (old == jump) return;
    myOptions.VERTICAL_SCROLL_JUMP = jump;
    myPropertyChangeSupport.firePropertyChange(PropNames.PROP_VERTICAL_SCROLL_JUMP, old, jump);
  }
public void setVerticalScrollJump(int jump)