src/Pure/GUI/gui.scala

--- a/src/Pure/GUI/gui.scala	Mon Dec 23 14:09:43 2024 +0100
+++ b/src/Pure/GUI/gui.scala	Tue Dec 24 14:59:56 2024 +0100
@@ -67,6 +67,18 @@
   }
 
 
+  /* 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 */
 
   def scrollable_text(