--- 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 =>