clarified signature: more general operations;

--- a/src/Pure/Thy/export.scala	Mon Jan 02 15:18:13 2023 +0100
+++ b/src/Pure/Thy/export.scala	Mon Jan 02 15:28:33 2023 +0100
@@ -430,10 +430,14 @@
           node = snapshot.get_node(name)
           text = node.source if text.nonEmpty
         } yield text
+
+      val store = database_context.store
       def db_source: Option[String] =
-        db_hierarchy.view.map(database =>
-            database_context.store.read_sources(database.db, database.session, name.node))
-          .collectFirst({ case Some(file) => file.text })
+        (for {
+          database <- db_hierarchy.iterator
+          file <- store.read_sources(database.db, database.session, name = name.node).iterator
+        } yield file.text).nextOption()
+
       snapshot_source orElse db_source getOrElse ""
     }
 

--- a/src/Pure/Thy/sessions.scala	Mon Jan 02 15:18:13 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Jan 02 15:28:33 2023 +0100
@@ -1661,18 +1661,22 @@
       }
     }
 
-    def read_sources(db: SQL.Database, session_name: String, name: String): Option[Source_File] = {
-      val sql =
-        Sources.table.select(Nil, Sources.where_equal(session_name, name = name))
-      db.using_statement(sql) { stmt =>
-        val res = stmt.execute_query()
-        if (!res.next()) None
-        else {
+    def read_sources(
+      db: SQL.Database,
+      session_name: String,
+      name: String = ""
+    ): List[Source_File] = {
+      val select =
+        Sources.table.select(Nil,
+          Sources.where_equal(session_name, name = name) + " ORDER BY " + Sources.name)
+      db.using_statement(select) { stmt =>
+        (stmt.execute_query().iterator { res =>
+          val res_name = res.string(Sources.name)
           val digest = SHA1.fake_digest(res.string(Sources.digest))
           val compressed = res.bool(Sources.compressed)
           val body = res.bytes(Sources.body)
-          Some(Source_File(name, digest, compressed, body, cache.compress))
-        }
+          Source_File(res_name, digest, compressed, body, cache.compress)
+        }).toList
       }
     }
   }