import java.awt.Color;
import java.awt.event.ActionEvent;
+import java.awt.event.MouseWheelEvent;
+import java.awt.event.MouseWheelListener;
import javax.swing.AbstractAction;
import javax.swing.JScrollBar;
}
};
addChangeListener(changeListener);
+
+ // Fix for bug #13543
+ this.addMouseWheelListener(new MouseWheelListener() {
+ public void mouseWheelMoved(MouseWheelEvent e) {
+ int notches = e.getWheelRotation();
+ int step = (e.isControlDown() ? getMajorTickSpacing() : getMinorTickSpacing());
+ if (notches < 0) {
+ setValue(getValue() + step);
+ } else {
+ setValue(getValue() - step);
+ }
+ }
+ });
}
/**