src/Tools/Graphview/tree_panel.scala

--- a/src/Tools/Graphview/tree_panel.scala	Tue May 19 18:34:16 2015 +0200
+++ b/src/Tools/Graphview/tree_panel.scala	Wed May 20 22:22:27 2015 +0200
@@ -70,6 +70,7 @@
   private val root = new DefaultMutableTreeNode("Nodes")
 
   val tree = new JTree(root)
+  tree.setRowHeight(0)
 
   tree.addKeyListener(new KeyAdapter {
     override def keyPressed(e: KeyEvent): Unit =