removed somewhat pointless transaction: db is meant to be finished (or updated monotonically);

--- a/src/Pure/Thy/export.scala	Tue Aug 02 19:25:37 2022 +0200
+++ b/src/Pure/Thy/export.scala	Wed Aug 03 11:23:12 2022 +0200
@@ -329,28 +329,26 @@
     export_patterns: List[String] = Nil
   ): Unit = {
     using(store.open_database(session_name)) { db =>
-      db.transaction {
-        val entry_names = read_entry_names(db, session_name)
+      val entry_names = read_entry_names(db, session_name)
 
-        // list
-        if (export_list) {
-          for (entry_name <- entry_names) progress.echo(entry_name.compound_name)
-        }
+      // list
+      if (export_list) {
+        for (entry_name <- entry_names) progress.echo(entry_name.compound_name)
+      }
 
-        // export
-        if (export_patterns.nonEmpty) {
-          val matcher = make_matcher(export_patterns)
-          for {
-            entry_name <- entry_names if matcher(entry_name)
-            entry <- entry_name.read(db, store.cache)
-          } {
-            val path = export_dir + entry_name.make_path(prune = export_prune)
-            progress.echo("export " + path + (if (entry.executable) " (executable)" else ""))
-            Isabelle_System.make_directory(path.dir)
-            val bytes = entry.uncompressed
-            if (!path.is_file || Bytes.read(path) != bytes) Bytes.write(path, bytes)
-            File.set_executable(path, entry.executable)
-          }
+      // export
+      if (export_patterns.nonEmpty) {
+        val matcher = make_matcher(export_patterns)
+        for {
+          entry_name <- entry_names if matcher(entry_name)
+          entry <- entry_name.read(db, store.cache)
+        } {
+          val path = export_dir + entry_name.make_path(prune = export_prune)
+          progress.echo("export " + path + (if (entry.executable) " (executable)" else ""))
+          Isabelle_System.make_directory(path.dir)
+          val bytes = entry.uncompressed
+          if (!path.is_file || Bytes.read(path) != bytes) Bytes.write(path, bytes)
+          File.set_executable(path, entry.executable)
         }
       }
     }

--- a/src/Pure/Thy/export_theory.scala	Tue Aug 02 19:25:37 2022 +0200
+++ b/src/Pure/Thy/export_theory.scala	Wed Aug 03 11:23:12 2022 +0200
@@ -33,13 +33,11 @@
     val thys =
       sessions_structure.build_requirements(List(session_name)).flatMap(session =>
         using(store.open_database(session)) { db =>
-          db.transaction {
-            for (theory <- Export.read_theory_names(db, session))
-            yield {
-              progress.echo("Reading theory " + theory)
-              val provider = Export.Provider.database(db, store.cache, session, theory)
-              read_theory(provider, session, theory, cache = cache)
-            }
+          for (theory <- Export.read_theory_names(db, session))
+          yield {
+            progress.echo("Reading theory " + theory)
+            val provider = Export.Provider.database(db, store.cache, session, theory)
+            read_theory(provider, session, theory, cache = cache)
           }
         })
 
@@ -153,10 +151,8 @@
     val theory_name = Thy_Header.PURE
 
     using(store.open_database(session_name)) { db =>
-      db.transaction {
-        val provider = Export.Provider.database(db, store.cache, session_name, theory_name)
-        read(provider, session_name, theory_name)
-      }
+      val provider = Export.Provider.database(db, store.cache, session_name, theory_name)
+      read(provider, session_name, theory_name)
     }
   }
 

--- 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(