//# 0 errors, 85 messages
//#
/*
    //#ListScroller.java:1:1: class: com.dmdirc.addons.ui_swing.components.ListScroller
    //#ListScroller.java:1:1: method: com.dmdirc.addons.ui_swing.components.ListScroller.com.dmdirc.addons.ui_swing.components.ListScroller__static_init
 * Copyright (c) 2006-2009 Chris Smith, Shane Mc Cormack, Gregory Holmes
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in
 * all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 * SOFTWARE.
 */

package com.dmdirc.addons.ui_swing.components;

import java.awt.event.MouseWheelEvent;
import java.awt.event.MouseWheelListener;

import javax.swing.JList;
import javax.swing.ListModel;
import javax.swing.ListSelectionModel;

/**
 * Utility class to provide mouse wheel scrolling to a JList.
 */
public class ListScroller implements MouseWheelListener {

    /** List to scroll. */
    private final ListModel model;
    /** List to scroll. */
    private final ListSelectionModel selectionModel;

    /**
     * Creates a new instance of ListScroller.
     *
     * @param list List to scroll over
     */
    public ListScroller(final JList list) {
        this(list.getModel(), list.getSelectionModel());
    //#ListScroller.java:48: method: void com.dmdirc.addons.ui_swing.components.ListScroller.com.dmdirc.addons.ui_swing.components.ListScroller(JList)
    //#input(void com.dmdirc.addons.ui_swing.components.ListScroller(JList)): list
    //#input(void com.dmdirc.addons.ui_swing.components.ListScroller(JList)): this
    //#output(void com.dmdirc.addons.ui_swing.components.ListScroller(JList)): this.model
    //#output(void com.dmdirc.addons.ui_swing.components.ListScroller(JList)): this.selectionModel
    //#pre[1] (void com.dmdirc.addons.ui_swing.components.ListScroller(JList)): list != null
    //#post(void com.dmdirc.addons.ui_swing.components.ListScroller(JList)): init'ed(this.model)
    //#post(void com.dmdirc.addons.ui_swing.components.ListScroller(JList)): init'ed(this.selectionModel)

        list.addMouseWheelListener(this);
    }
    //#ListScroller.java:51: end of method: void com.dmdirc.addons.ui_swing.components.ListScroller.com.dmdirc.addons.ui_swing.components.ListScroller(JList)

    /**
     * Creates a new instance of ListScroller.
     *
     * @param model List model to scroll over
     * @param selectionModel List selection model to scroll over
     */
    public ListScroller(final ListModel model,
            final ListSelectionModel selectionModel) {
    //#ListScroller.java:60: method: void com.dmdirc.addons.ui_swing.components.ListScroller.com.dmdirc.addons.ui_swing.components.ListScroller(ListModel, ListSelectionModel)
    //#input(void com.dmdirc.addons.ui_swing.components.ListScroller(ListModel, ListSelectionModel)): model
    //#input(void com.dmdirc.addons.ui_swing.components.ListScroller(ListModel, ListSelectionModel)): selectionModel
    //#input(void com.dmdirc.addons.ui_swing.components.ListScroller(ListModel, ListSelectionModel)): this
    //#output(void com.dmdirc.addons.ui_swing.components.ListScroller(ListModel, ListSelectionModel)): this.model
    //#output(void com.dmdirc.addons.ui_swing.components.ListScroller(ListModel, ListSelectionModel)): this.selectionModel
    //#post(void com.dmdirc.addons.ui_swing.components.ListScroller(ListModel, ListSelectionModel)): this.model == model
    //#post(void com.dmdirc.addons.ui_swing.components.ListScroller(ListModel, ListSelectionModel)): init'ed(this.model)
    //#post(void com.dmdirc.addons.ui_swing.components.ListScroller(ListModel, ListSelectionModel)): this.selectionModel == selectionModel
    //#post(void com.dmdirc.addons.ui_swing.components.ListScroller(ListModel, ListSelectionModel)): init'ed(this.selectionModel)
        this.model = model;
        this.selectionModel = selectionModel;
    }
    //#ListScroller.java:63: end of method: void com.dmdirc.addons.ui_swing.components.ListScroller.com.dmdirc.addons.ui_swing.components.ListScroller(ListModel, ListSelectionModel)

    /**
     * {@inheritDoc}
     * 
     * @param e Moust wheel event
     */
    @Override
    public void mouseWheelMoved(final MouseWheelEvent e) {
        if (e.getWheelRotation() < 0) {
    //#ListScroller.java:72: method: void com.dmdirc.addons.ui_swing.components.ListScroller.mouseWheelMoved(MouseWheelEvent)
    //#input(void mouseWheelMoved(MouseWheelEvent)): __Descendant_Table[com/dmdirc/addons/ui_swing/components/ListScroller]
    //#input(void mouseWheelMoved(MouseWheelEvent)): __Descendant_Table[others]
    //#input(void mouseWheelMoved(MouseWheelEvent)): __Dispatch_Table.changeFocus(Z)V
    //#input(void mouseWheelMoved(MouseWheelEvent)): e
    //#input(void mouseWheelMoved(MouseWheelEvent)): this
    //#input(void mouseWheelMoved(MouseWheelEvent)): this.__Tag
    //#input(void mouseWheelMoved(MouseWheelEvent)): this.model
    //#input(void mouseWheelMoved(MouseWheelEvent)): this.selectionModel
    //#pre[1] (void mouseWheelMoved(MouseWheelEvent)): e != null
    //#pre[3] (void mouseWheelMoved(MouseWheelEvent)): this.__Tag == com/dmdirc/addons/ui_swing/components/ListScroller
    //#pre[5] (void mouseWheelMoved(MouseWheelEvent)): this.selectionModel != null
    //#pre[4] (void mouseWheelMoved(MouseWheelEvent)): (soft) this.model != null
    //#unanalyzed(void mouseWheelMoved(MouseWheelEvent)): Effects-of-calling:javax.swing.ListModel:getSize
    //#unanalyzed(void mouseWheelMoved(MouseWheelEvent)): Effects-of-calling:javax.swing.ListSelectionModel:getMinSelectionIndex
    //#unanalyzed(void mouseWheelMoved(MouseWheelEvent)): Effects-of-calling:javax.swing.ListSelectionModel:setSelectionInterval
    //#test_vector(void mouseWheelMoved(MouseWheelEvent)): java.awt.event.MouseWheelEvent:getWheelRotation(...)@72: {0..4_294_967_295}, {-2_147_483_648..-1}
            changeFocus(true);
        } else {
            changeFocus(false);
        }
    }
    //#ListScroller.java:77: end of method: void com.dmdirc.addons.ui_swing.components.ListScroller.mouseWheelMoved(MouseWheelEvent)

    /**
     * Activates the node above or below the active node in the list.
     *
     * @param direction true = up, false = down.
     */
    public void changeFocus(final boolean direction) {
        int index;

        //are we going up or down?
        if (direction) {
    //#ListScroller.java:88: method: void com.dmdirc.addons.ui_swing.components.ListScroller.changeFocus(bool)
    //#input(void changeFocus(bool)): direction
    //#input(void changeFocus(bool)): this
    //#input(void changeFocus(bool)): this.model
    //#input(void changeFocus(bool)): this.selectionModel
    //#pre[4] (void changeFocus(bool)): this.selectionModel != null
    //#pre[3] (void changeFocus(bool)): (soft) this.model != null
    //#presumption(void changeFocus(bool)): javax.swing.ListSelectionModel:getMinSelectionIndex(...)@90 >= -2_147_483_647
    //#presumption(void changeFocus(bool)): javax.swing.ListSelectionModel:getMinSelectionIndex(...)@93 <= 4_294_967_294
    //#unanalyzed(void changeFocus(bool)): Effects-of-calling:javax.swing.ListModel:getSize
    //#test_vector(void changeFocus(bool)): direction: {0}, {1}
            //up
            index = changeFocusUp(selectionModel.getMinSelectionIndex());
        } else {
            //down
            index = changeFocusDown(selectionModel.getMinSelectionIndex());
        }
        selectionModel.setSelectionInterval(index, index);
    }
    //#ListScroller.java:96: end of method: void com.dmdirc.addons.ui_swing.components.ListScroller.changeFocus(bool)

    /**
     * Changes the list focus up.
     *
     * @param index Start index
     *
     * @return next index
     */
    private int changeFocusUp(final int index) {
        int nextIndex;

        if (index == 0 || index == -1) {
    //#ListScroller.java:108: method: int com.dmdirc.addons.ui_swing.components.ListScroller.changeFocusUp(int)
    //#input(int changeFocusUp(int)): index
    //#input(int changeFocusUp(int)): this
    //#input(int changeFocusUp(int)): this.model
    //#output(int changeFocusUp(int)): return_value
    //#pre[1] (int changeFocusUp(int)): index >= -2_147_483_647
    //#pre[3] (int changeFocusUp(int)): (soft) this.model != null
    //#presumption(int changeFocusUp(int)): javax.swing.ListModel:getSize(...)@109 >= -2_147_483_647
    //#post(int changeFocusUp(int)): return_value <= 4_294_967_294
    //#test_vector(int changeFocusUp(int)): index: {0}, {-2_147_483_647..-2, 1..4_294_967_295}, {-1}
            nextIndex = model.getSize() - 1;
        } else {
            nextIndex = index - 1;
        }

        return nextIndex;
    //#ListScroller.java:114: end of method: int com.dmdirc.addons.ui_swing.components.ListScroller.changeFocusUp(int)
    }

    /**
     * Changes the list focus down.
     *
     * @param index Start index
     *
     * @return next index
     */
    private int changeFocusDown(final int index) {
        int nextIndex;

        if (index == model.getSize() - 1) {
    //#ListScroller.java:127: method: int com.dmdirc.addons.ui_swing.components.ListScroller.changeFocusDown(int)
    //#input(int changeFocusDown(int)): index
    //#input(int changeFocusDown(int)): this
    //#input(int changeFocusDown(int)): this.model
    //#output(int changeFocusDown(int)): return_value
    //#pre[1] (int changeFocusDown(int)): index <= 4_294_967_294
    //#pre[3] (int changeFocusDown(int)): this.model != null
    //#post(int changeFocusDown(int)): return_value == One-of{0, index + 1}
    //#post(int changeFocusDown(int)): return_value >= -2_147_483_647
            nextIndex = 0;
        } else {
            nextIndex = index + 1;
        }

        return nextIndex;
    //#ListScroller.java:133: end of method: int com.dmdirc.addons.ui_swing.components.ListScroller.changeFocusDown(int)
    }
}
    //#output(com.dmdirc.addons.ui_swing.components.ListScroller__static_init): __Descendant_Table[com/dmdirc/addons/ui_swing/components/ListScroller]
    //#output(com.dmdirc.addons.ui_swing.components.ListScroller__static_init): __Dispatch_Table.changeFocus(Z)V
    //#output(com.dmdirc.addons.ui_swing.components.ListScroller__static_init): __Dispatch_Table.changeFocusDown(I)I
    //#output(com.dmdirc.addons.ui_swing.components.ListScroller__static_init): __Dispatch_Table.changeFocusUp(I)I
    //#output(com.dmdirc.addons.ui_swing.components.ListScroller__static_init): __Dispatch_Table.mouseWheelMoved(Ljava/awt/event/MouseWheelEvent;)V
    //#post(com.dmdirc.addons.ui_swing.components.ListScroller__static_init): __Descendant_Table[com/dmdirc/addons/ui_swing/components/ListScroller] == &__Dispatch_Table
    //#post(com.dmdirc.addons.ui_swing.components.ListScroller__static_init): __Dispatch_Table.changeFocus(Z)V == &changeFocus
    //#post(com.dmdirc.addons.ui_swing.components.ListScroller__static_init): __Dispatch_Table.changeFocusDown(I)I == &changeFocusDown
    //#post(com.dmdirc.addons.ui_swing.components.ListScroller__static_init): __Dispatch_Table.changeFocusUp(I)I == &changeFocusUp
    //#post(com.dmdirc.addons.ui_swing.components.ListScroller__static_init): __Dispatch_Table.mouseWheelMoved(Ljava/awt/event/MouseWheelEvent;)V == &mouseWheelMoved
    //#ListScroller.java:: end of method: com.dmdirc.addons.ui_swing.components.ListScroller.com.dmdirc.addons.ui_swing.components.ListScroller__static_init
    //#ListScroller.java:: end of class: com.dmdirc.addons.ui_swing.components.ListScroller
