src/Pure/GUI/gui.scala

--- a/src/Pure/GUI/gui.scala	Thu Dec 26 15:43:07 2024 +0100
+++ b/src/Pure/GUI/gui.scala	Thu Dec 26 16:16:28 2024 +0100
@@ -116,6 +116,8 @@
     prefix: String = "",
     style: Style = Style_Plain
   ) {
+    def set_style(new_style: Style): Name = copy(style = new_style)
+
     override def toString: String = {
       val a = kind.nonEmpty
       val b = name.nonEmpty