--- a/src/Tools/Graphview/tree_panel.scala Wed Aug 05 20:04:21 2015 +0200
+++ b/src/Tools/Graphview/tree_panel.scala Wed Aug 05 20:19:51 2015 +0200
@@ -88,7 +88,7 @@
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(100, 100)
+ tree_pane.minimumSize = new Dimension(200, 100)
tree_pane.peer.getVerticalScrollBar.setUnitIncrement(10)
--- a/src/Tools/jEdit/src/debugger_dockable.scala Wed Aug 05 20:04:21 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Wed Aug 05 20:19:51 2015 +0200
@@ -136,7 +136,7 @@
})
val tree_view = new JScrollPane(tree)
- tree_view.setMinimumSize(new Dimension(100, 50))
+ tree_view.setMinimumSize(new Dimension(200, 50))
/* controls */
--- a/src/Tools/jEdit/src/documentation_dockable.scala Wed Aug 05 20:04:21 2015 +0200
+++ b/src/Tools/jEdit/src/documentation_dockable.scala Wed Aug 05 20:19:51 2015 +0200
@@ -120,7 +120,7 @@
}
private val tree_view = new JScrollPane(tree)
- tree_view.setMinimumSize(new Dimension(100, 50))
+ tree_view.setMinimumSize(new Dimension(200, 50))
set_content(tree_view)
}