# HG changeset patch
# User wenzelm
# Date 1377431980 -7200
# Node ID 4786e4447cd2b635925aa8c1daf6569cd89eab6b
# Parent  0f4d9df1eaec030e1cfcec676303e74d7db3abe2
use view root as parent for popup, which provides more space and avoids confusion of mouse wheel handlers on Windows (wrt. text area scrollbar);

diff -r 0f4d9df1eaec -r 4786e4447cd2 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