pack window before accessing its geometry;
authorwenzelm
Thu, 22 Nov 2012 17:11:26 +0100
changeset 50169 071902349e3e
parent 50168 4a575ef46466
child 50171 d655dda100c5
pack window before accessing its geometry;
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()
 }