# HG changeset patch
# User immler@in.tum.de
# Date 1225896833 -3600
# Node ID 61674cd653f93a5cd07b978f6af40bec84260977
# Parent  3d6f4dd10e63ca6270803b269ee4827dcba374f2
scroll to first message immediately; potential later messages periodically

diff -r 3d6f4dd10e63 -r 61674cd653f9 src/Tools/jEdit/src/jedit/ScrollerDockable.scala
--- a/src/Tools/jEdit/src/jedit/ScrollerDockable.scala	Wed Nov 05 15:33:52 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/ScrollerDockable.scala	Wed Nov 05 15:53:53 2008 +0100
@@ -14,8 +14,8 @@
 
 import java.awt.{ BorderLayout, GridLayout, Adjustable, Rectangle, Scrollbar }
 import java.awt.image.BufferedImage
-import java.awt.event.{ AdjustmentListener, AdjustmentEvent, ComponentListener, ComponentEvent }
-import javax.swing.{ JPanel, JRadioButton, JScrollBar, JScrollPane, JTextArea, ScrollPaneConstants }
+import java.awt.event.{ ActionListener, ActionEvent, AdjustmentListener, AdjustmentEvent, ComponentListener, ComponentEvent }
+import javax.swing.{ JPanel, JRadioButton, JScrollBar, JScrollPane, JTextArea, ScrollPaneConstants, Timer }
 
 import isabelle.IsabelleSystem.getenv
 
@@ -162,9 +162,21 @@
     repaint()
   }
 
+  val scroll_delay_timer : Timer = new Timer(200, new ActionListener {
+      override def actionPerformed(e:ActionEvent){
+        //fire scroll-event => updating is done by scroller
+        if(message_no != message_buffer.size) vscroll.setValue(message_buffer.size - 1)
+        scroll_delay_timer.stop
+      }
+    })
+
   def jump_to_bottom = {
-    //fire scroll-event => updating is done by scroller
-    vscroll.setValue(message_buffer.size - 1)
+    if (scroll_delay_timer.isRunning())
+      scroll_delay_timer.restart()
+    else{
+      vscroll.setValue(message_buffer.size - 1)
+      scroll_delay_timer.start()
+    }
   }
 
   def add_message (message: Document) = {