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