# HG changeset patch
# User wenzelm
# Date 1407671948 -7200
# Node ID 91e188508bc9df5de2737325c390836603a3e409
# Parent  51a2f91401756791e50d2f055620602e8447e7e9
proper layered_pane for JDialog, e.g. relevant for floating dockables in jEdit, for completion popup in text field;

diff -r 51a2f9140175 -r 91e188508bc9 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Sun Aug 10 13:06:26 2014 +0200
+++ b/src/Pure/GUI/gui.scala	Sun Aug 10 13:59:08 2014 +0200
@@ -12,7 +12,7 @@
 import java.awt.{Image, Component, Container, Toolkit, Window, Font, KeyboardFocusManager}
 import java.awt.font.{TextAttribute, TransformAttribute, FontRenderContext, LineMetrics}
 import java.awt.geom.AffineTransform
-import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow,
+import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow, JDialog,
   JButton, JTextField}
 
 import scala.collection.convert.WrapAsJava
@@ -208,8 +208,9 @@
 
   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 Some(w: JWindow) => Some(w.getLayeredPane)
+      case Some(w: JFrame) => Some(w.getLayeredPane)
+      case Some(w: JDialog) => Some(w.getLayeredPane)
       case _ => None
     }