# HG changeset patch
# User wenzelm
# Date 1432153347 -7200
# Node ID ba3c716144dd4e30d6111719f0b0a701a6537a95
# Parent  4335ee20014e2670334ec328e0b7064ef631aab6
cell-specific row height based on its font, e.g. relevant for DPI scaling on Windows;

diff -r 4335ee20014e -r ba3c716144dd 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 =
diff -r 4335ee20014e -r ba3c716144dd src/Tools/jEdit/src/documentation_dockable.scala
--- 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 }