# HG changeset patch
# User wenzelm
# Date 1229888169 -3600
# Node ID ee19d8ef5dc3bb52b7e7e28d0de7ef3487d65ebc
# Parent  03afc73e185fe5b598673831ceb29b26e7caa58b
renamed isabelle.jedit.UserAgent to isabelle.renderer.UserAgent;

diff -r 03afc73e185f -r ee19d8ef5dc3 src/Tools/jEdit/src/jedit/UserAgent.scala
--- a/src/Tools/jEdit/src/jedit/UserAgent.scala	Sun Dec 21 20:16:43 2008 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-/*
- * XML/CSS rendering -- user agent
- *
- * @author Fabian Immler, TU Munich
- * @author Johannes Hölzl, TU Munich
- */
-
-package isabelle.jedit
-
-import java.io.ByteArrayInputStream
-import org.xhtmlrenderer.swing.NaiveUserAgent
-import org.xhtmlrenderer.resource.CSSResource
-import isabelle.IsabelleSystem.getenv
-
-object UserAgent {
-  // FIXME avoid static getenv
-  val baseURL = "file://localhost" + getenv("ISABELLE_HOME") + "/lib/html/"
-  val userStylesheet =  "file://localhost" + getenv("ISABELLE_HOME_USER") + "/etc/user.css"
-  val stylesheet = """
-
-@import "isabelle.css";
-
-@import '""" + userStylesheet + """';
-
-messages, message {
-  display: block;
-  white-space: pre-wrap;
-  font-family: Isabelle;
-}
-""" 
-}
-
-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
-    }
-  }
-}
\ No newline at end of file
diff -r 03afc73e185f -r ee19d8ef5dc3 src/Tools/jEdit/src/renderer/UserAgent.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/renderer/UserAgent.scala	Sun Dec 21 20:36:09 2008 +0100
@@ -0,0 +1,49 @@
+/*
+ * XML/CSS rendering -- user agent
+ *
+ * @author Fabian Immler, TU Munich
+ * @author Johannes Hölzl, TU Munich
+ */
+
+package isabelle.renderer
+
+
+import java.io.ByteArrayInputStream
+import org.xhtmlrenderer.swing.NaiveUserAgent
+import org.xhtmlrenderer.resource.CSSResource
+import isabelle.IsabelleSystem.getenv
+
+
+object UserAgent {
+  // FIXME avoid static getenv
+  val baseURL = "file://localhost" + getenv("ISABELLE_HOME") + "/lib/html/"
+  val userStylesheet =  "file://localhost" + getenv("ISABELLE_HOME_USER") + "/etc/user.css"
+  val stylesheet = """
+
+@import "isabelle.css";
+
+@import '""" + userStylesheet + """';
+
+messages, message {
+  display: block;
+  white-space: pre-wrap;
+  font-family: Isabelle;
+}
+""" 
+}
+
+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
+    }
+  }
+}
\ No newline at end of file