fahrenheitslider.java

Java程序设计(美) David D. Riley著 机械工业出版社 书籍配套 代码

// Figure 8.48

import javax.swing.event.ChangeEvent;
public class FahrenheitSlider extends EventSlider {
	private FahrenheitField theField;
	
	/**	pre:	f != null 
	 *	post:	theField == f
     *			and  getMinimum() == min  and  getMaximum() == max
     *			and  getValue() = val  and  orientation is HORIZONTAL
     *			and  theField == f  
     */
	public FahrenheitSlider(int min, int max, int val, FahrenheitField f)  {
		super(HORIZONTAL, min, max, val);
		theField = f;
	}

	/**	pre:	theField != null 
	 *	post:	theField.intValue == intValue
	 *			and  the postcondition of theField.actionPerformed(null)  
	 */
	public void stateChanged(ChangeEvent e)   {
		theField.setText("" + getValue());
		theField.repaint();
		theField.actionPerformed(null);  //null is a dummy argument
	}
}