# HG changeset patch
# User wenzelm
# Date 1246054751 -7200
# Node ID 42ab7ad9b07eda209a0dc71a0d28c0757187c21e
# Parent  f044d8446ae9f5046f65a049a96c6474bae95d72
preload CSS resources;

diff -r f044d8446ae9 -r 42ab7ad9b07e src/Tools/jEdit/src/renderer/UserAgent.scala
--- a/src/Tools/jEdit/src/renderer/UserAgent.scala	Fri Jun 26 23:28:46 2009 +0200
+++ b/src/Tools/jEdit/src/renderer/UserAgent.scala	Sat Jun 27 00:19:11 2009 +0200
@@ -9,6 +9,8 @@
 
 import isabelle.jedit.Isabelle
 
+import scala.io.Source
+
 import java.io.{InputStream, ByteArrayInputStream, FileInputStream}
 
 import org.xhtmlrenderer.swing.NaiveUserAgent
@@ -17,12 +19,12 @@
 
 object UserAgent
 {
-  // FIXME avoid static getenv
   val base_URL = "file://localhost/dummy/"
-  val style = base_URL + "style"
-  val isabelle_css = base_URL + "isabelle.css"
-  val isabelle_user_css = base_URL + "isabelle_user.css"
-  val stylesheet = """
+
+  private val style = base_URL + "style"
+  private val isabelle_css = base_URL + "isabelle.css"
+  private val isabelle_user_css = base_URL + "isabelle_user.css"
+  private val stylesheet = """
 @import "isabelle.css";
 @import 'isabelle_user.css';
 
@@ -36,31 +38,37 @@
 
 class UserAgent extends NaiveUserAgent
 {
-  private def empty_stream(): InputStream =
-    new ByteArrayInputStream(new Array[Byte](0))
-
-  private def try_file_stream(name: String): InputStream =
+  private def string_content(text: String): Array[Byte] =
+    text.getBytes(Isabelle_System.charset)
+  
+  private def try_file_content(name: String): Array[Byte] =
   {
     val file = Isabelle.system.platform_file(name)
-    if (file.exists) new FileInputStream(file)
-    else empty_stream()
+    val text =
+      if (file.exists) Source.fromFile(file).mkString
+      else ""
+    string_content(text)
   }
 
+  private def CSS(content: Array[Byte]): CSSResource =
+    new CSSResource(new ByteArrayInputStream(content))
+
+  private val stylesheet = string_content(UserAgent.stylesheet)
+  private val isabelle_css = try_file_content("~~/lib/html/isabelle.css")
+  private val isabelle_user_css = try_file_content("$ISABELLE_HOME_USER/etc/isabelle.css")
+
   override def getCSSResource(uri: String): CSSResource =
   {
     uri match {
-      case UserAgent.style =>
-        new CSSResource(
-          new ByteArrayInputStream(UserAgent.stylesheet.getBytes(Isabelle_System.charset)))
-      case UserAgent.isabelle_css =>
-        new CSSResource(try_file_stream("~~/lib/html/isabelle.css"))
-      case UserAgent.isabelle_user_css =>
-        new CSSResource(try_file_stream("$ISABELLE_HOME_USER/etc/isabelle.css"))
+      case UserAgent.style => CSS(stylesheet)
+      case UserAgent.isabelle_css => CSS(isabelle_css)
+      case UserAgent.isabelle_user_css => CSS(isabelle_user_css)
       case _ =>
         val stream = resolveAndOpenStream(uri)
         val resource = new CSSResource(stream)
         if (stream == null)
-          resource.getResourceInputSource().setByteStream(empty_stream())
+          resource.getResourceInputSource().setByteStream(
+            new ByteArrayInputStream(Array()))
         resource
     }
   }