# HG changeset patch
# User immler@in.tum.de
# Date 1225632738 -3600
# Node ID 1714aeef838840714e82b7350201e47550365a3f
# Parent  abea94120f4b9cc570647b394020154a413bf7cc
renamed class

diff -r abea94120f4b -r 1714aeef8388 src/Tools/jEdit/src/jedit/ScrollerDockable.scala
--- a/src/Tools/jEdit/src/jedit/ScrollerDockable.scala	Sun Nov 02 14:31:18 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/ScrollerDockable.scala	Sun Nov 02 14:32:18 2008 +0100
@@ -1,5 +1,5 @@
 /*
- * LazyScroller.scala
+ * ScrollerDockable.scala
  *
  * TODO: clearer seperation of tasks: layout message_view, layout panel (with preferredsize), repaint, relayout, ...
  * + relayout on ValueIsAdjusting while scrolling
@@ -30,7 +30,7 @@
 
 import org.gjt.sp.jedit.View
 
-object LazyScroller {
+object ScrollerDockable {
   val baseURL = "file://localhost" + getenv("ISABELLE_HOME") + "/lib/html/"
   val userStylesheet = 
     "file://localhost" + getenv("ISABELLE_HOME_USER") + "/etc/user.css";
@@ -49,7 +49,7 @@
 }
 
 
-class LazyScroller(view : View, position : String) extends JPanel with AdjustmentListener with ComponentListener {
+class ScrollerDockable(view : View, position : String) extends JPanel with AdjustmentListener with ComponentListener {
   //holding the unrendered messages
   val message_buffer = new ArrayBuffer[Document]()
   //rendered messages
@@ -86,7 +86,7 @@
       panel.relayout()
     })
 
-    panel.setDocument(message, LazyScroller.baseURL)
+    panel.setDocument(message, ScrollerDockable.baseURL)
     panel
   }