# HG changeset patch # User wenzelm # Date 1709650473 -3600 # Node ID 752806151432a9dc40d58250874c113a8c81c17c # Parent 48af00f6f110c325a681a2839464a9f7793569f5 clarified signature: incorporate guard into Logger; diff -r 48af00f6f110 -r 752806151432 src/Pure/General/logger.scala --- 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) } diff -r 48af00f6f110 -r 752806151432 src/Pure/General/sql.scala --- 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) "" diff -r 48af00f6f110 -r 752806151432 src/Pure/General/time.scala --- 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 { diff -r 48af00f6f110 -r 752806151432 src/Pure/Tools/server.scala --- 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) diff -r 48af00f6f110 -r 752806151432 src/Tools/VSCode/src/language_server.scala --- 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,