src/Pure/System/gui.scala
changeset 53712 ea51046be71b
parent 53452 8181bc357dc4
child 53714 89fb20ae9b73
equal deleted inserted replaced
53711:8ce7795256e1 53712:ea51046be71b
     1 /*  Title:      Pure/System/gui.scala
     1 /*  Title:      Pure/System/gui.scala
     2     Author:     Makarius
     2     Author:     Makarius
     3 
     3 
     4 Elementary GUI tools.
     4 Basic GUI tools (for AWT/Swing).
     5 */
     5 */
     6 
     6 
     7 package isabelle
     7 package isabelle
     8 
     8 
     9 
     9 
    10 import java.awt.{Image, Component, Toolkit}
    10 import java.awt.{Image, Component, Container, Toolkit, Window}
    11 import javax.swing.{ImageIcon, JOptionPane, UIManager}
    11 import javax.swing.{ImageIcon, JOptionPane, UIManager}
    12 
    12 
    13 import scala.swing.{ComboBox, TextArea, ScrollPane}
    13 import scala.swing.{ComboBox, TextArea, ScrollPane}
    14 import scala.swing.event.SelectionChanged
    14 import scala.swing.event.SelectionChanged
    15 
    15 
   115 
   115 
   116   def isabelle_icon(): ImageIcon =
   116   def isabelle_icon(): ImageIcon =
   117     new ImageIcon(getClass.getClassLoader.getResource("isabelle/isabelle.gif"))
   117     new ImageIcon(getClass.getClassLoader.getResource("isabelle/isabelle.gif"))
   118 
   118 
   119   def isabelle_image(): Image = isabelle_icon().getImage
   119   def isabelle_image(): Image = isabelle_icon().getImage
       
   120 
       
   121 
       
   122   /* component hierachy */
       
   123 
       
   124   def get_parent(component: Component): Option[Container] =
       
   125     component.getParent match {
       
   126       case null => None
       
   127       case parent => Some(parent)
       
   128     }
       
   129 
       
   130   def ancestors(component: Component): Iterator[Container] = new Iterator[Container] {
       
   131     private var next_elem = get_parent(component)
       
   132     def hasNext(): Boolean = next_elem.isDefined
       
   133     def next(): Container =
       
   134       next_elem match {
       
   135         case Some(parent) =>
       
   136           next_elem = get_parent(parent)
       
   137           parent
       
   138         case None => Iterator.empty.next()
       
   139       }
       
   140   }
       
   141 
       
   142   def parent_window(component: Component): Option[Window] =
       
   143     ancestors(component).collectFirst({ case x: Window => x })
   120 }
   144 }
   121 
   145