auto-scrolling
authorimmler@in.tum.de
Wed, 05 Nov 2008 15:33:52 +0100
changeset 34356 3d6f4dd10e63
parent 34355 3ae10f5d40aa
child 34357 61674cd653f9
auto-scrolling
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
     }