--- a/src/Pure/Thy/sessions.scala Mon Jul 11 13:21:22 2022 +0200
+++ b/src/Pure/Thy/sessions.scala Mon Jul 11 13:36:08 2022 +0200
@@ -1216,12 +1216,15 @@
database_server match {
case Some(db) =>
sessions.view.map(session_name =>
- Export.Entry_Name(session_name, theory_name, name).read(db, store.cache))
+ Export.Entry_Name(session = session_name, theory = theory_name, name = name)
+ .read(db, store.cache))
case None =>
sessions.view.map(session_name =>
store.try_open_database(session_name) match {
case Some(db) =>
- using(db)(Export.Entry_Name(session_name, theory_name, name).read(_, store.cache))
+ using(db) { _ =>
+ Export.Entry_Name(session = session_name, theory = theory_name, name = name)
+ .read(db, store.cache) }
case None => None
})
}