src/Pure/Thy/sessions.scala

--- a/src/Pure/Thy/sessions.scala	Tue Aug 02 19:25:37 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Wed Aug 03 11:23:12 2022 +0200
@@ -1245,15 +1245,13 @@
         patterns = structure(name).export_classpath if patterns.nonEmpty
       } yield {
         database(name) { db =>
-          db.transaction {
-            val matcher = Export.make_matcher(patterns)
-            val res =
-              for {
-                entry_name <- Export.read_entry_names(db, name) if matcher(entry_name)
-                entry <- entry_name.read(db, store.cache)
-              } yield File.Content(entry.entry_name.make_path(), entry.uncompressed)
-            Some(res)
-          }
+          val matcher = Export.make_matcher(patterns)
+          val res =
+            for {
+              entry_name <- Export.read_entry_names(db, name) if matcher(entry_name)
+              entry <- entry_name.read(db, store.cache)
+            } yield File.Content(entry.entry_name.make_path(), entry.uncompressed)
+          Some(res)
         }.getOrElse(Nil)
       }).flatten
     }
@@ -1438,12 +1436,10 @@
     }
 
     def session_info_defined(db: SQL.Database, name: String): Boolean =
-      db.transaction {
-        session_info_exists(db) && {
-          db.using_statement(
-            Session_Info.table.select(List(Session_Info.session_name),
-              Session_Info.session_name.where_equal(name)))(stmt => stmt.execute_query().next())
-        }
+      session_info_exists(db) && {
+        db.using_statement(
+          Session_Info.table.select(List(Session_Info.session_name),
+            Session_Info.session_name.where_equal(name)))(stmt => stmt.execute_query().next())
       }
 
     def write_session_info(