--- a/src/Tools/jEdit/src/jedit/LazyScroller.scala Thu Oct 23 14:16:04 2008 +0200
+++ b/src/Tools/jEdit/src/jedit/LazyScroller.scala Sun Oct 26 00:10:39 2008 +0200
@@ -59,11 +59,10 @@
message_view.setLayout(new GridLayout(1,1))
// setting up view
setLayout(new BorderLayout())
- val pane = new JScrollPane(message_view, ScrollPaneConstants.VERTICAL_SCROLLBAR_NEVER, ScrollPaneConstants.HORIZONTAL_SCROLLBAR_ALWAYS)
val vscroll = new JScrollBar(Adjustable.VERTICAL, 0, 1, 0, 1)
vscroll.addAdjustmentListener(this)
add (vscroll, BorderLayout.EAST)
- add (pane, BorderLayout.CENTER)
+ add (message_view, BorderLayout.CENTER)
// subclasses should implement this
@@ -73,7 +72,9 @@
// - render only when necessary
def update_view = {
message_view.removeAll()
- message_view.add (render (message_buffer(message_no)))
+ val rendered_message = render (message_buffer(message_no))
+ val resizable = new JScrollPane(rendered_message, ScrollPaneConstants.VERTICAL_SCROLLBAR_NEVER, ScrollPaneConstants.HORIZONTAL_SCROLLBAR_NEVER)
+ message_view.add (resizable)
}
def update_scrollbar = {
@@ -107,14 +108,14 @@
case _ =>
}
}
-}
+ }
class XMLScroller(view : View, position : String) extends LazyScroller[Document] {
Plugin.plugin.stateUpdate.add(state => {
var i = 0
- if(state != null) while (i < 10000) {
+ if(state != null) while (i < 1000) {
add_message(state.document)
i += 1
}