prefer ownerless window, to avoid question of potentially changing parent view;
authorwenzelm
Mon, 18 Mar 2013 20:02:37 +0100
changeset 51458 67542078fa21
parent 51457 66824fea1a72
child 51459 bc3651180a09
prefer ownerless window, to avoid question of potentially changing parent view;
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 =>