# HG changeset patch
# User wenzelm
# Date 1661594285 -7200
# Node ID 627a08637c35c04fda099e682a6cf2a2be1cb404
# Parent  f0ea03be7cebf2e1f77a81519c7a1ae5291cd3b6
tuned;

diff -r f0ea03be7ceb -r 627a08637c35 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Aug 26 23:37:21 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat Aug 27 11:58:05 2022 +0200
@@ -1018,24 +1018,6 @@
     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,
-    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 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, chapter_defs1)
-  }
-
   def parse_roots(roots: Path): List[String] = {
     for {
       line <- split_lines(File.read(roots))
@@ -1108,13 +1090,18 @@
 
     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
+      val info_roots = new mutable.ListBuffer[Info]
+
+      for ((select, path) <- unique_roots) {
+        var entry_chapter = UNSORTED
+        parse_root(path).foreach {
+          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)
+        }
       }
-      (chapter_defs, result.toList)
+      (chapter_defs, info_roots.toList)
     }
 
     Structure.make(chapter_defs, info_roots ::: infos)