# HG changeset patch
# User wenzelm
# Date 1379788263 -7200
# Node ID 29eaacff407840f396a0bdfd357d5b122022b8d9
# Parent  06a6216f733ed338b8646695f14bb4c7b9bce6fd
proper layered pane at root of parent component, not global view (e.g. relevant for tooltips for detached info windows);

diff -r 06a6216f733e -r 29eaacff4078 src/Pure/System/gui.scala
--- a/src/Pure/System/gui.scala	Sat Sep 21 19:48:46 2013 +0200
+++ b/src/Pure/System/gui.scala	Sat Sep 21 20:31:03 2013 +0200
@@ -8,7 +8,7 @@
 
 
 import java.awt.{Image, Component, Container, Toolkit, Window}
-import javax.swing.{ImageIcon, JOptionPane, UIManager}
+import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow}
 
 import scala.swing.{ComboBox, TextArea, ScrollPane}
 import scala.swing.event.SelectionChanged
@@ -143,5 +143,12 @@
 
   def parent_window(component: Component): Option[Window] =
     ancestors(component).collectFirst({ case x: Window => x })
+
+  def layered_pane(component: Component): Option[JLayeredPane] =
+    parent_window(component) match {
+      case Some(window: JWindow) => Some(window.getLayeredPane)
+      case Some(frame: JFrame) => Some(frame.getLayeredPane)
+      case _ => None
+    }
 }
 
diff -r 06a6216f733e -r 29eaacff4078 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Sep 21 19:48:46 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Sep 21 20:31:03 2013 +0200
@@ -11,7 +11,7 @@
 
 import java.awt.{Color, Point, BorderLayout, Dimension}
 import java.awt.event.{FocusAdapter, FocusEvent}
-import javax.swing.{JPanel, JComponent, SwingUtilities}
+import javax.swing.{JPanel, JComponent, SwingUtilities, JLayeredPane}
 import javax.swing.border.LineBorder
 
 import scala.swing.{FlowPanel, Label}
@@ -42,25 +42,28 @@
     location: Point,
     rendering: Rendering,
     results: Command.Results,
-    info: Text.Info[XML.Body]): Pretty_Tooltip =
+    info: Text.Info[XML.Body])
   {
     Swing_Thread.require()
 
     stack match {
       case top :: _ if top.results == results && top.info == info => top
       case _ =>
-        val (old, rest) =
-          GUI.ancestors(parent).collectFirst({ case x: Pretty_Tooltip => x }) match {
-            case Some(tip) => hierarchy(tip).getOrElse((stack, Nil))
-            case None => (stack, Nil)
-          }
-        old.foreach(_.hide_popup)
+        GUI.layered_pane(parent) match {
+          case None =>
+          case Some(layered) =>
+            val (old, rest) =
+              GUI.ancestors(parent).collectFirst({ case x: Pretty_Tooltip => x }) match {
+                case Some(tip) => hierarchy(tip).getOrElse((stack, Nil))
+                case None => (stack, Nil)
+              }
+            old.foreach(_.hide_popup)
 
-        val loc = SwingUtilities.convertPoint(parent, location, view.getLayeredPane)
-        val tip = new Pretty_Tooltip(view, loc, rendering, results, info)
-        stack = tip :: rest
-        tip.show_popup
-        tip
+            val loc = SwingUtilities.convertPoint(parent, location, layered)
+            val tip = new Pretty_Tooltip(view, layered, loc, rendering, results, info)
+            stack = tip :: rest
+            tip.show_popup
+        }
     }
   }
 
@@ -139,6 +142,7 @@
 
 class Pretty_Tooltip private(
   view: View,
+  layered: JLayeredPane,
   location: Point,
   rendering: Rendering,
   private val results: Command.Results,
@@ -218,7 +222,6 @@
 
   private val popup =
   {
-    val layered = view.getLayeredPane
     val screen = JEdit_Lib.screen_location(layered, location)
     val size =
     {