tuned;
authorwenzelm
Wed, 05 Aug 2015 20:19:51 +0200
changeset 60849 6e49311ef842
parent 60848 7ec20b1c8dc9
child 60850 d5d776c8a7e2
tuned;
src/Tools/Graphview/tree_panel.scala
src/Tools/jEdit/src/debugger_dockable.scala
src/Tools/jEdit/src/documentation_dockable.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)
 
 
--- 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)
 }