# HG changeset patch
# User wenzelm
# Date 1670870952 -3600
# Node ID f55c67f2889b11f01097f3223f4c6a6d1c7c345d
# Parent  46017d6b9bfa64776d8753a6183a5968cc43cd0b
clarified signature: more types and operations;

diff -r 46017d6b9bfa -r f55c67f2889b src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Dec 12 13:59:18 2022 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Dec 12 19:49:12 2022 +0100
@@ -1089,21 +1089,32 @@
     yield (select, dir.canonical)
   }
 
-  def load_structure(
-    options: Options,
+  sealed case class Root_File(path: Path, select: Boolean) {
+    val key: JFile = path.canonical_file
+    def dir: Path = path.dir
+
+    def || (that: Root_File): Root_File = {
+      require(key == that.key)
+      val select1 = select || that.select
+      if (select1 == select) this else copy(select = select1)
+    }
+
+    lazy val entries: List[Entry] = Parsers.parse_root(path)
+  }
+
+  def load_root_files(
     dirs: List[Path] = Nil,
-    select_dirs: List[Path] = Nil,
-    infos: List[Info] = Nil
-  ): Structure = {
-    def load_dir(select: Boolean, dir: Path): List[(Boolean, Path)] =
+    select_dirs: List[Path] = Nil
+  ): List[Root_File] = {
+    def load_dir(select: Boolean, dir: Path): List[Root_File] =
       load_root(select, dir) ::: load_roots(select, dir)
 
-    def load_root(select: Boolean, dir: Path): List[(Boolean, Path)] = {
+    def load_root(select: Boolean, dir: Path): List[Root_File] = {
       val root = dir + ROOT
-      if (root.is_file) List((select, root)) else Nil
+      if (root.is_file) List(Root_File(root, select)) else Nil
     }
 
-    def load_roots(select: Boolean, dir: Path): List[(Boolean, Path)] = {
+    def load_roots(select: Boolean, dir: Path): List[Root_File] = {
       val roots = dir + ROOTS
       if (roots.is_file) {
         for {
@@ -1120,42 +1131,48 @@
       else Nil
     }
 
-    val raw_roots: List[(Boolean, Path)] =
+    val raw_roots: List[Root_File] =
       for {
         (select, dir) <- directories(dirs, select_dirs)
-        res <- load_dir(select, check_session_dir(dir))
-      } yield res
+        root <- load_dir(select, check_session_dir(dir))
+      } yield root
 
-    val unique_roots: List[(Boolean, Path, List[Entry])] =
-      raw_roots.foldLeft(Map.empty[JFile, (Boolean, Path, List[Entry])]) {
-        case (m, (select, path)) =>
-          val file = path.canonical_file
-          m.get(file) match {
-            case None =>
-              val entries = parse_root(path)
-              m + (file -> (select, path.dir, entries))
-            case Some((select1, dir1, entries1)) =>
-              m + (file -> (select1 || select, dir1, entries1))
-          }
-      }.valuesIterator.toList
+    var next_root = 0
+    var seen_roots = Map.empty[JFile, (Root_File, Int)]
+    for (root <- raw_roots) {
+      seen_roots.get(root.key) match {
+        case None =>
+          seen_roots += (root.key -> (root, next_root))
+          next_root += 1
+        case Some((root1, next1)) =>
+          seen_roots += (root.key -> (root || root1, next1))
+      }
+    }
+    seen_roots.valuesIterator.toList.sortBy(_._2).map(_._1)
+  }
 
+  def make_structure(
+    options: Options,
+    roots: List[Root_File] = Nil,
+    infos: List[Info] = Nil
+  ): Structure = {
     val chapter_defs: Chapter_Defs =
-      unique_roots.foldLeft(Chapter_Defs.empty) {
-        case (defs1, (_, _, entries)) =>
-          entries.foldLeft(defs1) {
-            case ((defs2, entry: Chapter_Def)) => defs2 + entry
-            case ((defs2, _)) => defs2
+      roots.foldLeft(Chapter_Defs.empty) {
+        case (defs1, root) =>
+          root.entries.foldLeft(defs1) {
+            case (defs2, entry: Chapter_Def) => defs2 + entry
+            case (defs2, _) => defs2
           }
       }
 
     val info_roots = {
       var chapter = UNSORTED
       val info_roots = new mutable.ListBuffer[Info]
-      for ((select, dir, entries) <- unique_roots) {
-        entries.foreach {
+      for (root <- roots) {
+        root.entries.foreach {
           case entry: Chapter_Entry => chapter = entry.name
           case entry: Session_Entry =>
-            info_roots += make_info(chapter_defs, options, select, dir, chapter, entry)
+            info_roots += make_info(chapter_defs, options, root.select, root.dir, chapter, entry)
           case _ =>
         }
         chapter = UNSORTED
@@ -1166,6 +1183,16 @@
     Structure.make(chapter_defs, info_roots ::: infos)
   }
 
+  def load_structure(
+    options: Options,
+    dirs: List[Path] = Nil,
+    select_dirs: List[Path] = Nil,
+    infos: List[Info] = Nil
+  ): Structure = {
+    val roots = load_root_files(dirs = dirs, select_dirs = select_dirs)
+    make_structure(options, roots = roots, infos = infos)
+  }
+
 
   /* Isabelle tool wrapper */