scrollable text;
authorwenzelm
Mon, 23 Apr 2012 23:55:06 +0200
changeset 47710 4ced56100757
parent 47709 7d292190c4ab
child 47711 c1cca2a052e4
scrollable text;
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