# HG changeset patch
# User wenzelm
# Date 1661606638 -7200
# Node ID b831a0bdd7513ea762fd72a094b687fe208c8b69
# Parent  c36e5c6f306966e146732887f9a2990792d87208
clarified signature of Sessions.Session: chapter_defs: vs. known_chapters (in declaration order) vs. chapters (covered by visible sessions);
clarified browser_info root index: preserve declaration order as much as possible;

diff -r c36e5c6f3069 -r b831a0bdd751 src/Pure/Thy/browser_info.scala
--- a/src/Pure/Thy/browser_info.scala	Sat Aug 27 12:18:49 2022 +0200
+++ b/src/Pure/Thy/browser_info.scala	Sat Aug 27 15:23:58 2022 +0200
@@ -139,12 +139,8 @@
     sealed case class Index(kind: String, items: List[Item]) {
       def is_empty: Boolean = items.isEmpty
 
-      def ++ (more_items: List[Item]): Index = {
-        val items1 = items.filterNot(item => more_items.exists(_.name == item.name))
-        val items2 = (more_items ::: items1).sortBy(_.name)
-        Index(kind, items2)
-      }
-      def + (item: Item): Index = this ++ List(item)
+      def + (item: Item): Index =
+        Index(kind, (item :: items.filterNot(_.name == item.name)).sortBy(_.name))
 
       def json: JSON.T = JSON.Object("kind" -> kind, "items" -> items.map(_.json))
       def print_json: JSON.S = JSON.Format.pretty_print(json)
@@ -323,14 +319,10 @@
         val index0 = Meta_Data.Index.parse(text, "root")
         val index = {
           val items1 =
-            for (entry <- sessions_structure.chapter_defs.list)
-              yield Meta_Data.Item(entry.name, description = entry.description)
-          val items2 =
-            (for {
-              (name, _) <- sessions_structure.chapters.iterator
-              if !items1.exists(_.name == name)
-            } yield Meta_Data.Item(name)).toList
-          index0 ++ (items1 ::: items2)
+            sessions_structure.known_chapters
+              .map(ch => Meta_Data.Item(ch.name, description = ch.description))
+          val items2 = index0.items.filterNot(item => items1.exists(_.name == item.name))
+          index0.copy(items = items1 ::: items2)
         }
 
         if (index != index0) {
diff -r c36e5c6f3069 -r b831a0bdd751 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Aug 27 12:18:49 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat Aug 27 15:23:58 2022 +0200
@@ -457,6 +457,13 @@
 
   /* cumulative session info */
 
+  sealed case class Chapter_Info(
+    name: String,
+    pos: Position.T,
+    description: String,
+    sessions: List[String]
+  )
+
   sealed case class Info(
     name: String,
     chapter: String,
@@ -722,7 +729,7 @@
   }
 
   final class Structure private[Sessions](
-    val chapter_defs: Chapter_Defs,
+    chapter_defs: Chapter_Defs,
     val session_positions: List[(String, Position.T)],
     val session_directories: Map[JFile, String],
     val global_theories: Map[String, String],
@@ -737,11 +744,25 @@
       for ((file, session) <- session_directories.toList)
         yield (File.standard_path(file), session)
 
-    lazy val chapters: SortedMap[String, List[Info]] =
-      build_graph.iterator.foldLeft(SortedMap.empty[String, List[Info]]) {
-        case (chs, (_, (info, _))) =>
-          chs + (info.chapter -> (info :: chs.getOrElse(info.chapter, Nil)))
-      }
+    lazy val known_chapters: List[Chapter_Info] = {
+      val chapter_sessions =
+        Multi_Map.from(
+          for ((_, (info, _)) <- build_graph.iterator)
+            yield info.chapter -> info.name)
+      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)
+        }).toList
+      val chapters2 =
+        (for {
+          (name, sessions) <- chapter_sessions.iterator_list
+          if !chapters1.exists(_.name == name)
+        } yield Chapter_Info(name, Position.none, "", sessions.sorted)).toList
+      chapters1 ::: chapters2
+    }
+
+    def chapters: List[Chapter_Info] = known_chapters.filter(_.sessions.nonEmpty)
 
     def build_graph_display: Graph_Display.Graph = Graph_Display.make_graph(build_graph)
     def imports_graph_display: Graph_Display.Graph = Graph_Display.make_graph(imports_graph)
diff -r c36e5c6f3069 -r b831a0bdd751 src/Tools/jEdit/src/isabelle_session.scala
--- a/src/Tools/jEdit/src/isabelle_session.scala	Sat Aug 27 12:18:49 2022 +0200
+++ b/src/Tools/jEdit/src/isabelle_session.scala	Sat Aug 27 15:23:58 2022 +0200
@@ -50,25 +50,26 @@
           val sessions = JEdit_Sessions.sessions_structure()
           elems match {
             case Nil =>
-              sessions.chapters.iterator.map(p => make_entry(p._1, is_dir = true)).toArray
+              sessions.chapters.sortBy(_.name).map(ch => make_entry(ch.name, is_dir = true)).toArray
             case List(chapter) =>
-              sessions.chapters.get(chapter) match {
+              sessions.chapters.find(_.name == chapter) match {
                 case None => null
-                case Some(infos) =>
-                  infos.map(info => {
-                    val name = chapter + "/" + info.name
+                case Some(chapter_info) =>
+                  chapter_info.sessions.map { session =>
+                    val pos = sessions(session).pos
+                    val name = chapter_info.name + "/" + session
                     val path =
-                      Position.File.unapply(info.pos) match {
+                      Position.File.unapply(pos) match {
                         case Some(path) => File.platform_path(path)
                         case None => null
                       }
                     val marker =
-                      Position.Line.unapply(info.pos) match {
+                      Position.Line.unapply(pos) match {
                         case Some(line) => "+line:" + line
                         case None => null
                       }
                     new Session_Entry(name, path, marker)
-                  }).toArray
+                  }.toArray
               }
             case _ => null
           }