clarified signature: incorporate guard into Logger;

--- a/src/Pure/General/logger.scala	Mon Mar 04 21:58:53 2024 +0100
+++ b/src/Pure/General/logger.scala	Tue Mar 05 15:54:33 2024 +0100
@@ -8,41 +8,51 @@
 
 
 object Logger {
-  def make(log_file: Option[Path]): Logger =
-    log_file match { case Some(file) => new File_Logger(file) case None => No_Logger }
+  def make_file(log_file: Option[Path], guard_time: Time = Time.min): Logger =
+    log_file match {
+      case Some(file) => new File_Logger(file, guard_time)
+      case None => No_Logger
+    }
 
-  def make(progress: Progress): Logger =
-    new Logger { def apply(msg: => String): Unit = if (progress != null) progress.echo(msg) }
+  def make_progress(progress: Progress, guard_time: Time = Time.min): Logger =
+    new Logger {
+      override def output(msg: => String): Unit =
+        if (progress != null) progress.echo(msg)
+    }
 
-  def make_system_log(progress: Progress, options: Options): Logger =
+  def make_system_log(progress: Progress, options: Options, guard_time: Time = Time.min): Logger =
     options.string("system_log") match {
       case "" => No_Logger
-      case "-" => make(progress)
-      case log_file => make(Some(Path.explode(log_file)))
+      case "-" => make_progress(progress, guard_time = guard_time)
+      case log_file => make_file(Some(Path.explode(log_file)), guard_time = guard_time)
     }
 }
 
 trait Logger {
-  def apply(msg: => String): Unit
+  val guard_time: Time = Time.min
+  def guard(t: Time): Boolean = t >= guard_time
+  def output(msg: => String): Unit = {}
 
-  def timeit[A](body: => A,
+  final def apply(msg: => String, time: Option[Time] = None): Unit =
+    if (time.isEmpty || guard(time.get)) output(msg)
+
+  final def timeit[A](body: => A,
     message: Exn.Result[A] => String = null,
     enabled: Boolean = true
   ): A = Timing.timeit(body, message = message, enabled = enabled, output = apply(_))
 }
 
-object No_Logger extends Logger {
-  def apply(msg: => String): Unit = {}
-}
+object No_Logger extends Logger
 
-class File_Logger(path: Path) extends Logger {
-  def apply(msg: => String): Unit = synchronized { File.append(path, msg + "\n") }
-
+class File_Logger(path: Path, override val guard_time: Time = Time.min)
+extends Logger {
+  override def output(msg: => String): Unit = synchronized { File.append(path, msg + "\n") }
   override def toString: String = path.toString
 }
 
-class System_Logger extends Logger {
-  def apply(msg: => String): Unit = synchronized {
+class System_Logger(override val guard_time: Time = Time.min)
+extends Logger {
+  override def output(msg: => String): Unit = synchronized {
     if (Platform.is_windows) System.out.println(msg)
     else System.console.writer.println(msg)
   }

--- a/src/Pure/General/sql.scala	Mon Mar 04 21:58:53 2024 +0100
+++ b/src/Pure/General/sql.scala	Tue Mar 05 15:54:33 2024 +0100
@@ -243,6 +243,12 @@
     }
   }
 
+
+  /* access data */
+
+  def transaction_logger(): Logger =
+    new System_Logger(guard_time = Time.guard_property("isabelle.transaction_trace"))
+
   abstract class Data(table_prefix: String = "") {
     def tables: Tables
 
@@ -250,7 +256,7 @@
       db: Database,
       create: Boolean = false,
       label: String = "",
-      log: Logger = new System_Logger
+      log: Logger = transaction_logger()
     )(body: => A): A = {
       db.transaction_lock(tables, create = create, label = label, log = log)(body)
     }
@@ -468,24 +474,15 @@
       tables: Tables,
       create: Boolean = false,
       label: String = "",
-      log: Logger = new System_Logger
+      log: Logger = transaction_logger()
     )(body: => A): A = {
-      val prop = "isabelle.transaction_trace"
-      val trace_min =
-        System.getProperty(prop, "") match {
-          case Value.Seconds(t) => t
-          case "true" => Time.min
-          case "false" | "" => Time.max
-          case s => error("Bad system property " + prop + ": " + quote(s))
-        }
-
       val trace_count = - SQL.transaction_count()
       val trace_start = Time.now()
       var trace_nl = false
 
       def trace(msg: String): Unit = {
         val trace_time = Time.now() - trace_start
-        if (trace_time >= trace_min) {
+        if (log.guard(trace_time)) {
           time_start
           val nl =
             if (trace_nl) ""

--- a/src/Pure/General/time.scala	Mon Mar 04 21:58:53 2024 +0100
+++ b/src/Pure/General/time.scala	Tue Mar 05 15:54:33 2024 +0100
@@ -27,6 +27,16 @@
     String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef])
 
   def instant(t: Instant): Time = ms(t.getEpochSecond * 1000L + t.getNano / 1000000L)
+
+  def guard_property(prop: String): Time =
+    System.getProperty(prop, "") match {
+      case Value.Seconds(t) => t
+      case "true" => Time.min
+      case "false" | "" => Time.max
+      case s =>
+        error("Bad system property " + prop + ": " + quote(s) +
+        "\n expected true, false, or time in seconds")
+    }
 }
 
 final class Time private(val ms: Long) extends AnyVal {

--- a/src/Pure/Tools/server.scala	Mon Mar 04 21:58:53 2024 +0100
+++ b/src/Pure/Tools/server.scala	Tue Mar 05 15:54:33 2024 +0100
@@ -495,7 +495,7 @@
           sys.exit(if (ok) Process_Result.RC.ok else Process_Result.RC.failure)
         }
         else {
-          val log = Logger.make(log_file)
+          val log = Logger.make_file(log_file)
           val (server_info, server) =
             init(name, port = port, existing_server = existing_server, log = log)
           Output.writeln(server_info.toString, stdout = true)

--- a/src/Tools/VSCode/src/language_server.scala	Mon Mar 04 21:58:53 2024 +0100
+++ b/src/Tools/VSCode/src/language_server.scala	Tue Mar 05 15:54:33 2024 +0100
@@ -73,7 +73,7 @@
           val more_args = getopts(args)
           if (more_args.nonEmpty) getopts.usage()
 
-          val log = Logger.make(log_file)
+          val log = Logger.make_file(log_file)
           val channel = new Channel(System.in, System.out, log, verbose)
           val server =
             new Language_Server(channel, options, session_name = logic, session_dirs = dirs,