/* A child of javax.swing.text.html.HTMLEditorKit, patched to use
   PatchedStyleSheet rather than javax.swing.text.html.StyleSheet.

   kvlinden, 10Feb00
*/

package TV;

import javax.swing.text.html.*;
import javax.swing.text.*;
import java.io.*;

public class PatchedHTMLEditorKit extends HTMLEditorKit {

    /* This is changed to associate a PatchedStyleSheet with the 
       default document, rather than a StyleSheet. - kvlinden, 10feb00
    */
    public Document createDefaultDocument() {
	PatchedStyleSheet styles = (PatchedStyleSheet)getStyleSheet();
	// PENDING(prinz) We should be cloning the
	// sheet so the document can add it's own
	// styles to it.  Since clone isn't yet implemented
	// and the document doesn't yet install styles
	// this works temporarily.

	HTMLDocument doc = new HTMLDocument(styles);
	doc.setAsynchronousLoadPriority(4);
	doc.setTokenThreshold(100);
	return doc;
    }

    /* We can't use defaultStyles from HTMLEditorKit because it
       is declared as private, not protected.  It doesn't matter
       though, we just load the default isolde.css rules and return
       them; this basically ignores the value of defaultStyles in
       the parent class.  - kvlinden, 10Feb00
    */
    public StyleSheet getStyleSheet() {
	PatchedStyleSheet defaultStyles = new PatchedStyleSheet();
	try {
	    InputStream is;

	    //PENDING(prinz): Use new security model
	    is = PatchedHTMLEditorKit.class.getResourceAsStream("isolde.css");

	    Reader r = new BufferedReader(new InputStreamReader(is));
	    defaultStyles.loadRules(r, null);
	    r.close();
	} catch (Throwable e) {
	    // on error we simply have no styles... the html
	    // will look mighty wrong but still function.
	}
	return defaultStyles;
    }
}
