src/Pure/GUI/gui.scala

       case Some(w: JFrame) => Some(w.getLayeredPane)
       case Some(w: JDialog) => Some(w.getLayeredPane)
       case _ => None
     }
 
+  def traverse_components(component: Component, apply: Component => Unit)
+  {
+    def traverse(comp: Component)
+    {
+      apply(comp)
+      comp match {
+        case cont: Container =>
+          for (i <- 0 until cont.getComponentCount)
+            traverse(cont.getComponent(i))
+        case _ =>
+      }
+    }
+    traverse(component)
+  }
+
 
   /* font operations */
 
   def copy_font(font: Font): Font =
     if (font == null) null