src/Pure/Thy/sessions.scala

--- a/src/Pure/Thy/sessions.scala	Fri Aug 26 21:25:35 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Aug 26 21:28:26 2022 +0200
@@ -641,9 +641,9 @@
   }
 
   object Structure {
-    val empty: Structure = make(Nil)
+    val empty: Structure = make(Chapter_Defs.empty, Nil)
 
-    def make(infos: List[Info]): Structure = {
+    def make(chapter_defs: Chapter_Defs, infos: List[Info]): Structure = {
       def add_edges(
         graph: Graph[String, Info],
         kind: String,
@@ -716,12 +716,13 @@
               }
           }
 
-      new Structure(
-        session_positions, session_directories, global_theories, build_graph, imports_graph)
+      new Structure(chapter_defs, session_positions, session_directories,
+        global_theories, build_graph, imports_graph)
     }
   }
 
   final class Structure private[Sessions](
+    val chapter_defs: Chapter_Defs,
     val session_positions: List[(String, Position.T)],
     val session_directories: Map[JFile, String],
     val global_theories: Map[String, String],
@@ -799,8 +800,7 @@
         graph.restrict(graph.all_preds(sessions).toSet)
       }
 
-      new Structure(
-        session_positions, session_directories, global_theories,
+      new Structure(chapter_defs, session_positions, session_directories, global_theories,
         restrict(build_graph), restrict(imports_graph))
     }
 
@@ -853,6 +853,7 @@
 
   /* parser */
 
+  private val CHAPTER_DEFINITION = "chapter_definition"
   private val CHAPTER = "chapter"
   private val SESSION = "session"
   private val IN = "in"
@@ -870,6 +871,7 @@
   val root_syntax: Outer_Syntax =
     Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" +
       GLOBAL + IN +
+      (CHAPTER_DEFINITION, Keyword.THY_DECL) +
       (CHAPTER, Keyword.THY_DECL) +
       (SESSION, Keyword.THY_DECL) +
       (DESCRIPTION, Keyword.QUASI_COMMAND) +
@@ -883,6 +885,7 @@
       (EXPORT_CLASSPATH, Keyword.QUASI_COMMAND)
 
   abstract class Entry
+  sealed case class Chapter_Def(pos: Position.T, name: String, description: String) extends Entry
   sealed case class Chapter_Entry(name: String) extends Entry
   sealed case class Session_Entry(
     pos: Position.T,
@@ -906,12 +909,48 @@
       document_theories.map(_._1)
   }
 
+  object Chapter_Defs {
+    val empty: Chapter_Defs = new Chapter_Defs(Nil)
+  }
+
+  class Chapter_Defs private(rev_list: List[Chapter_Def]) {
+    def list: List[Chapter_Def] = rev_list.reverse
+
+    override def toString: String =
+      list.map(_.name).mkString("Chapter_Defs(", ", ", ")")
+
+    private def find(chapter: String): Option[Chapter_Def] =
+      rev_list.find(_.name == chapter)
+
+    def apply(chapter: String): String =
+      find(chapter) match {
+        case None => ""
+        case Some(ch_def) => ch_def.description
+      }
+
+    def + (ch_def: Chapter_Def): Chapter_Defs =
+      if (ch_def.description.isEmpty) this
+      else {
+        find(ch_def.name) match {
+          case None => new Chapter_Defs(ch_def :: rev_list)
+          case Some(old_def) =>
+            error("Duplicate chapter definition " + quote(ch_def.name) +
+              Position.here(old_def.pos) + Position.here(ch_def.pos))
+        }
+      }
+  }
+
   private object Parsers extends Options.Parsers {
-    private val chapter: Parser[Chapter_Entry] = {
-      val chapter_name = atom("chapter name", _.is_name)
+    private val chapter_name: Parser[String] =
+      atom("chapter name", _.is_name)
 
+    private val chapter_def: Parser[Chapter_Def] =
+      command(CHAPTER_DEFINITION) ~!
+        (position(chapter_name) ~ $$$(DESCRIPTION) ~ text) ^^
+        { case _ ~ ((a, pos) ~ _ ~ b) => Chapter_Def(pos, a, b) }
+
+    private val chapter_entry: Parser[Chapter_Entry] =
       command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter_Entry(a) }
-    }
 
     private val session_entry: Parser[Session_Entry] = {
       val option =
@@ -968,8 +1007,8 @@
     def parse_root(path: Path): List[Entry] = {
       val toks = Token.explode(root_syntax.keywords, File.read(path))
       val start = Token.Pos.file(path.implode)
-
-      parse_all(rep(chapter | session_entry), Token.reader(toks, start)) match {
+      val parser: Parser[Entry] = chapter_def | chapter_entry | session_entry
+      parse_all(rep(parser), Token.reader(toks, start)) match {
         case Success(result, _) => result
         case bad => error(bad.toString)
       }
@@ -982,15 +1021,22 @@
     for (entry <- Parsers.parse_root(path) if entry.isInstanceOf[Session_Entry])
     yield entry.asInstanceOf[Session_Entry]
 
-  def read_root(options: Options, select: Boolean, path: Path): List[Info] = {
+  def read_root(
+    options: Options,
+    select: Boolean,
+    path: Path,
+    chapter_defs: Chapter_Defs
+  ): (List[Info], Chapter_Defs) = {
+    var chapter_defs1 = chapter_defs
     var entry_chapter = UNSORTED
     val infos = new mutable.ListBuffer[Info]
     parse_root(path).foreach {
-      case Chapter_Entry(name) => entry_chapter = name
+      case ch_def: Chapter_Def => chapter_defs1 += ch_def
+      case entry: Chapter_Entry => entry_chapter = entry.name
       case entry: Session_Entry =>
         infos += make_info(options, select, path.dir, entry_chapter, entry)
     }
-    infos.toList
+    (infos.toList, chapter_defs1)
   }
 
   def parse_roots(roots: Path): List[String] = {
@@ -1063,7 +1109,18 @@
           }
       }.toList.map(_._2)
 
-    Structure.make(unique_roots.flatMap(p => read_root(options, p._1, p._2)) ::: infos)
+    val (chapter_defs, info_roots) = {
+      var chapter_defs = Chapter_Defs.empty
+      val result = new mutable.ListBuffer[Info]
+      for { (select, path) <- unique_roots } {
+        val (infos, chapter_defs1) = read_root(options, select, path, chapter_defs)
+        chapter_defs = chapter_defs1
+        result ++= infos
+      }
+      (chapter_defs, result.toList)
+    }
+
+    Structure.make(chapter_defs, info_roots ::: infos)
   }