# HG changeset patch
# User wenzelm
# Date 1438798791 -7200
# Node ID 6e49311ef842d0be5604e0b12a5ba7a96f63de97
# Parent  7ec20b1c8dc9aafbaba4e9bd8c6a5ebf647d29ed
tuned;

diff -r 7ec20b1c8dc9 -r 6e49311ef842 src/Tools/Graphview/tree_panel.scala
--- 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)
 
 
diff -r 7ec20b1c8dc9 -r 6e49311ef842 src/Tools/jEdit/src/debugger_dockable.scala
--- 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 */
diff -r 7ec20b1c8dc9 -r 6e49311ef842 src/Tools/jEdit/src/documentation_dockable.scala
--- 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)
 }