# HG changeset patch
# User wenzelm
# Date 1358021520 -3600
# Node ID a667ac8c7afee20010fdd81207e662bb8fad1bb0
# Parent  b756cbce1cd031d38c05bd0b55d9d7042519a82d
forced scroll to bottom, for improved cross-platform appearance;

diff -r b756cbce1cd0 -r a667ac8c7afe src/Pure/Tools/build_dialog.scala
--- a/src/Pure/Tools/build_dialog.scala	Sat Jan 12 20:42:20 2013 +0100
+++ b/src/Pure/Tools/build_dialog.scala	Sat Jan 12 21:12:00 2013 +0100
@@ -81,10 +81,16 @@
       rows = 20
     }
 
+    val scroll_text = new ScrollPane(text)
+
     val progress = new Build.Progress
     {
       override def echo(msg: String): Unit =
-        Swing_Thread.later { text.append(msg + "\n") }
+        Swing_Thread.later {
+          text.append(msg + "\n")
+          val vertical = scroll_text.peer.getVerticalScrollBar
+          vertical.setValue(vertical.getMaximum)
+        }
       override def theory(session: String, theory: String): Unit =
         echo(session + ": theory " + theory)
       override def stopped: Boolean =
@@ -126,7 +132,7 @@
     /* layout panel */
 
     val layout_panel = new BorderPanel
-    layout_panel.layout(new ScrollPane(text)) = BorderPanel.Position.Center
+    layout_panel.layout(scroll_text) = BorderPanel.Position.Center
     layout_panel.layout(action_panel) = BorderPanel.Position.South
 
     contents = layout_panel