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 }