--- 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