image.java

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

/*	Image objects are invisible panes for displaying gif or jpeg images 
    Author:  David Riley -- Nov, 2004 */
    
/*	class invariant
    	getWidth() >= 0  AND  getHeight() >= 0  */

import java.awt.Toolkit.*;
import java.awt.*;
import javax.imageio.ImageIO;
import java.io.*;
import javax.swing.JComponent;

public class Image extends JComponent implements java.awt.image.ImageObserver {
	private java.awt.Image content;

// Constructor methods
	/*	postcondition 
			an empty image view is instantiated
			AND  getX() == 0   AND  getY() == 0   
			AND  getWidth() == 10  AND  getHeight() == 10   */
	public Image()  {
		super();
		setBounds(0, 0, 10, 10);
	} 

	/*	precondition
			w >= 0   AND   h >= 0
		postcondition 
			an empty image view is instantiated
			AND  getX() == x   AND  getY() == y   
			AND  getWidth() == w  AND  getHeight() == h   */
	public Image(int x, int y, int w, int h)  {
		super();
		setBounds(x, y, w, h);
	} 


	/*	precondition
			w >= 0   AND   h >= 0
		postcondition 
            getX() == x   AND  getY() == y   
			AND  getWidth() == w  AND  getHeight() == h   
			AND  Upon repaint the image displayed will be given by the 
                 file with complete pathname specified as s 
			     (Note that the file should be a gif or jpeg encoding.)  */
	public Image(int x, int y, int w, int h, String s)  {
		super();
		setBounds(x, y, w, h);
        setImage(s);
	} 


// Class Methods   

	/*	postcondition
			Upon repaint the image displayed will be given by the 
			file with complete pathname specified as s 
			(Note that the file should be a gif or jpeg encoding.)  */
	public void setImage(String s)  {
        java.net.URL url = getClass().getResource(s);  // for applets
        if (url == null)   {
            url = getClass().getResource("/"+s);
            if (url == null)
                try {  // for applications
                    content = ImageIO.read(new File(s));
                } catch(IOException ioe) {
                    ioe.printStackTrace();
                }
            else
                content = getToolkit().getImage(url);
        } else
            content = getToolkit().getImage(url);

	}


	public void paint(Graphics g)  {
		g.drawImage(content, 0, 0, getWidth(), getHeight(), this);
        paintChildren(g);
	} 

}