--- 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) = {