# HG changeset patch
# User wenzelm
# Date 1346417549 -7200
# Node ID 2f0530b81c45dc4eecaa6984b9ffc16b08e2b9f1
# Parent  d7a1973b063cabee6d3f6f8bc9e6bcba16d910fd
recovered ScrollPane from d899be1cfe6d;

diff -r d7a1973b063c -r 2f0530b81c45 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 */