changeset 81657 | 4210fd10e776 |
parent 81656 | 7593c0976dc6 |
child 82720 | 956ecf2c07a0 |
--- 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><b>" + HTML.output(name) + "</b>: " + HTML.output(title) + "</html>" + val style = GUI.Style_HTML + style.enclose(style.make_bold(name) + style.make_text(": " + title)) } else name }