clarified signature: more explicit section structure;

--- a/src/Pure/Tools/doc.scala	Mon Feb 21 15:33:04 2022 +0100
+++ b/src/Pure/Tools/doc.scala	Mon Feb 21 16:23:11 2022 +0100
@@ -7,6 +7,9 @@
 package isabelle
 
 
+import scala.collection.mutable
+
+
 object Doc
 {
   /* dirs */
@@ -25,8 +28,8 @@
       line <- Library.trim_split_lines(File.read(catalog))
     } yield (dir, line)
 
+  case class Section(title: String, important: Boolean, entries: List[Entry])
   sealed abstract class Entry
-  case class Heading(title: String, important: Boolean) extends Entry
   case class Doc(name: String, title: String, path: Path) extends Entry
   case class Text_File(name: String, path: Path) extends Entry
 
@@ -38,47 +41,71 @@
     }
     else None
 
-  private val Section_Entry = """^(\S.*)\s*$""".r
-  private val Doc_Entry = """^\s+(\S+)\s+(.+)\s*$""".r
+  def release_notes(): Section =
+    Section("Release Notes", true,
+      Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_RELEASE_NOTES")).flatMap(text_file))
 
-  private def release_notes(): List[Entry] =
-    Heading("Release Notes", true) ::
-      Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_RELEASE_NOTES")).flatMap(text_file)
-
-  private def examples(): List[Entry] =
-    Heading("Examples", true) ::
+  def examples(): Section =
+    Section("Examples", true,
       Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_EXAMPLES")).map(file =>
         text_file(file) match {
           case Some(entry) => entry
           case None => error("Bad entry in ISABELLE_DOCS_EXAMPLES: " + file)
-        })
+        }))
+
+  def main_contents(): List[Section] =
+  {
+    val result = new mutable.ListBuffer[Section]
+    val entries = new mutable.ListBuffer[Entry]
+    var section: Option[Section] = None
+
+    def flush(): Unit =
+      if (section.nonEmpty) {
+        result += section.get.copy(entries = entries.toList)
+        entries.clear()
+        section = None
+      }
+
+    def begin(s: Section): Unit =
+    {
+      flush()
+      section = Some(s)
+    }
+
+    val Section_ = """^(\S.*)\s*$""".r
+    val Doc_ = """^\s+(\S+)\s+(.+)\s*$""".r
 
-  def main_contents(): List[Entry] =
-    for {
-      (dir, line) <- contents_lines()
-      entry <-
-        line match {
-          case Section_Entry(text) =>
-            Library.try_unsuffix("!", text) match {
-              case None => Some(Heading(text, false))
-              case Some(txt) => Some(Heading(txt, true))
-            }
-          case Doc_Entry(name, title) => Some(Doc(name, title, dir + Path.basic(name)))
-          case _ => None
-        }
-    } yield entry
+    for ((dir, line) <- contents_lines()) {
+      line match {
+        case Section_(text) =>
+          Library.try_unsuffix("!", text) match {
+            case None => begin(Section(text, false, Nil))
+            case Some(txt) => begin(Section(txt, true, Nil))
+          }
+        case Doc_(name, title) =>
+          entries += Doc(name, title, dir + Path.basic(name))
+        case _ =>
+      }
+    }
 
-  def contents(): List[Entry] =
+    flush()
+    result.toList
+  }
+
+  def contents(): List[Section] =
   {
-    examples() ::: release_notes() ::: main_contents()
+    examples() :: release_notes() :: main_contents()
   }
 
+  def doc_entries(sections: List[Section]): List[Doc] =
+    sections.flatMap(_.entries).collect({ case doc: Doc => doc })
+
   object Doc_Names extends Scala.Fun_String("doc_names")
   {
     val here = Scala_Project.here
     def apply(arg: String): String =
       if (arg.nonEmpty) error("Bad argument: " + quote(arg))
-      else cat_lines((for (Doc(name, _, _) <- contents()) yield name).sorted)
+      else cat_lines((for (doc <- doc_entries(contents())) yield doc.name).sorted)
   }
 
 
@@ -107,13 +134,13 @@
 """)
     val docs = getopts(args)
 
-    val entries = contents()
+    val sections = contents()
     if (docs.isEmpty) Output.writeln(cat_lines(contents_lines().map(_._2)), stdout = true)
     else {
-      docs.foreach(doc =>
-        entries.collectFirst { case Doc(name, _, path) if doc == name => path } match {
-          case Some(path) => view(path)
-          case None => error("No Isabelle documentation entry: " + quote(doc))
+      docs.foreach(name =>
+        doc_entries(sections).find(_.name == name) match {
+          case Some(doc) => view(doc.path)
+          case None => error("No Isabelle documentation entry: " + quote(name))
         }
       )
     }

--- a/src/Tools/jEdit/src/documentation_dockable.scala	Mon Feb 21 15:33:04 2022 +0100
+++ b/src/Tools/jEdit/src/documentation_dockable.scala	Mon Feb 21 16:23:11 2022 +0100
@@ -19,7 +19,7 @@
 
 class Documentation_Dockable(view: View, position: String) extends Dockable(view, position)
 {
-  private val docs = Doc.contents()
+  private val sections = Doc.contents()
 
   private case class Documentation(name: String, title: String, path: Path)
   {
@@ -33,15 +33,17 @@
   }
 
   private val root = new DefaultMutableTreeNode
-  docs foreach {
-    case Doc.Heading(text, _) =>
-      root.add(new DefaultMutableTreeNode(text))
-    case Doc.Doc(name, title, path) =>
-      root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
-        .add(new DefaultMutableTreeNode(Documentation(name, title, path)))
-    case Doc.Text_File(name: String, path: Path) =>
-      root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
-        .add(new DefaultMutableTreeNode(Text_File(name, path.expand)))
+  for (section <- sections) {
+    root.add(new DefaultMutableTreeNode(section.title))
+    section.entries.foreach(
+      {
+        case Doc.Doc(name, title, path) =>
+          root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
+            .add(new DefaultMutableTreeNode(Documentation(name, title, path)))
+        case Doc.Text_File(name: String, path: Path) =>
+          root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
+            .add(new DefaultMutableTreeNode(Text_File(name, path.expand)))
+      })
   }
 
   private val tree = new JTree(root)
@@ -93,14 +95,15 @@
   {
     var expand = true
     var visible = 0
-    def make_visible(row: Int): Unit = { visible += 1; tree.expandRow(row) }
-    for ((entry, row) <- docs.zipWithIndex) {
-      entry match {
-        case Doc.Heading(_, important) =>
-          expand = important
-          make_visible(row)
-        case _ =>
-          if (expand) make_visible(row)
+    var row = 0
+    def make_visible(): Unit = { visible += 1; tree.expandRow(row) }
+    for (section <- sections) {
+      expand = section.important
+      make_visible()
+      row += 1
+      for (_ <- section.entries) {
+        if (expand) make_visible()
+        row += 1
       }
     }
     tree.setRootVisible(false)

--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Feb 21 15:33:04 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Feb 21 16:23:11 2022 +0100
@@ -198,7 +198,7 @@
   /* hyperlinks */
 
   def hyperlink_doc(name: String): Option[Hyperlink] =
-    Doc.contents().collectFirst({
+    Doc.contents().iterator.flatMap(_.entries.iterator).collectFirst({
       case doc: Doc.Text_File if doc.name == name => doc.path
       case doc: Doc.Doc if doc.name == name => doc.path}).map(path =>
         new Hyperlink {