improved adhoc height for small fonts;

--- 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)
   }