# HG changeset patch
# User wenzelm
# Date 1688745885 -7200
# Node ID 03eb7f7bb990f6bf7248acd58d0c1c7406590617
# Parent  c8fde312c895748a4d9c8ee8bba7be17a97a49aa
proper transaction_lock;
clarified signature;

diff -r c8fde312c895 -r 03eb7f7bb990 src/Pure/Thy/store.scala
--- a/src/Pure/Thy/store.scala	Fri Jul 07 14:20:58 2023 +0200
+++ b/src/Pure/Thy/store.scala	Fri Jul 07 18:04:45 2023 +0200
@@ -125,6 +125,54 @@
           if_proper(name, Sources.name.equal(name)))
     }
 
+    def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
+      db.execute_query_statementO[Bytes](
+        Session_Info.table.select(List(column), sql = Session_Info.session_name.where_equal(name)),
+        res => res.bytes(column)
+      ).getOrElse(Bytes.empty)
+
+    def read_properties(
+      db: SQL.Database, name: String, column: SQL.Column, cache: Term.Cache
+    ): List[Properties.T] = Properties.uncompress(read_bytes(db, name, column), cache = cache)
+
+    def read_session_timing(db: SQL.Database, name: String, cache: Term.Cache): Properties.T =
+      Properties.decode(read_bytes(db, name, Session_Info.session_timing), cache = cache)
+
+    def read_command_timings(db: SQL.Database, name: String): Bytes =
+      read_bytes(db, name, Session_Info.command_timings)
+
+    def read_theory_timings(db: SQL.Database, name: String, cache: Term.Cache): List[Properties.T] =
+      read_properties(db, name, Session_Info.theory_timings, cache)
+
+    def read_ml_statistics(db: SQL.Database, name: String, cache: Term.Cache): List[Properties.T] =
+      read_properties(db, name, Session_Info.ml_statistics, cache)
+
+    def read_task_statistics(db: SQL.Database, name: String, cache: Term.Cache): List[Properties.T] =
+      read_properties(db, name, Session_Info.task_statistics, cache)
+
+    def read_errors(db: SQL.Database, name: String, cache: Term.Cache): List[String] =
+      Build_Log.uncompress_errors(read_bytes(db, name, Session_Info.errors), cache = cache)
+
+    def read_build(db: SQL.Database, name: String): Option[Store.Build_Info] = {
+      if (db.tables.contains(Session_Info.table.name)) {
+        db.execute_query_statementO[Store.Build_Info](
+          Session_Info.table.select(sql = Session_Info.session_name.where_equal(name)),
+          { res =>
+            val uuid =
+              try { Option(res.string(Session_Info.uuid)).getOrElse("") }
+              catch { case _: SQLException => "" }
+            Store.Build_Info(
+              SHA1.fake_shasum(res.string(Session_Info.sources)),
+              SHA1.fake_shasum(res.string(Session_Info.input_heaps)),
+              SHA1.fake_shasum(res.string(Session_Info.output_heap)),
+              res.int(Session_Info.return_code),
+              uuid)
+          }
+        )
+      }
+      else None
+    }
+
     def write_session_info(
       db: SQL.Database,
       cache: Compress.Cache,
@@ -163,9 +211,9 @@
 
     def read_sources(
       db: SQL.Database,
-      cache: Compress.Cache,
       session_name: String,
-      name: String = ""
+      name: String,
+      cache: Compress.Cache
     ): List[Source_File] = {
       db.execute_query_statement(
         Sources.table.select(
@@ -359,19 +407,6 @@
   }
 
 
-  /* SQL database content */
-
-  def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
-    db.execute_query_statementO[Bytes](
-      Store.Data.Session_Info.table.select(List(column),
-        sql = Store.Data.Session_Info.session_name.where_equal(name)),
-      res => res.bytes(column)
-    ).getOrElse(Bytes.empty)
-
-  def read_properties(db: SQL.Database, name: String, column: SQL.Column): List[Properties.T] =
-    Properties.uncompress(read_bytes(db, name, column), cache = cache)
-
-
   /* session info */
 
   def session_info_exists(db: SQL.Database): Boolean = {
@@ -416,48 +451,30 @@
     }
   }
 
-  def read_session_timing(db: SQL.Database, name: String): Properties.T =
-    Properties.decode(read_bytes(db, name, Store.Data.Session_Info.session_timing), cache = cache)
+  def read_session_timing(db: SQL.Database, session: String): Properties.T =
+    Store.Data.transaction_lock(db) { Store.Data.read_session_timing(db, session, cache) }
 
-  def read_command_timings(db: SQL.Database, name: String): Bytes =
-    read_bytes(db, name, Store.Data.Session_Info.command_timings)
-
-  def read_theory_timings(db: SQL.Database, name: String): List[Properties.T] =
-    read_properties(db, name, Store.Data.Session_Info.theory_timings)
+  def read_command_timings(db: SQL.Database, session: String): Bytes =
+    Store.Data.transaction_lock(db) { Store.Data.read_command_timings(db, session) }
 
-  def read_ml_statistics(db: SQL.Database, name: String): List[Properties.T] =
-    read_properties(db, name, Store.Data.Session_Info.ml_statistics)
-
-  def read_task_statistics(db: SQL.Database, name: String): List[Properties.T] =
-    read_properties(db, name, Store.Data.Session_Info.task_statistics)
+  def read_theory_timings(db: SQL.Database, session: String): List[Properties.T] =
+    Store.Data.transaction_lock(db) { Store.Data.read_theory_timings(db, session, cache) }
 
-  def read_theories(db: SQL.Database, name: String): List[String] =
-    read_theory_timings(db, name).flatMap(Markup.Name.unapply)
-
-  def read_errors(db: SQL.Database, name: String): List[String] =
-    Build_Log.uncompress_errors(read_bytes(db, name, Store.Data.Session_Info.errors), cache = cache)
+  def read_ml_statistics(db: SQL.Database, session: String): List[Properties.T] =
+    Store.Data.transaction_lock(db) { Store.Data.read_ml_statistics(db, session, cache) }
 
-  def read_build(db: SQL.Database, name: String): Option[Store.Build_Info] = {
-    if (db.tables.contains(Store.Data.Session_Info.table.name)) {
-      db.execute_query_statementO[Store.Build_Info](
-        Store.Data.Session_Info.table.select(
-          sql = Store.Data.Session_Info.session_name.where_equal(name)),
-        { res =>
-          val uuid =
-            try { Option(res.string(Store.Data.Session_Info.uuid)).getOrElse("") }
-            catch { case _: SQLException => "" }
-          Store.Build_Info(
-            SHA1.fake_shasum(res.string(Store.Data.Session_Info.sources)),
-            SHA1.fake_shasum(res.string(Store.Data.Session_Info.input_heaps)),
-            SHA1.fake_shasum(res.string(Store.Data.Session_Info.output_heap)),
-            res.int(Store.Data.Session_Info.return_code),
-            uuid)
-        }
-      )
-    }
-    else None
-  }
+  def read_task_statistics(db: SQL.Database, session: String): List[Properties.T] =
+    Store.Data.transaction_lock(db) { Store.Data.read_task_statistics(db, session, cache) }
+
+  def read_theories(db: SQL.Database, session: String): List[String] =
+    read_theory_timings(db, session).flatMap(Markup.Name.unapply)
+
+  def read_errors(db: SQL.Database, session: String): List[String] =
+    Store.Data.transaction_lock(db) { Store.Data.read_errors(db, session, cache) }
+
+  def read_build(db: SQL.Database, session: String): Option[Store.Build_Info] =
+    Store.Data.transaction_lock(db) { Store.Data.read_build(db, session) }
 
   def read_sources(db: SQL.Database, session: String, name: String = ""): List[Store.Source_File] =
-    Store.Data.read_sources(db, cache.compress, session, name = name)
+    Store.Data.transaction_lock(db) { Store.Data.read_sources(db, session, name, cache.compress) }
 }