--- a/src/Pure/Thy/export.scala Sun Jul 16 15:53:13 2023 +0200
+++ b/src/Pure/Thy/export.scala Sun Jul 16 16:11:12 2023 +0200
@@ -332,7 +332,8 @@
case Some(db) => session_hierarchy.map(name => new Session_Database(name, db))
case None =>
val attempts =
- session_hierarchy.map(name => name -> store.try_open_database(name, server = false))
+ for (name <- session_hierarchy)
+ yield name -> store.try_open_database(name, server_mode = false)
attempts.collectFirst({ case (name, None) => name }) match {
case Some(bad) =>
for ((_, Some(db)) <- attempts) db.close()