# HG changeset patch
# User wenzelm
# Date 1670926289 -3600
# Node ID 207932c3435346629ca00df920f030e0d0fc9253
# Parent  7db5744fcf4f381a96c95019338189e266ef3344
clarified modules;

diff -r 7db5744fcf4f -r 207932c34353 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Dec 13 11:01:04 2022 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Dec 13 11:11:29 2022 +0100
@@ -668,9 +668,47 @@
   }
 
   object Structure {
-    val empty: Structure = make(Chapter_Defs.empty, Nil)
+    val empty: Structure = make(Options.empty)
+
+    def make(
+      options: Options,
+      roots: List[Root_File] = Nil,
+      infos: List[Info] = Nil
+    ): Structure = {
+      val chapter_defs: Chapter_Defs =
+        roots.foldLeft(Chapter_Defs.empty) {
+          case (defs1, root) =>
+            root.entries.foldLeft(defs1) {
+              case (defs2, entry: Chapter_Def) => defs2 + entry
+              case (defs2, _) => defs2
+            }
+        }
 
-    def make(chapter_defs: Chapter_Defs, all_infos: List[Info]): Structure = {
+      val root_infos = {
+        var chapter = UNSORTED
+        val info_roots = new mutable.ListBuffer[Info]
+        for (root <- roots) {
+          root.entries.foreach {
+            case entry: Chapter_Entry => chapter = entry.name
+            case entry: Session_Entry =>
+              info_roots += make_info(chapter_defs, options, root.select, root.dir, chapter, entry)
+            case _ =>
+          }
+          chapter = UNSORTED
+        }
+        info_roots.toList
+      }
+
+      val info_graph =
+        (root_infos ::: infos).foldLeft(Graph.string[Info]) {
+          case (graph, info) =>
+            if (graph.defined(info.name)) {
+              error("Duplicate session " + quote(info.name) + Position.here(info.pos) +
+                Position.here(graph.get_node(info.name).pos))
+            }
+            else graph.new_node(info.name, info)
+        }
+
       def augment_graph(
         graph: Graph[String, Info],
         kind: String,
@@ -696,15 +734,6 @@
         }
       }
 
-      val info_graph =
-        all_infos.foldLeft(Graph.string[Info]) {
-          case (graph, info) =>
-            if (graph.defined(info.name)) {
-              error("Duplicate session " + quote(info.name) + Position.here(info.pos) +
-                Position.here(graph.get_node(info.name).pos))
-            }
-            else graph.new_node(info.name, info)
-        }
       val build_graph = augment_graph(info_graph, "parent", _.parent)
       val imports_graph = augment_graph(build_graph, "imports", _.imports)
 
@@ -1152,38 +1181,6 @@
     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 =
-      roots.foldLeft(Chapter_Defs.empty) {
-        case (defs1, root) =>
-          root.entries.foldLeft(defs1) {
-            case (defs2, entry: Chapter_Def) => defs2 + entry
-            case (defs2, _) => defs2
-          }
-      }
-
-    val root_infos = {
-      var chapter = UNSORTED
-      val info_roots = new mutable.ListBuffer[Info]
-      for (root <- roots) {
-        root.entries.foreach {
-          case entry: Chapter_Entry => chapter = entry.name
-          case entry: Session_Entry =>
-            info_roots += make_info(chapter_defs, options, root.select, root.dir, chapter, entry)
-          case _ =>
-        }
-        chapter = UNSORTED
-      }
-      info_roots.toList
-    }
-
-    Structure.make(chapter_defs, root_infos ::: infos)
-  }
-
   def load_structure(
     options: Options,
     dirs: List[Path] = Nil,
@@ -1191,7 +1188,7 @@
     infos: List[Info] = Nil
   ): Structure = {
     val roots = load_root_files(dirs = dirs, select_dirs = select_dirs)
-    make_structure(options, roots = roots, infos = infos)
+    Structure.make(options, roots = roots, infos = infos)
   }