recovered ScrollPane from d899be1cfe6d;
authorwenzelm
Fri, 31 Aug 2012 14:52:29 +0200
changeset 49038 2f0530b81c45
parent 49037 d7a1973b063c
child 49039 e780d1bf767e
recovered ScrollPane from d899be1cfe6d;
src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Fri Aug 31 14:35:04 2012 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Fri Aug 31 14:52:29 2012 +0200
@@ -10,7 +10,7 @@
 import isabelle._
 
 import scala.actors.Actor._
-import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, Component}
+import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, ScrollPane, Component}
 import scala.swing.event.{ButtonClicked, MouseClicked, SelectionChanged}
 
 import java.lang.System
@@ -36,7 +36,7 @@
   status.peer.setLayoutOrientation(JList.VERTICAL_WRAP)
   status.selection.intervalMode = ListView.IntervalMode.Single
 
-  set_content(status)
+  set_content(new ScrollPane(status))
 
 
   /* controls */