# HG changeset patch
# User wenzelm
# Date 1645471890 -3600
# Node ID 6fd8e482c9ce77a31ed7e6b33ed6abc4ffc35b0d
# Parent  4b3ae1a3bbbded6fb02da5e56d7a9480e942e394
clarified signature;

diff -r 4b3ae1a3bbbd -r 6fd8e482c9ce src/Pure/Tools/doc.scala
--- a/src/Pure/Tools/doc.scala	Mon Feb 21 16:50:21 2022 +0100
+++ b/src/Pure/Tools/doc.scala	Mon Feb 21 20:31:30 2022 +0100
@@ -28,8 +28,26 @@
       line <- Library.trim_split_lines(File.read(catalog))
     } yield (dir, line)
 
+  object Contents
+  {
+    def apply(sections: List[Section]): Contents = new Contents(sections)
+
+    def section(title: String, important: Boolean, entries: List[Entry]): Contents =
+      apply(List(Section(title, important, entries)))
+  }
+  class Contents private(val sections: List[Section])
+  {
+    def ++ (other: Contents): Contents = new Contents(sections ::: other.sections)
+    def entries: List[Entry] = sections.flatMap(_.entries)
+    def docs: List[Doc] = entries.collect({ case doc: Doc => doc })
+  }
+
   case class Section(title: String, important: Boolean, entries: List[Entry])
   sealed abstract class Entry
+  {
+    def name: String
+    def path: Path
+  }
   case class Doc(name: String, title: String, path: Path) extends Entry
   case class Text_File(name: String, path: Path) extends Entry
 
@@ -41,19 +59,19 @@
     }
     else None
 
-  def release_notes(): Section =
-    Section("Release Notes", true,
+  def release_notes(): Contents =
+    Contents.section("Release Notes", true,
       Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_RELEASE_NOTES")).flatMap(text_file))
 
-  def examples(): Section =
-    Section("Examples", true,
+  def examples(): Contents =
+    Contents.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] =
+  def main_contents(): Contents =
   {
     val result = new mutable.ListBuffer[Section]
     val entries = new mutable.ListBuffer[Entry]
@@ -89,23 +107,20 @@
     }
 
     flush()
-    result.toList
+    Contents(result.toList)
   }
 
-  def contents(): List[Section] =
+  def contents(): Contents =
   {
-    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 <- doc_entries(contents())) yield doc.name).sorted)
+      else cat_lines((for (doc <- contents().docs) yield doc.name).sorted)
   }
 
 
@@ -134,11 +149,10 @@
 """)
     val docs = getopts(args)
 
-    val sections = contents()
     if (docs.isEmpty) Output.writeln(cat_lines(contents_lines().map(_._2)), stdout = true)
     else {
       docs.foreach(name =>
-        doc_entries(sections).find(_.name == name) match {
+        contents().docs.find(_.name == name) match {
           case Some(doc) => view(doc.path)
           case None => error("No Isabelle documentation entry: " + quote(name))
         }
diff -r 4b3ae1a3bbbd -r 6fd8e482c9ce src/Tools/jEdit/src/documentation_dockable.scala
--- a/src/Tools/jEdit/src/documentation_dockable.scala	Mon Feb 21 16:50:21 2022 +0100
+++ b/src/Tools/jEdit/src/documentation_dockable.scala	Mon Feb 21 20:31:30 2022 +0100
@@ -19,7 +19,7 @@
 
 class Documentation_Dockable(view: View, position: String) extends Dockable(view, position)
 {
-  private val sections = Doc.contents()
+  private val doc_contents = Doc.contents()
 
   private case class Documentation(name: String, title: String, path: Path)
   {
@@ -33,7 +33,7 @@
   }
 
   private val root = new DefaultMutableTreeNode
-  for (section <- sections) {
+  for (section <- doc_contents.sections) {
     root.add(new DefaultMutableTreeNode(section.title))
     section.entries.foreach(
       {
@@ -97,7 +97,7 @@
     var visible = 0
     var row = 0
     def make_visible(): Unit = { visible += 1; tree.expandRow(row) }
-    for (section <- sections) {
+    for (section <- doc_contents.sections) {
       expand = section.important
       make_visible()
       row += 1
diff -r 4b3ae1a3bbbd -r 6fd8e482c9ce src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Feb 21 16:50:21 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Feb 21 20:31:30 2022 +0100
@@ -198,14 +198,14 @@
   /* hyperlinks */
 
   def hyperlink_doc(name: String): Option[Hyperlink] =
-    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 {
-          override val external: Boolean = !path.is_file
-          def follow(view: View): Unit = goto_doc(view, path)
-          override def toString: String = "doc " + quote(name)
-        })
+    Doc.contents().entries.collectFirst(
+      { case entry if entry.name == name =>
+          new Hyperlink {
+            override val external: Boolean = !entry.path.is_file
+            def follow(view: View): Unit = goto_doc(view, entry.path)
+            override def toString: String = "doc " + quote(name)
+          }
+      })
 
   def hyperlink_url(name: String): Hyperlink =
     new Hyperlink {