diff -r 137559b26f74 -r a519b9d1e1c1 src/Pure/GUI/gui.scala --- a/src/Pure/GUI/gui.scala Sat Feb 15 15:06:38 2025 +0100 +++ b/src/Pure/GUI/gui.scala Sat Feb 15 16:12:29 2025 +0100 @@ -147,7 +147,7 @@ val b = name.nonEmpty style.make_text(prefix) + if_proper(a || b, - if_proper(prefix, ": ") + if_proper(kind, style.make_bold(kind)) + + if_proper(prefix, ": ") + if_proper(kind, style.make_text(kind)) + if_proper(a && b, " ") + if_proper(b, style.make_text(quote(name)))) } }