src/Pure/Tools/doc.scala

 
 
 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
       if (title.nonEmpty) {
         val style = GUI.Style_HTML

 
     def section(title: String, important: Boolean, entries: List[Entry]): Contents =
       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)))
   }