cell-specific row height based on its font, e.g. relevant for DPI scaling on Windows;

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

--- a/src/Tools/jEdit/src/documentation_dockable.scala	Tue May 19 18:34:16 2015 +0200
+++ b/src/Tools/jEdit/src/documentation_dockable.scala	Wed May 20 22:22:27 2015 +0200
@@ -46,6 +46,7 @@
   }
 
   private val tree = new JTree(root)
+  tree.setRowHeight(0)
 
   override def focusOnDefaultComponent { tree.requestFocusInWindow }