# HG changeset patch
# User wenzelm
# Date 1363633357 -3600
# Node ID 67542078fa2159f2e0b5d076d9eb1313142616f0
# Parent  66824fea1a72a47a0195f16e8cf3a5dd32581223
prefer ownerless window, to avoid question of potentially changing parent view;

diff -r 66824fea1a72 -r 67542078fa21 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Mon Mar 18 19:33:25 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Mon Mar 18 20:02:37 2013 +0100
@@ -43,17 +43,20 @@
   {
     Swing_Thread.require()
 
-    val parent_window = JEdit_Lib.parent_window(parent) getOrElse view
+    val old_windows =
+      JEdit_Lib.parent_window(parent) match {
+        case Some(parent_window: Pretty_Tooltip) =>
+          windows().find(_ == parent_window) match {
+            case Some(window) => window.descendants()
+            case None => windows()
+          }
+        case _ => windows()
+      }
 
-    val old_windows =
-      windows().find(_ == parent_window) match {
-        case None => windows()
-        case Some(window) => window.descendants()
-      }
     val window =
       old_windows.reverse match {
         case Nil =>
-          val window = new Pretty_Tooltip(view, parent_window)
+          val window = new Pretty_Tooltip(view)
           window_stack = window :: window_stack
           window
         case window :: others =>
@@ -89,8 +92,7 @@
 }
 
 
-class Pretty_Tooltip private(view: View, parent_window: Window)
-  extends JDialog(parent_window)
+class Pretty_Tooltip private(view: View) extends JDialog
 {
   window =>