src/Pure/Tools/doc.scala

--- a/src/Pure/Tools/doc.scala	Sat Oct 25 17:13:50 2025 +0200
+++ b/src/Pure/Tools/doc.scala	Sat Oct 25 17:27:33 2025 +0200
@@ -13,7 +13,9 @@
 object Doc {
   /* entries */
 
-  case class Section(title: String, important: Boolean, entries: List[Entry])
+  case class Section(title: String, important: Boolean, entries: List[Entry]) {
+    def print_title: String = title + if_proper(important, "!")
+  }
   case class Entry(name: String, path: Path, title: String = "") {
     def view(): Unit = Doc.view(path)
     override def toString: String =  // GUI label
@@ -57,6 +59,9 @@
       apply(List(Section(title, important, entries)))
   }
   class Contents private(val sections: List[Section]) {
+    override def toString: String =
+      sections.map(_.print_title).mkString("Doc.Contents(", ", ", ")")
+
     def ++ (other: Contents): Contents = new Contents(sections ::: other.sections)
     def entries(name: String => Boolean = _ => true, pdf: Boolean = false): List[Entry] =
       sections.flatMap(s => s.entries.filter(e => name(e.name) && (!pdf || e.path.is_pdf)))