--- 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
}
}