src/Pure/GUI/gui.scala
changeset 57879 91e188508bc9
parent 57639 ba170c8ea578
child 57908 1937603dbdf2
equal deleted inserted replaced
57878:51a2f9140175 57879:91e188508bc9
    10 
    10 
    11 import java.lang.{ClassLoader, ClassNotFoundException, NoSuchMethodException}
    11 import java.lang.{ClassLoader, ClassNotFoundException, NoSuchMethodException}
    12 import java.awt.{Image, Component, Container, Toolkit, Window, Font, KeyboardFocusManager}
    12 import java.awt.{Image, Component, Container, Toolkit, Window, Font, KeyboardFocusManager}
    13 import java.awt.font.{TextAttribute, TransformAttribute, FontRenderContext, LineMetrics}
    13 import java.awt.font.{TextAttribute, TransformAttribute, FontRenderContext, LineMetrics}
    14 import java.awt.geom.AffineTransform
    14 import java.awt.geom.AffineTransform
    15 import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow,
    15 import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow, JDialog,
    16   JButton, JTextField}
    16   JButton, JTextField}
    17 
    17 
    18 import scala.collection.convert.WrapAsJava
    18 import scala.collection.convert.WrapAsJava
    19 import scala.swing.{ComboBox, TextArea, ScrollPane}
    19 import scala.swing.{ComboBox, TextArea, ScrollPane}
    20 import scala.swing.event.SelectionChanged
    20 import scala.swing.event.SelectionChanged
   206   def parent_window(component: Component): Option[Window] =
   206   def parent_window(component: Component): Option[Window] =
   207     ancestors(component).collectFirst({ case x: Window => x })
   207     ancestors(component).collectFirst({ case x: Window => x })
   208 
   208 
   209   def layered_pane(component: Component): Option[JLayeredPane] =
   209   def layered_pane(component: Component): Option[JLayeredPane] =
   210     parent_window(component) match {
   210     parent_window(component) match {
   211       case Some(window: JWindow) => Some(window.getLayeredPane)
   211       case Some(w: JWindow) => Some(w.getLayeredPane)
   212       case Some(frame: JFrame) => Some(frame.getLayeredPane)
   212       case Some(w: JFrame) => Some(w.getLayeredPane)
       
   213       case Some(w: JDialog) => Some(w.getLayeredPane)
   213       case _ => None
   214       case _ => None
   214     }
   215     }
   215 
   216 
   216 
   217 
   217   /* font operations */
   218   /* font operations */