# HG changeset patch
# User wenzelm
# Date 1363450599 -3600
# Node ID c5605f3c84b0283c52fce397540a6af1c0a2705f
# Parent  b10b64679c5b13b94f09e2401173542f6d2f9716
some more hammering to convince JDK 7 (and 8-ea) on Mac OS X about window size change;

diff -r b10b64679c5b -r c5605f3c84b0 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Mar 16 12:46:22 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Mar 16 17:16:39 2013 +0100
@@ -104,6 +104,7 @@
       XML.traverse_text(Pretty.formatted(body, margin, Pretty.font_metric(fm)))(0)(
         (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
 
+    window.setSize(new Dimension(100, 100))
     window.setPreferredSize(new Dimension(100, 100))
     window.pack
     val deco_width = window.getWidth - painter.getWidth
@@ -117,8 +118,10 @@
       (fm.getHeight * (lines + 1) + deco_height) min
       (screen_bounds.height * bounds).toInt
 
+    window.setSize(new Dimension(w, h))
     window.setPreferredSize(new Dimension(w, h))
     window.pack
+    window.revalidate
 
     val x = screen_point.x min (screen_bounds.x + screen_bounds.width - window.getWidth)
     val y = screen_point.y min (screen_bounds.y + screen_bounds.height - window.getHeight)