# HG changeset patch
# User immler@in.tum.de
# Date 1225734288 -3600
# Node ID 3ae10f5d40aa520a07dcf129f438af2ba1113659
# Parent  110f5f6902dc440b68eda608c434cdb4fb465d80
prepared for automatic scrolling

diff -r 110f5f6902dc -r 3ae10f5d40aa src/Tools/jEdit/src/jedit/ScrollerDockable.scala
--- a/src/Tools/jEdit/src/jedit/ScrollerDockable.scala	Mon Nov 03 17:29:06 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/ScrollerDockable.scala	Mon Nov 03 18:44:48 2008 +0100
@@ -15,7 +15,7 @@
 import java.awt.{ BorderLayout, GridLayout, Adjustable, Rectangle, Scrollbar }
 import java.awt.image.BufferedImage
 import java.awt.event.{ AdjustmentListener, AdjustmentEvent, ComponentListener, ComponentEvent }
-import javax.swing.{ JScrollBar, JPanel, JScrollPane, ScrollPaneConstants }
+import javax.swing.{ JPanel, JRadioButton, JScrollBar, JScrollPane, JTextArea, ScrollPaneConstants }
 
 import isabelle.IsabelleSystem.getenv
 
@@ -36,7 +36,7 @@
   //rendered messages
   var message_cache = Map[Int, XHTMLPanel]()
   // defining the current view
-  val scrollunit = 5
+  val scrollunit = 1
   var message_offset = 0 //how many pixels of the lowest message are hidden
   var message_no = -1  //index of the lowest message
   // absolute positioning for messages
@@ -49,7 +49,13 @@
   add (vscroll, BorderLayout.EAST)
   add (message_view, BorderLayout.CENTER)
   addComponentListener(this)
-
+  //automated scrolling, new message ind
+  val infopanel = new JPanel
+  val auto_scroll = new JRadioButton("Auto Scroll", false)
+  val new_message_ind = new JTextArea("0")
+  infopanel.add(new_message_ind)
+  infopanel.add(auto_scroll)
+  add (infopanel, BorderLayout.SOUTH)
 
   //Render a message to a Panel
   def render (message: Document): XHTMLPanel = {
@@ -138,6 +144,8 @@
             c.setBounds(newrect)
           })
         repaint()
+      } else {
+        vscroll.setValue(message_no)
       }
     }
   }
@@ -166,9 +174,11 @@
   override def adjustmentValueChanged (e : AdjustmentEvent) = {
     //event-handling has to be so general (without UNIT_INCR,...)
     // because all events could be sent as TRACK e.g. on my mac
-    message_no = e.getValue
-    message_offset = 0
-    update_view
+    if (e.getSource == vscroll){
+        message_no = e.getValue
+        message_offset = 0
+        update_view
+    }
   }
 
   // handle Component-Events