diff -r 7593c0976dc6 -r 4210fd10e776 src/Pure/Tools/doc.scala --- a/src/Pure/Tools/doc.scala Thu Dec 26 15:18:19 2024 +0100 +++ b/src/Pure/Tools/doc.scala Thu Dec 26 15:24:21 2024 +0100 @@ -18,7 +18,8 @@ def view(): Unit = Doc.view(path) override def toString: String = // GUI label if (title.nonEmpty) { - "" + HTML.output(name) + ": " + HTML.output(title) + "" + val style = GUI.Style_HTML + style.enclose(style.make_bold(name) + style.make_text(": " + title)) } else name }