src/Pure/GUI/gui.scala

     val dummy_button = new JButton
     def apply(id: Int): Unit =
       component.setFocusTraversalKeys(id, dummy_button.getFocusTraversalKeys(id))
     apply(KeyboardFocusManager.FORWARD_TRAVERSAL_KEYS)
     apply(KeyboardFocusManager.BACKWARD_TRAVERSAL_KEYS)
+  }
+
+
+  /* named items */
+
+  sealed case class Name(name: String, kind: String = "", prefix: String = "") {
+    override def toString: String = {
+      val a = kind.nonEmpty
+      val b = name.nonEmpty
+      prefix + if_proper(a || b,
+        if_proper(prefix, ": ") + kind + if_proper(a && b, " ") + if_proper(b, quote(name)))
+    }
   }
 
 
   /* simple dialogs */