src/Tools/jEdit/src/renderer/UserAgent.scala

--- a/src/Tools/jEdit/src/renderer/UserAgent.scala	Fri Jun 26 21:52:56 2009 +0200
+++ b/src/Tools/jEdit/src/renderer/UserAgent.scala	Fri Jun 26 23:28:46 2009 +0200
@@ -7,21 +7,24 @@
 
 package isabelle.renderer
 
+import isabelle.jedit.Isabelle
 
-import java.io.ByteArrayInputStream
+import java.io.{InputStream, ByteArrayInputStream, FileInputStream}
+
 import org.xhtmlrenderer.swing.NaiveUserAgent
 import org.xhtmlrenderer.resource.CSSResource
 
 
-object UserAgent {
+object UserAgent
+{
   // FIXME avoid static getenv
-  val baseURL = "file://localhost" + System.getenv("ISABELLE_HOME") + "/lib/html/"
-  val userStylesheet =  "file://localhost" + System.getenv("ISABELLE_HOME_USER") + "/etc/user.css"
+  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 = """
-
 @import "isabelle.css";
-
-@import '""" + userStylesheet + """';
+@import 'isabelle_user.css';
 
 messages, message {
   display: block;
@@ -31,18 +34,34 @@
 """ 
 }
 
-class UserAgent extends NaiveUserAgent {
-  override def getCSSResource(uri : String) : CSSResource = {
-    if (uri == UserAgent.baseURL + "style")
-      new CSSResource(
-        new ByteArrayInputStream(UserAgent.stylesheet.getBytes()))
-    else {
-      val stream = resolveAndOpenStream(uri)
-      val resource = new CSSResource(stream)
-      if (stream == null)
-        resource.getResourceInputSource().setByteStream(
-          new ByteArrayInputStream(new Array[Byte](0)))
-      resource
+class UserAgent extends NaiveUserAgent
+{
+  private def empty_stream(): InputStream =
+    new ByteArrayInputStream(new Array[Byte](0))
+
+  private def try_file_stream(name: String): InputStream =
+  {
+    val file = Isabelle.system.platform_file(name)
+    if (file.exists) new FileInputStream(file)
+    else empty_stream()
+  }
+
+  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 _ =>
+        val stream = resolveAndOpenStream(uri)
+        val resource = new CSSResource(stream)
+        if (stream == null)
+          resource.getResourceInputSource().setByteStream(empty_stream())
+        resource
     }
   }
 }
\ No newline at end of file