org.jutil.java.swing
Class SliderControlledLabel

java.lang.Object
  |
  +--java.awt.Component
        |
        +--java.awt.Container
              |
              +--javax.swing.JComponent
                    |
                    +--javax.swing.JLabel
                          |
                          +--org.jutil.java.swing.SliderControlledLabel

All Implemented Interfaces:

javax.accessibility.Accessible, javax.swing.event.ChangeListener, java.util.EventListener, java.awt.image.ImageObserver, java.awt.MenuContainer, java.io.Serializable, javax.swing.SwingConstants

public class SliderControlledLabel

extends javax.swing.JLabel

implements javax.swing.event.ChangeListener

A SliderControlledLabel is a JLabel that keeps its text equal to the value of a JSlider.

Do not register this SliderControlledLabel more than once with getSlider(). Termination will not work because before jdk 1.4, JSlider does not have a getChangeListeners() method.

Version:

$Revision: 1.2 $

Author:

Tom Schrijvers, Marko van Dooren

See Also:

JLabel, JSlider, Serialized Form

Inner classes inherited from class javax.swing.JLabel

javax.swing.JLabel.AccessibleJLabel

Inner classes inherited from class javax.swing.JComponent

javax.swing.JComponent.AccessibleJComponent

Inner classes inherited from class java.awt.Container

java.awt.Container.AccessibleAWTContainer

Inner classes inherited from class java.awt.Component

java.awt.Component.AccessibleAWTComponent

Fields inherited from class javax.swing.JLabel

labelFor

Fields inherited from class javax.swing.JComponent

accessibleContext, listenerList, TOOL_TIP_TEXT_KEY, ui, UNDEFINED_CONDITION, WHEN_ANCESTOR_OF_FOCUSED_COMPONENT, WHEN_FOCUSED, WHEN_IN_FOCUSED_WINDOW

Fields inherited from class java.awt.Component

BOTTOM_ALIGNMENT, CENTER_ALIGNMENT, LEFT_ALIGNMENT, RIGHT_ALIGNMENT, TOP_ALIGNMENT

Fields inherited from interface javax.swing.SwingConstants

BOTTOM, CENTER, EAST, HORIZONTAL, LEADING, LEFT, NORTH, NORTH_EAST, NORTH_WEST, RIGHT, SOUTH, SOUTH_EAST, SOUTH_WEST, TOP, TRAILING, VERTICAL, WEST

Fields inherited from interface java.awt.image.ImageObserver

ABORT, ALLBITS, ERROR, FRAMEBITS, HEIGHT, PROPERTIES, SOMEBITS, WIDTH

Constructor Summary

SliderControlledLabel(javax.swing.JSlider slider)
public invariant (* If getSlider() is not sending events,
getText().equals(
Integer.toString(getSlider().getValue())
)
*);
// The slider may not be null
public invariant getSlider() != null;
// This SliderControlledLabel is registered as a ChangeListener with the slider.

Method Summary

javax.swing.JSlider	getSlider() Return the slider that controls the value of this SliderControlledLabel.
void	stateChanged(javax.swing.event.ChangeEvent evt) public behavior post getText().equals(Integer.toString(slider.getValue())); Update this SliderControlledLabel.
void	terminate() public behavior post getSlider() == null; // Can not work correct for pre-1.4 jdk's. post (\forall int i; i >= 0 && i< \old(getSlider()).getChangeListeners().length; \old(getSlider()).getChangeListeners()[i] != this); Terminate this SliderControlledLabel.

Methods inherited from class javax.swing.JLabel

checkHorizontalKey, checkVerticalKey, getAccessibleContext, getDisabledIcon, getDisplayedMnemonic, getHorizontalAlignment, getHorizontalTextPosition, getIcon, getIconTextGap, getLabelFor, getText, getUI, getUIClassID, getVerticalAlignment, getVerticalTextPosition, imageUpdate, paramString, setDisabledIcon, setDisplayedMnemonic, setDisplayedMnemonic, setHorizontalAlignment, setHorizontalTextPosition, setIcon, setIconTextGap, setLabelFor, setText, setUI, setVerticalAlignment, setVerticalTextPosition, updateUI

Methods inherited from class javax.swing.JComponent

addAncestorListener, addNotify, addPropertyChangeListener, addPropertyChangeListener, addVetoableChangeListener, computeVisibleRect, contains, createToolTip, disable, enable, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, firePropertyChange, fireVetoableChange, getActionForKeyStroke, getActionMap, getAlignmentX, getAlignmentY, getAutoscrolls, getBorder, getBounds, getClientProperty, getComponentGraphics, getConditionForKeyStroke, getDebugGraphicsOptions, getGraphics, getHeight, getInputMap, getInputMap, getInputVerifier, getInsets, getInsets, getListeners, getLocation, getMaximumSize, getMinimumSize, getNextFocusableComponent, getPreferredSize, getRegisteredKeyStrokes, getRootPane, getSize, getToolTipLocation, getToolTipText, getToolTipText, getTopLevelAncestor, getVerifyInputWhenFocusTarget, getVisibleRect, getWidth, getX, getY, grabFocus, hasFocus, hide, isDoubleBuffered, isFocusCycleRoot, isFocusTraversable, isLightweightComponent, isManagingFocus, isMaximumSizeSet, isMinimumSizeSet, isOpaque, isOptimizedDrawingEnabled, isPaintingTile, isPreferredSizeSet, isRequestFocusEnabled, isValidateRoot, paint, paintBorder, paintChildren, paintComponent, paintImmediately, paintImmediately, print, printAll, printBorder, printChildren, printComponent, processComponentKeyEvent, processFocusEvent, processKeyBinding, processKeyEvent, processMouseMotionEvent, putClientProperty, registerKeyboardAction, registerKeyboardAction, removeAncestorListener, removeNotify, removePropertyChangeListener, removePropertyChangeListener, removeVetoableChangeListener, repaint, repaint, requestDefaultFocus, requestFocus, resetKeyboardActions, reshape, revalidate, scrollRectToVisible, setActionMap, setAlignmentX, setAlignmentY, setAutoscrolls, setBackground, setBorder, setDebugGraphicsOptions, setDoubleBuffered, setEnabled, setFont, setForeground, setInputMap, setInputVerifier, setMaximumSize, setMinimumSize, setNextFocusableComponent, setOpaque, setPreferredSize, setRequestFocusEnabled, setToolTipText, setUI, setVerifyInputWhenFocusTarget, setVisible, unregisterKeyboardAction, update

Methods inherited from class java.awt.Container

add, add, add, add, add, addContainerListener, addImpl, countComponents, deliverEvent, doLayout, findComponentAt, findComponentAt, getComponent, getComponentAt, getComponentAt, getComponentCount, getComponents, getLayout, insets, invalidate, isAncestorOf, layout, list, list, locate, minimumSize, paintComponents, preferredSize, printComponents, processContainerEvent, processEvent, remove, remove, removeAll, removeContainerListener, setLayout, validate, validateTree

Methods inherited from class java.awt.Component

action, add, addComponentListener, addFocusListener, addHierarchyBoundsListener, addHierarchyListener, addInputMethodListener, addKeyListener, addMouseListener, addMouseMotionListener, bounds, checkImage, checkImage, coalesceEvents, contains, createImage, createImage, disableEvents, dispatchEvent, enable, enableEvents, enableInputMethods, getBackground, getBounds, getColorModel, getComponentOrientation, getCursor, getDropTarget, getFont, getFontMetrics, getForeground, getGraphicsConfiguration, getInputContext, getInputMethodRequests, getLocale, getLocation, getLocationOnScreen, getName, getParent, getPeer, getSize, getToolkit, getTreeLock, gotFocus, handleEvent, inside, isDisplayable, isEnabled, isLightweight, isShowing, isValid, isVisible, keyDown, keyUp, list, list, list, location, lostFocus, mouseDown, mouseDrag, mouseEnter, mouseExit, mouseMove, mouseUp, move, nextFocus, paintAll, postEvent, prepareImage, prepareImage, processComponentEvent, processHierarchyBoundsEvent, processHierarchyEvent, processInputMethodEvent, processMouseEvent, remove, removeComponentListener, removeFocusListener, removeHierarchyBoundsListener, removeHierarchyListener, removeInputMethodListener, removeKeyListener, removeMouseListener, removeMouseMotionListener, repaint, repaint, repaint, resize, resize, setBounds, setBounds, setComponentOrientation, setCursor, setDropTarget, setLocale, setLocation, setLocation, setName, setSize, setSize, show, show, size, toString, transferFocus

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Constructor Detail

SliderControlledLabel

public SliderControlledLabel(javax.swing.JSlider slider)

public invariant (* If getSlider() is not sending events,
getText().equals(
Integer.toString(getSlider().getValue())
)
*);
// The slider may not be null
public invariant getSlider() != null;
// This SliderControlledLabel is registered as a ChangeListener with the slider.
public invariant (\exists int i; i >= 0 && i < getSlider().getChangeListeners().length;
getSlider().getChangeListeners()[i] == this);

public behavior

pre slider != null;

post getSlider() == slider;
post getText().equals(Integer.toString(slider.getValue()));
Initialize a new SliderControlledLabel that gets its value of the given slider.

Parameters:

slider - The slider this SliderControlledLabel has to show the value of.

Method Detail

stateChanged

public void stateChanged(javax.swing.event.ChangeEvent evt)

public behavior

post getText().equals(Integer.toString(slider.getValue()));
Update this SliderControlledLabel.

Specified by:

stateChanged in interface javax.swing.event.ChangeListener

Parameters:

event - The event sent by the JSlider.

getSlider

public javax.swing.JSlider getSlider()

Return the slider that controls the value of this SliderControlledLabel.

terminate

public void terminate()

public behavior

post getSlider() == null;
// Can not work correct for pre-1.4 jdk's.
post (\forall int i; i >= 0 && i< \old(getSlider()).getChangeListeners().length;
\old(getSlider()).getChangeListeners()[i] != this);
Terminate this SliderControlledLabel.