# HG changeset patch
# User wenzelm
# Date 1335218106 -7200
# Node ID 4ced561007571af1c3dfe785865fcb4e642cae14
# Parent  7d292190c4aba02dd33da75c7df75d6680d7eb95
scrollable text;

diff -r 7d292190c4ab -r 4ced56100757 src/Pure/System/gui_setup.scala
--- a/src/Pure/System/gui_setup.scala	Mon Apr 23 23:50:27 2012 +0200
+++ b/src/Pure/System/gui_setup.scala	Mon Apr 23 23:55:06 2012 +0200
@@ -8,7 +8,8 @@
 
 import java.lang.System
 
-import scala.swing.{Button, FlowPanel, BorderPanel, MainFrame, TextArea, SwingApplication}
+import scala.swing.{ScrollPane, Button, FlowPanel,
+  BorderPanel, MainFrame, TextArea, SwingApplication}
 import scala.swing.event.ButtonClicked
 
 
@@ -34,7 +35,7 @@
     val ok_panel = new FlowPanel(FlowPanel.Alignment.Center)(ok)
 
     val panel = new BorderPanel
-    panel.layout(text) = BorderPanel.Position.Center
+    panel.layout(new ScrollPane(text)) = BorderPanel.Position.Center
     panel.layout(ok_panel) = BorderPanel.Position.South
     contents = panel