# HG changeset patch
# User wenzelm
# Date 1439233570 -7200
# Node ID 8eb8640d7300bf964cefdcbdc394552850d6e918
# Parent  45bfd18835f1ad028f224c0b01a6d20331463655
more uniform ScrollPane, like graphview;

diff -r 45bfd18835f1 -r 8eb8640d7300 src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Mon Aug 10 20:42:59 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Mon Aug 10 21:06:10 2015 +0200
@@ -12,11 +12,12 @@
 import java.awt.{BorderLayout, Dimension}
 import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent, MouseEvent, MouseAdapter,
   FocusAdapter, FocusEvent}
-import javax.swing.{JTree, JScrollPane, JMenuItem}
+import javax.swing.{JTree, JMenuItem}
 import javax.swing.tree.{DefaultMutableTreeNode, DefaultTreeModel, TreeSelectionModel}
 import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener}
 
-import scala.swing.{Button, Label, Component, SplitPane, Orientation, CheckBox}
+import scala.swing.{Button, Label, Component, ScrollPane, SplitPane, Orientation,
+  CheckBox, BorderPanel}
 import scala.swing.event.ButtonClicked
 
 import org.gjt.sp.jedit.{jEdit, View}
@@ -216,8 +217,10 @@
     }
   })
 
-  val tree_view = new JScrollPane(tree)
-  tree_view.setMinimumSize(new Dimension(200, 50))
+  private val tree_pane = new ScrollPane(Component.wrap(tree))
+  tree_pane.horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always
+  tree_pane.verticalScrollBarPolicy = ScrollPane.BarPolicy.Always
+  tree_pane.minimumSize = new Dimension(200, 100)
 
 
   /* controls */
@@ -337,7 +340,7 @@
 
   val main_panel = new SplitPane(Orientation.Vertical) {
     oneTouchExpandable = true
-    leftComponent = Component.wrap(tree_view)
+    leftComponent = tree_pane
     rightComponent = Component.wrap(pretty_text_area)
   }
   set_content(main_panel)