# HG changeset patch # User wenzelm # Date 1735215748 -3600 # Node ID f13d04506126851a75f081b16c9bf6e69363b895 # Parent 18c16b94164a0bd6eaa4d4dd3d840667dd2a8c21 more robust: proper HTML.output; diff -r 18c16b94164a -r f13d04506126 src/Pure/GUI/gui.scala --- 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))) } }