# HG changeset patch
# User immler@in.tum.de
# Date 1225727852 -3600
# Node ID aa0d2f0bde83d19cc03a7e45155e72fcf5e32825
# Parent  74ddfd2cf5a5575dcd8209311f8388c3957f410b
UserAgent as seperate class, moved stylesheets, baseURL to UserAgent

diff -r 74ddfd2cf5a5 -r aa0d2f0bde83 src/Tools/jEdit/src/jedit/ScrollerDockable.scala
--- a/src/Tools/jEdit/src/jedit/ScrollerDockable.scala	Mon Nov 03 16:03:11 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/ScrollerDockable.scala	Mon Nov 03 16:57:32 2008 +0100
@@ -30,25 +30,6 @@
 
 import org.gjt.sp.jedit.View
 
-object ScrollerDockable {
-  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 ScrollerDockable(view : View, position : String) extends JPanel with AdjustmentListener with ComponentListener {
   //holding the unrendered messages
   val message_buffer = new ArrayBuffer[Document]()
@@ -86,7 +67,7 @@
       panel.relayout()
     })
 
-    panel.setDocument(message, ScrollerDockable.baseURL)
+    panel.setDocument(message, UserAgent.baseURL)
     panel
   }
   
@@ -99,22 +80,27 @@
    
   //render and load a message into cache, place its bottom at y-coordinate;
   def set_message (message_no: Int, y: Int) = {
-    //get or add panel from/to cache
+    //add panel to cache if necessary
     if(!message_cache.isDefinedAt(message_no)){
       if(message_buffer.isDefinedAt(message_no)){
         message_cache = message_cache.update (message_no, render (message_buffer(message_no)))
       }
     }
-    val panel = message_cache.get(message_no).get
-    // recalculate preferred sie after resizing
-    if(panel.getPreferredSize.getWidth.toInt != message_view.getWidth)
-      calculate_preferred_size (panel)
-    //place message on view
-    val width = panel.getPreferredSize.getWidth.toInt
-    val height = panel.getPreferredSize.getHeight.toInt
-    panel.setBounds(0, y - height, width, height)
-    message_view.add(panel)
-    panel
+    val result = message_cache.get(message_no) match {
+      case Some(panel) => {
+        // recalculate preferred sie after resizing
+        if(panel.getPreferredSize.getWidth.toInt != message_view.getWidth)
+          calculate_preferred_size (panel)
+        //place message on view
+        val width = panel.getPreferredSize.getWidth.toInt
+        val height = panel.getPreferredSize.getHeight.toInt
+        panel.setBounds(0, y - height, width, height)
+        message_view.add(panel)
+        panel
+      }
+      case None => null
+    }
+    result
   }
   
   def move_view (y : Int) = {
diff -r 74ddfd2cf5a5 -r aa0d2f0bde83 src/Tools/jEdit/src/jedit/StateViewDockable.scala
--- a/src/Tools/jEdit/src/jedit/StateViewDockable.scala	Mon Nov 03 16:03:11 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/StateViewDockable.scala	Mon Nov 03 16:57:32 2008 +0100
@@ -1,57 +1,18 @@
 package isabelle.jedit
 
-import java.io.{ ByteArrayInputStream, FileInputStream, InputStream }
 
 import java.awt.GridLayout
-import javax.swing.{ JPanel, JTextArea, JScrollPane }
+import javax.swing.{ JPanel, JScrollPane }
 
 import isabelle.IsabelleSystem.getenv
 
-import org.xml.sax.InputSource;
-
 import org.w3c.dom.Document
 
 import org.xhtmlrenderer.simple.XHTMLPanel
 import org.xhtmlrenderer.context.AWTFontResolver
-import org.xhtmlrenderer.swing.NaiveUserAgent
-import org.xhtmlrenderer.resource.CSSResource
 
 import org.gjt.sp.jedit.View
 
-object StateViewDockable {
-  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 == StateViewDockable.baseURL + "style")
-      new CSSResource(
-        new ByteArrayInputStream(StateViewDockable.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 StateViewDockable(view : View, position : String) extends JPanel {
   {
     val panel = new XHTMLPanel(new UserAgent())
@@ -74,7 +35,7 @@
       if (state == null)
         panel.setDocument(null : Document)
       else
-        panel.setDocument(state.document, StateViewDockable.baseURL)
+        panel.setDocument(state.document, UserAgent.baseURL)
     })
   }
 }
diff -r 74ddfd2cf5a5 -r aa0d2f0bde83 src/Tools/jEdit/src/jedit/UserAgent.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/UserAgent.scala	Mon Nov 03 16:57:32 2008 +0100
@@ -0,0 +1,39 @@
+package isabelle.jedit
+
+import java.io.ByteArrayInputStream
+import org.xhtmlrenderer.swing.NaiveUserAgent
+import org.xhtmlrenderer.resource.CSSResource
+import isabelle.IsabelleSystem.getenv
+
+object UserAgent {
+  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