Ticket #3368: scrolllistener_for_prefs.patch

File scrolllistener_for_prefs.patch, 2.2 KB (added by xeen, 15 years ago)
  • src/org/openstreetmap/josm/gui/preferences/PreferenceDialog.java

     
    55
    66import java.awt.Font;
    77import java.awt.GridBagLayout;
     8import java.awt.Rectangle;
    89import java.awt.ScrollPane;
     10import java.awt.event.MouseAdapter;
     11import java.awt.event.MouseEvent;
     12import java.awt.event.MouseWheelEvent;
     13import java.awt.event.MouseWheelListener;
    914import java.util.ArrayList;
    1015import java.util.Collection;
    1116import java.util.Iterator;
     
    3237 *
    3338 * @author imi
    3439 */
    35 public class PreferenceDialog extends JTabbedPane {
     40public class PreferenceDialog extends JTabbedPane implements MouseWheelListener {
    3641
    3742    private final static Collection<PreferenceSettingFactory> settingsFactory = new LinkedList<PreferenceSettingFactory>();
    3843    private final List<PreferenceSetting> settings = new ArrayList<PreferenceSetting>();
     
    116121    public PreferenceDialog() {
    117122        super(JTabbedPane.LEFT, JTabbedPane.SCROLL_TAB_LAYOUT);
    118123
     124        super.addMouseWheelListener(this);
     125
    119126        for (PreferenceSettingFactory factory:settingsFactory) {
    120127
    121128            PreferenceSetting setting = factory.createPreferenceSetting();
     
    173180        // always the last: advanced tab
    174181        settingsFactory.add(new AdvancedPreference.Factory());
    175182    }
     183
     184    /**
     185     * This mouse wheel listener reacts when a scroll is carried out over the
     186     * tab strip and scrolls one tab/down or up, selecting it immediately.
     187     */
     188    public void mouseWheelMoved(MouseWheelEvent wev) {
     189        // Ensure the cursor is over the tab strip
     190        if(super.indexAtLocation(wev.getPoint().x, wev.getPoint().y) < 0)
     191            return;
     192
     193        // Get currently selected tab
     194        int newTab = super.getSelectedIndex() + wev.getWheelRotation();
     195
     196        // Ensure the new tab index is sound
     197        newTab = newTab < 0 ? 0 : newTab;
     198        newTab = newTab >= super.getTabCount() ? super.getTabCount() - 1 : newTab;
     199
     200        // select new tab
     201        super.setSelectedIndex(newTab);
     202    }
    176203}