# HG changeset patch
# User wenzelm
# Date 1661615218 -7200
# Node ID a9bbf075f4319e920a22a1c0a5b763b6575f2089
# Parent  152c5c83c119cd89373a68994e6a5486581b3b1a
include groups from 'chapter_definition' in session info, based on the state of chapter_defs after processing all ROOT files (thus the declaration order does not matter);

diff -r 152c5c83c119 -r a9bbf075f431 NEWS
--- a/NEWS	Sat Aug 27 17:11:39 2022 +0200
+++ b/NEWS	Sat Aug 27 17:46:58 2022 +0200
@@ -12,8 +12,14 @@
 * Old-style {* verbatim *} tokens have been discontinued (legacy feature
 since Isabelle2019). INCOMPATIBILITY, use \<open>cartouche\<close> syntax instead.
 
-* Session ROOT files support 'chapter_definition', in order to associate
-a description for presentation purposes.
+* Session ROOT files support 'chapter_definition' entries (optional).
+This allows to associate additional information as follows:
+
+  - "chapter_definition NAME (GROUPS)" to make all sessions that belong
+  to this chapter members of the given groups
+
+  - "chapter_definition NAME description TEXT" to provide a description
+  for presentation purposes
 
 
 *** Isabelle/VSCode Prover IDE ***
diff -r 152c5c83c119 -r a9bbf075f431 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Sat Aug 27 17:11:39 2022 +0200
+++ b/src/Doc/System/Sessions.thy	Sat Aug 27 17:46:58 2022 +0200
@@ -42,15 +42,16 @@
   and @{syntax session_entry} is given as syntax diagram below. Each ROOT file
   may contain multiple specifications like this. Chapters help to organize
   browser info (\secref{sec:info}), but have no formal meaning. The default
-  chapter is ``\<open>Unsorted\<close>''. Chapter definitions are optional: the main
-  purpose is to associate a description for presentation.
+  chapter is ``\<open>Unsorted\<close>''. Chapter definitions, which are optional, allow to
+  associate additional information.
 
   Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple editing mode
   \<^verbatim>\<open>isabelle-root\<close> for session ROOT files, which is enabled by default for any
   file of that name.
 
   \<^rail>\<open>
-    @{syntax_def chapter_def}: @'chapter_definition' @{syntax name} description?
+    @{syntax_def chapter_def}: @'chapter_definition' @{syntax name} \<newline>
+      groups? description?
     ;
 
     @{syntax_def chapter_entry}: @'chapter' @{syntax name}
@@ -90,6 +91,10 @@
       (@{syntax embedded}+)
   \<close>
 
+  \<^descr> \isakeyword{chapter{\isacharunderscorekeyword}definition}~\<open>A (groups)\<close>
+  associates a collection of groups with chapter \<open>A\<close>. All sessions that belong
+  to this chapter will automatically become members of these groups.
+
   \<^descr> \isakeyword{session}~\<open>A = B + body\<close> defines a new session \<open>A\<close> based on
   parent session \<open>B\<close>, with its content given in \<open>body\<close> (imported sessions and
   theories). Note that a parent (like \<open>HOL\<close>) is mandatory in practical
@@ -114,8 +119,8 @@
   All theory files are located relatively to the session directory. The prover
   process is run within the same as its current working directory.
 
-  \<^descr> \isakeyword{description}~\<open>text\<close> is a free-form annotation for this
-  session.
+  \<^descr> \isakeyword{description}~\<open>text\<close> is a free-form description for this
+  session (or chapter), e.g. for presentation purposes.
 
   \<^descr> \isakeyword{options}~\<open>[x = a, y = b, z]\<close> defines separate options
   (\secref{sec:system-options}) that are used when processing this session,
diff -r 152c5c83c119 -r a9bbf075f431 src/Pure/Thy/sessions.ML
--- a/src/Pure/Thy/sessions.ML	Sat Aug 27 17:11:39 2022 +0200
+++ b/src/Pure/Thy/sessions.ML	Sat Aug 27 17:46:58 2022 +0200
@@ -20,6 +20,9 @@
 
 local
 
+val groups =
+  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.name --| Parse.$$$ ")")) [];
+
 val description =
   Scan.optional (Parse.$$$ "description" |-- Parse.!!! (Parse.input Parse.embedded)) Input.empty;
 
@@ -54,7 +57,7 @@
 in
 
 val chapter_definition_parser =
-  Parse.chapter_name -- description >> (fn (_, descr) =>
+  Parse.chapter_name -- groups -- description >> (fn (_, descr) =>
     Toplevel.keep (fn state =>
       let
         val ctxt = Toplevel.context_of state;
@@ -65,8 +68,7 @@
       in () end));
 
 val session_parser =
-  Parse.session_name --
-  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.name --| Parse.$$$ ")")) [] --
+  Parse.session_name -- groups --
   Scan.optional (Parse.$$$ "in" |-- Parse.!!! Parse.path_input) (Input.string ".") --
   (Parse.$$$ "=" |--
     Parse.!!! (Scan.option (Parse.session_name --| Parse.!!! (Parse.$$$ "+")) -- description --
diff -r 152c5c83c119 -r a9bbf075f431 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Aug 27 17:11:39 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat Aug 27 17:46:58 2022 +0200
@@ -418,7 +418,9 @@
 
           (other_name,
             List(
-              make_info(info.options,
+              make_info(
+                Chapter_Defs.empty,
+                info.options,
                 dir_selected = false,
                 dir = Path.explode("$ISABELLE_TMP_PREFIX"),
                 chapter = info.chapter,
@@ -460,6 +462,7 @@
   sealed case class Chapter_Info(
     name: String,
     pos: Position.T,
+    groups: List[String],
     description: String,
     sessions: List[String]
   )
@@ -554,6 +557,7 @@
   }
 
   def make_info(
+    chapter_defs: Chapter_Defs,
     options: Options,
     dir_selected: Boolean,
     dir: Path,
@@ -609,7 +613,10 @@
             entry.document_files)
           .toString)
 
-      Info(name, chapter, dir_selected, entry.pos, entry.groups, session_path,
+      val chapter_groups = chapter_defs(chapter).groups
+      val groups = chapter_groups ::: entry.groups.filterNot(chapter_groups.contains)
+
+      Info(name, chapter, dir_selected, entry.pos, groups, session_path,
         entry.parent, entry.description, directories, session_options,
         entry.imports, theories, global_theories, entry.document_theories, document_files,
         export_files, entry.export_classpath, meta_digest)
@@ -752,13 +759,13 @@
       val chapters1 =
         (for (entry <- chapter_defs.list.iterator) yield {
           val sessions = chapter_sessions.get_list(entry.name)
-          Chapter_Info(entry.name, entry.pos, entry.description, sessions.sorted)
+          Chapter_Info(entry.name, entry.pos, entry.groups, entry.description, sessions.sorted)
         }).toList
       val chapters2 =
         (for {
           (name, sessions) <- chapter_sessions.iterator_list
           if !chapters1.exists(_.name == name)
-        } yield Chapter_Info(name, Position.none, "", sessions.sorted)).toList.sortBy(_.name)
+        } yield Chapter_Info(name, Position.none, Nil, "", sessions.sorted)).toList.sortBy(_.name)
       chapters1 ::: chapters2
     }
 
@@ -906,7 +913,15 @@
       (EXPORT_CLASSPATH, Keyword.QUASI_COMMAND)
 
   abstract class Entry
-  sealed case class Chapter_Def(pos: Position.T, name: String, description: String) extends Entry
+  object Chapter_Def {
+    def empty(chapter: String): Chapter_Def = Chapter_Def(Position.none, chapter, Nil, "")
+  }
+  sealed case class Chapter_Def(
+    pos: Position.T,
+    name: String,
+    groups: List[String],
+    description: String
+  ) extends Entry
   sealed case class Chapter_Entry(name: String) extends Entry
   sealed case class Session_Entry(
     pos: Position.T,
@@ -943,6 +958,9 @@
     def get(chapter: String): Option[Chapter_Def] =
       rev_list.find(_.name == chapter)
 
+    def apply(chapter: String): Chapter_Def =
+      get(chapter) getOrElse Chapter_Def.empty(chapter)
+
     def + (entry: Chapter_Def): Chapter_Defs =
       get(entry.name) match {
         case None => new Chapter_Defs(entry :: rev_list)
@@ -953,12 +971,15 @@
   }
 
   private object Parsers extends Options.Parsers {
+    private val groups: Parser[List[String]] =
+      ($$$("(") ~! (rep1(name) <~ $$$(")")) ^^ { case _ ~ x => x }) | success(Nil)
+
     private val description: Parser[String] =
       ($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")
 
     private val chapter_def: Parser[Chapter_Def] =
-      command(CHAPTER_DEFINITION) ~! (position(chapter_name) ~ description) ^^
-        { case _ ~ ((a, pos) ~ b) => Chapter_Def(pos, a, b) }
+      command(CHAPTER_DEFINITION) ~! (position(chapter_name) ~ groups ~ description) ^^
+        { case _ ~ ((a, pos) ~ b ~ c) => Chapter_Def(pos, a, b, c) }
 
     private val chapter_entry: Parser[Chapter_Entry] =
       command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter_Entry(a) }
@@ -997,8 +1018,7 @@
           { case _ ~ x => x }
 
       command(SESSION) ~!
-        (position(session_name) ~
-          (($$$("(") ~! (rep1(name) <~ $$$(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
+        (position(session_name) ~ groups ~
           (($$$(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~
           ($$$("=") ~!
             (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~ description ~
@@ -1103,7 +1123,7 @@
 
     val (chapter_defs, info_roots) = {
       var chapter_defs = Chapter_Defs.empty
-      val info_roots = new mutable.ListBuffer[Info]
+      val mk_infos = new mutable.ListBuffer[() => Info]
 
       for ((select, path) <- unique_roots) {
         var entry_chapter = UNSORTED
@@ -1111,10 +1131,11 @@
           case entry: Chapter_Def => chapter_defs += entry
           case entry: Chapter_Entry => entry_chapter = entry.name
           case entry: Session_Entry =>
-            info_roots += make_info(options, select, path.dir, entry_chapter, entry)
+            def mk(): Info = make_info(chapter_defs, options, select, path.dir, entry_chapter, entry)
+            mk_infos += mk
         }
       }
-      (chapter_defs, info_roots.toList)
+      (chapter_defs, mk_infos.toList.map(_()))
     }
 
     Structure.make(chapter_defs, info_roots ::: infos)