# HG changeset patch
# User wenzelm
# Date 1350079716 -7200
# Node ID 19ea3242ec37566261fe8753c706174edb01733a
# Parent  afddf4e26facfb2c9c134138c300595b42e325e0
improved adhoc height for small fonts;

diff -r afddf4e26fac -r 19ea3242ec37 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Oct 12 23:38:48 2012 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Oct 13 00:08:36 2012 +0200
@@ -113,7 +113,7 @@
 
     val screen = Toolkit.getDefaultToolkit.getScreenSize
     val w = (font_metrics.charWidth(Pretty.spc) * margin) min (screen.width / 2)
-    val h = (font_metrics.getHeight * (lines + 3)) min (screen.height / 2)
+    val h = (font_metrics.getHeight * (lines + 2) + 25) min (screen.height / 2)
     window.setSize(w, h)
   }