# HG changeset patch
# User wenzelm
# Date 1659711004 -7200
# Node ID d795d8b5956314e8121a714a4f00ef9e57a3812c
# Parent  b10c3d9dd48a411db2df7d25c847e64689bb5da8
proper session_databases for database_server: need to follow precise session_hierarchy;

diff -r b10c3d9dd48a -r d795d8b59563 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Fri Aug 05 16:40:06 2022 +0200
+++ b/src/Pure/Thy/export.scala	Fri Aug 05 16:50:04 2022 +0200
@@ -356,8 +356,8 @@
       val session_hierarchy = resources.sessions_structure.build_hierarchy(session)
       db_context.database_server match {
         case Some(db) =>
-          val session_database = new Session_Database(session, db)
-          new Session_Context(resources, snapshot, db_context.cache, List(session_database))
+          val session_databases = session_hierarchy.map(name => new Session_Database(name, db))
+          new Session_Context(resources, snapshot, db_context.cache, session_databases)
         case None =>
           val store = db_context.store
           val session_databases = {