src/Pure/Tools/doc.scala
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
   }