more robust: proper HTML.output;

--- a/src/Pure/GUI/gui.scala	Thu Dec 26 12:46:45 2024 +0100
+++ b/src/Pure/GUI/gui.scala	Thu Dec 26 13:22:28 2024 +0100
@@ -71,6 +71,9 @@
 
   enum Style { case plain, html, symbol_encoded, symbol_decoded }
 
+  def make_text(str: String, style: Style = Style.plain): String =
+    if (style == Style.html) HTML.output(str) else str
+
   def make_bold(str: String, style: Style = Style.plain): String =
     style match {
       case Style.plain => str
@@ -91,9 +94,10 @@
     override def toString: String = {
       val a = kind.nonEmpty
       val b = name.nonEmpty
-      val k = if_proper(kind, make_bold(kind, style = style))
-      prefix + if_proper(a || b,
-        if_proper(prefix, ": ") + k + if_proper(a && b, " ") + if_proper(b, quote(name)))
+      make_text(prefix, style = style) +
+        if_proper(a || b,
+          if_proper(prefix, ": ") + if_proper(kind, make_bold(kind, style = style)) +
+          if_proper(a && b, " ") + if_proper(b, make_text(quote(name), style = style)))
     }
   }