# HG changeset patch
# User wenzelm
# Date 1689500813 -7200
# Node ID f5cf8e500dee6914399f6dde59db04e6b3701eb9
# Parent  0cecb723629838f0b69f1fef2f79b04ae114313e
clarified isabelle.transaction_log: support time_min (in ms);

diff -r 0cecb7236298 -r f5cf8e500dee src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Sun Jul 16 11:43:32 2023 +0200
+++ b/src/Pure/General/sql.scala	Sun Jul 16 11:46:53 2023 +0200
@@ -465,14 +465,21 @@
       label: String = "",
       log: Logger = new System_Logger
     )(body: => A): A = {
-      val trace_enabled = System.getProperty("isabelle.transaction_log", "") == "true"
+      val prop = "isabelle.transaction_trace"
+      val trace_min =
+        System.getProperty(prop, "") match {
+          case Value.Long(ms) => Time.ms(ms)
+          case "true" => Time.min
+          case "false" | "" => Time.max
+          case s => error("Bad system property " + prop + ": " + quote(s))
+        }
 
-      val trace_count = if (trace_enabled) transaction_count() else 0
+      val trace_count = transaction_count()
       val trace_start = Time.now()
 
       def trace(msg: => String, nl: Boolean = false): Unit = {
-        if (trace_enabled) {
-          val trace_time = Time.now() - trace_start
+        val trace_time = Time.now() - trace_start
+        if (trace_time >= trace_min) {
           log((if (nl) "\n" else "") + trace_time + " transaction " +
             (if (label.isEmpty) "" else label + " ") + trace_count + ": " + msg)
         }