# HG changeset patch
# User wenzelm
# Date 1761414742 -7200
# Node ID 65d22b27471af3a548a58e84be3d2c9fb1c9efdb
# Parent  5294055465d37281fee2a665bce720306ef5ee82
tuned signature: more operations;

diff -r 5294055465d3 -r 65d22b27471a src/Pure/Tools/doc.scala
--- a/src/Pure/Tools/doc.scala	Sat Oct 25 19:20:37 2025 +0200
+++ b/src/Pure/Tools/doc.scala	Sat Oct 25 19:52:22 2025 +0200
@@ -18,12 +18,15 @@
   }
   case class Entry(name: String, path: Path, title: String = "") {
     def view(): Unit = Doc.view(path)
-    override def toString: String =  // GUI label
-      if (title.nonEmpty) {
-        val style = GUI.Style_HTML
-        style.enclose(style.make_bold(name) + style.make_text(": " + title))
-      }
-      else name
+
+    def print_html: String = {
+      val style = GUI.Style_HTML
+      if (title.nonEmpty) style.make_bold(name) + style.make_text(": " + title)
+      else style.make_text(name)
+    }
+
+    override def toString: String =  // Swing GUI label
+      if (title.nonEmpty) GUI.Style_HTML.enclose(print_html) else name
   }
 
   def plain_file(path0: Path,