use view root as parent for popup, which provides more space and avoids confusion of mouse wheel handlers on Windows (wrt. text area scrollbar);
authorwenzelm
Sun, 25 Aug 2013 13:59:40 +0200
changeset 53187 4786e4447cd2
parent 53186 0f4d9df1eaec
child 53188 bb5433b13ff2
use view root as parent for popup, which provides more space and avoids confusion of mouse wheel handlers on Windows (wrt. text area scrollbar);
src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Aug 24 23:16:37 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sun Aug 25 13:59:40 2013 +0200
@@ -56,7 +56,7 @@
           }
         old.foreach(_.hide_popup)
 
-        val tip = new Pretty_Tooltip(view, rendering, parent, screen_point, results, info)
+        val tip = new Pretty_Tooltip(view, rendering, screen_point, results, info)
         stack = tip :: rest
         tip.show_popup
         tip
@@ -139,7 +139,6 @@
 class Pretty_Tooltip private(
   view: View,
   rendering: Rendering,
-  parent: JComponent,
   screen_point: Point,
   private val results: Command.Results,
   private val info: Text.Info[XML.Body]) extends JPanel(new BorderLayout)
@@ -220,10 +219,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 root = view.getRootPane
+    val x0 = root.getLocationOnScreen.x
+    val y0 = root.getLocationOnScreen.y
+    val w0 = root.getWidth
+    val h0 = root.getHeight
 
     val (w, h) =
     {
@@ -266,7 +266,7 @@
 
     tip.setSize(new Dimension(w, h))
     tip.setPreferredSize(new Dimension(w, h))
-    PopupFactory.getSharedInstance.getPopup(parent, tip, x, y)
+    PopupFactory.getSharedInstance.getPopup(root, tip, x, y)
   }
 
   private def show_popup