src/Pure/Thy/export.scala

--- 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 ""
     }