# HG changeset patch
# User wenzelm
# Date 1689498190 -7200
# Node ID 9fbc6a043268ce1b08c78a229fafe10098321be3
# Parent  3b8f100f638584d73ad755222edad9957962d51c
support trace of transaction_lock via property "isabelle.transaction_log";

diff -r 3b8f100f6385 -r 9fbc6a043268 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Sun Jul 16 10:50:40 2023 +0200
+++ b/src/Pure/General/sql.scala	Sun Jul 16 11:03:10 2023 +0200
@@ -242,10 +242,11 @@
     def iterator: Iterator[Table] = list.iterator
 
     // requires transaction
-    def lock(db: Database, create: Boolean = false): Unit = {
+    def lock(db: Database, create: Boolean = false): Boolean = {
       if (create) foreach(db.create_table(_))
       val sql = db.lock_tables(list)
-      if (sql.nonEmpty) db.execute_statement(sql)
+      if (sql.nonEmpty) { db.execute_statement(sql); true }
+      else false
     }
   }
 
@@ -255,9 +256,10 @@
     def transaction_lock[A](
       db: Database,
       create: Boolean = false,
+      log: Logger = new System_Logger,
       synchronized: Boolean = false,
     )(body: => A): A = {
-      def run: A = db.transaction_lock(tables, create = create)(body)
+      def run: A = db.transaction_lock(tables, create = create, log = log)(body)
       if (synchronized) db.synchronized { run } else run
     }
 
@@ -452,8 +454,38 @@
       finally { connection.setAutoCommit(auto_commit) }
     }
 
-    def transaction_lock[A](tables: Tables, create: Boolean = false)(body: => A): A =
-      transaction { tables.lock(db, create = create); body }
+    private var _transaction_count: Int = 0
+    private def transaction_count(): Int =
+      synchronized { _transaction_count += 1; _transaction_count }
+
+    def transaction_lock[A](
+      tables: Tables,
+      create: Boolean = false,
+      log: Logger = new System_Logger
+    )(body: => A): A = {
+      val trace_enabled = System.getProperty("isabelle.transaction_log", "") == "true"
+
+      val trace_count = if (trace_enabled) transaction_count() else 0
+      val trace_start = Time.now()
+
+      def trace(msg: => String, nl: Boolean = false): Unit = {
+        if (trace_enabled) {
+          val trace_time = Time.now() - trace_start
+          log((if (nl) "\n" else "") + trace_time + " transaction " + trace_count + ": " + msg)
+        }
+      }
+
+      val res =
+        transaction {
+          trace("begin", nl = true)
+          if (tables.lock(db, create = create)) trace("locked")
+          val res = Exn.capture { body }
+          trace("end")
+          res
+        }
+      trace("commit")
+      Exn.release(res)
+    }
 
     def lock_tables(tables: List[Table]): Source = ""  // PostgreSQL only