# HG changeset patch
# User immler@in.tum.de
# Date 1225895632 -3600
# Node ID 3d6f4dd10e63ca6270803b269ee4827dcba374f2
# Parent  3ae10f5d40aa520a07dcf129f438af2ba1113659
auto-scrolling

diff -r 3ae10f5d40aa -r 3d6f4dd10e63 src/Tools/jEdit/src/jedit/ScrollerDockable.scala
--- a/src/Tools/jEdit/src/jedit/ScrollerDockable.scala	Mon Nov 03 18:44:48 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/ScrollerDockable.scala	Wed Nov 05 15:33:52 2008 +0100
@@ -162,11 +162,16 @@
     repaint()
   }
 
+  def jump_to_bottom = {
+    //fire scroll-event => updating is done by scroller
+    vscroll.setValue(message_buffer.size - 1)
+  }
+
   def add_message (message: Document) = {
     message_buffer += message
     vscroll.setMaximum (Math.max(1, message_buffer.length))
-    if(message_no == -1){
-      message_no = 0
+    if(message_no == -1 || auto_scroll.isSelected){
+      jump_to_bottom
       update_view
     }
   }
@@ -193,7 +198,7 @@
   // TODO: only testing atm
   Plugin.plugin.stateUpdate.add(state => {
     var i = 0
-    if(state != null) while (i < 500) {
+    if(state != null) while (i < 5) {
       add_message(state.document)
       i += 1
     }