import java.awt.*;
import java.net.*;
import java.io.*;
import java.util.Dictionary;
import java.util.Enumeration;

import javax.swing.*;
import javax.swing.event.*;
import javax.swing.text.*;
import javax.swing.text.html.*;

/**
  This class implements the special JInternalFrame Mozart uses.
  The internal frame contains a scrollable JEditorPane which is
  where all of the editing will occur.

  <br><br><a href="../source/MozartInternalFrame.java">View Source File</a>
*/
public class MozartInternalFrame extends JInternalFrame {
  private String title;
  private JEditorPane htmlPane;

  /** 
    Creates an empty MozartInternalFrame with a title
  */
  public MozartInternalFrame(Mozart mozart) {
    super("New Document", true, true, true, true);

    htmlPane = new JEditorPane();
    
    htmlPane.setContentType("text/html");
    htmlPane.setEditable(true);
    
    Document document = htmlPane.getDocument();
    document.addUndoableEditListener(mozart.getUndoManager());
    
    JScrollPane htmlScroller = new JScrollPane();
    JViewport htmlVp = htmlScroller.getViewport();
    htmlVp.add(htmlPane);
    htmlVp.setBackingStoreEnabled(true);
    
    getContentPane().add(htmlScroller, BorderLayout.CENTER);
    
    addInternalFrameListener(new InternalFrameAdapter() {
      public void internalFrameClosing(InternalFrameEvent e) {
	System.out.println(title + " frame closing");
      }
    });
    
    setSize(400,300);
    setLayer(JLayeredPane.DEFAULT_LAYER);
  }

  /** 
    Return the document contained in this internal frame.
  */
  public HTMLDocument getDocument() {
    return (HTMLDocument) htmlPane.getDocument();
  }

  /**
    Set the contents of this frame to document.
  */
  public void setPage(URL url) {
    try {
      htmlPane.setPage(url);
      HTMLDocument doc = (HTMLDocument) htmlPane.getDocument();

      // retrieve the document's title from its property list

    } catch (IOException ioe) {
      System.out.println("Error opening url: " + url + "\n" + ioe);
    }
  }

  public void setPage(File file) {
    // Read from file stream.
    // Set document's title from document property
    try {
      try {
	htmlPane.read(new FileReader(file), file);
	setTitle(file.toString());
      } catch (FileNotFoundException fe) { }
    } catch (IOException ioe) { }
  }

  public void setTitle(String title) {
    this.title = title;
    super.setTitle(title);
  }

  public String getTitle() {
    return title;
  }
  
  public void showProperties() {
    HTMLDocument doc = (HTMLDocument) htmlPane.getDocument();
    Dictionary properties = doc.getDocumentProperties();

    for (Enumeration elements = properties.elements(); elements.hasMoreElements() ;) {
      System.out.println(elements.nextElement());
    }
  }
}