--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala Fri Jun 26 21:52:56 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala Fri Jun 26 23:28:46 2009 +0200
@@ -74,7 +74,7 @@
if (state == null)
state_panel.setDocument(null: Document)
else
- state_panel.setDocument(state.result_document, UserAgent.baseURL)
+ state_panel.setDocument(state.result_document, UserAgent.base_URL)
}
})
--- a/src/Tools/jEdit/src/jedit/ScrollerDockable.scala Fri Jun 26 21:52:56 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/ScrollerDockable.scala Fri Jun 26 23:28:46 2009 +0200
@@ -229,7 +229,7 @@
panel.relayout()
})
val document = XML.document(Isabelle_Process.parse_message(Isabelle.system, r))
- panel.setDocument(document, UserAgent.baseURL)
+ panel.setDocument(document, UserAgent.base_URL)
val sa = new SelectionActions
sa.install(panel)
panel
--- 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