confine popup to parent component, to avoid javax.swing.PopupFactory$HeavyWeightPopup and its problems with Linux window management and Mac OS X key handling;
authorwenzelm
Sat, 24 Aug 2013 18:29:23 +0200
changeset 53184 5d6ffb87ee08
parent 53183 018d71bee930
child 53185 752e05d09708
confine popup to parent component, to avoid javax.swing.PopupFactory$HeavyWeightPopup and its problems with Linux window management and Mac OS X key handling;
src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Aug 24 17:41:57 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Aug 24 18:29:23 2013 +0200
@@ -220,6 +220,11 @@
   {
     val screen_bounds = JEdit_Lib.screen_bounds(screen_point)
 
+    val x0 = parent.getLocationOnScreen.x
+    val y0 = parent.getLocationOnScreen.y
+    val w0 = parent.getWidth
+    val h0 = parent.getHeight
+
     val (w, h) =
     {
       val painter = pretty_text_area.getPainter
@@ -235,25 +240,32 @@
       val bounds = rendering.tooltip_bounds
 
       val h1 = painter.getFontMetrics.getHeight * (lines + 1) + geometry.deco_height
-      val h2 = (screen_bounds.height * bounds).toInt
+      val h2 = h0 min (screen_bounds.height * bounds).toInt
       val h = h1 min h2
 
       val margin1 =
         if (h1 <= h2)
           (0.0 /: split_lines(XML.content(formatted)))({ case (m, line) => m max metric(line) })
         else margin
-      val w =
-        ((metric.unit * (margin1 + metric.average)).round.toInt + geometry.deco_width) min
-        (screen_bounds.width * bounds).toInt
+
+      val w1 = (metric.unit * (margin1 + metric.average)).round.toInt + geometry.deco_width
+      val w2 = w0 min (screen_bounds.width * bounds).toInt
+      val w = w1 min w2
 
       (w, h)
     }
 
+    val (x, y) =
+    {
+      val x1 = x0 + w0 - w
+      val y1 = y0 + h0 - h
+      val x2 = screen_point.x min (screen_bounds.x + screen_bounds.width - w)
+      val y2 = screen_point.y min (screen_bounds.y + screen_bounds.height - h)
+      ((x2 min x1) max x0, (y2 min y1) max y0)
+    }
+
     tip.setSize(new Dimension(w, h))
     tip.setPreferredSize(new Dimension(w, h))
-
-    val x = screen_point.x min (screen_bounds.x + screen_bounds.width - tip.getWidth)
-    val y = screen_point.y min (screen_bounds.y + screen_bounds.height - tip.getHeight)
     PopupFactory.getSharedInstance.getPopup(parent, tip, x, y)
   }