1.1 --- a/src/Pure/GUI/gui.scala	Sun Aug 10 13:06:26 2014 +0200
     1.2 +++ b/src/Pure/GUI/gui.scala	Sun Aug 10 13:59:08 2014 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  import java.awt.{Image, Component, Container, Toolkit, Window, Font, KeyboardFocusManager}
     1.5  import java.awt.font.{TextAttribute, TransformAttribute, FontRenderContext, LineMetrics}
     1.6  import java.awt.geom.AffineTransform
     1.7 -import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow,
     1.8 +import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow, JDialog,
     1.9    JButton, JTextField}
    1.10  
    1.11  import scala.collection.convert.WrapAsJava
    1.12 @@ -208,8 +208,9 @@
    1.13  
    1.14    def layered_pane(component: Component): Option[JLayeredPane] =
    1.15      parent_window(component) match {
    1.16 -      case Some(window: JWindow) => Some(window.getLayeredPane)
    1.17 -      case Some(frame: JFrame) => Some(frame.getLayeredPane)
    1.18 +      case Some(w: JWindow) => Some(w.getLayeredPane)
    1.19 +      case Some(w: JFrame) => Some(w.getLayeredPane)
    1.20 +      case Some(w: JDialog) => Some(w.getLayeredPane)
    1.21        case _ => None
    1.22      }
    1.23