src/Tools/jEdit/src/pretty_tooltip.scala

--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Thu Nov 22 17:01:20 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Thu Nov 22 17:11:26 2012 +0100
@@ -115,6 +115,7 @@
     val w = (font_metrics.charWidth(Pretty.spc) * (margin + 2)) min (screen.width / 2)
     val h = (font_metrics.getHeight * (lines + 2)) min (screen.height / 2)
     pretty_text_area.setPreferredSize(new Dimension(w, h))
+    window.pack
   }
 
   {
@@ -128,7 +129,6 @@
   }
 
   window.setVisible(true)
-  window.pack
   pretty_text_area.refresh()
 }