# HG changeset patch
# User wenzelm
# Date 1709660529 -3600
# Node ID a79280c7e8d5ded2dda4185e989ea4941fdf4836
# Parent  1f94d92b0dc26746c013935b949ff44f1c88024c# Parent  60e985e2a12f8e5d9f103b5e690e2f5b9f650c81
merged

diff -r 1f94d92b0dc2 -r a79280c7e8d5 Admin/Windows/Cygwin/README
--- a/Admin/Windows/Cygwin/README	Tue Mar 05 16:55:21 2024 +0100
+++ b/Admin/Windows/Cygwin/README	Tue Mar 05 18:42:09 2024 +0100
@@ -22,6 +22,7 @@
   - https://isabelle.sketis.net/cygwin_2021-1  (Isabelle2021-1)
   - https://isabelle.sketis.net/cygwin_2022  (Isabelle2022)
   - https://isabelle.sketis.net/cygwin_2023  (Isabelle2023)
+  - https://isabelle.sketis.net/cygwin_2024  (Isabelle2024)
 
 * Apache2 redirects for virtual host isabelle.conf:
 ```
@@ -57,6 +58,8 @@
   Redirect /cygwin_2022/noarch/release https://ftp.eq.uc.pt/software/pc/prog/cygwin/noarch/release
   Redirect /cygwin_2023/x86_64/release https://ftp.eq.uc.pt/software/pc/prog/cygwin/x86_64/release
   Redirect /cygwin_2023/noarch/release https://ftp.eq.uc.pt/software/pc/prog/cygwin/noarch/release
+  Redirect /cygwin_2024/x86_64/release https://ftp.eq.uc.pt/software/pc/prog/cygwin/x86_64/release
+  Redirect /cygwin_2024/noarch/release https://ftp.eq.uc.pt/software/pc/prog/cygwin/noarch/release
 ```
 
 * Quasi-component: "isabelle component_cygwin" (as Administrator)
diff -r 1f94d92b0dc2 -r a79280c7e8d5 Admin/components/PLATFORMS
--- a/Admin/components/PLATFORMS	Tue Mar 05 16:55:21 2024 +0100
+++ b/Admin/components/PLATFORMS	Tue Mar 05 18:42:09 2024 +0100
@@ -47,7 +47,7 @@
                     macOS 14 Sonoma (studio1 Mac13,2 M1 Ultra, 16+4 cores)
 
   x86_64-windows    Windows 10
-  x86_64-cygwin     Cygwin 3.4.x https://isabelle.sketis.net/cygwin_2023 (x86_64/release)
+  x86_64-cygwin     Cygwin 3.5.x https://isabelle.sketis.net/cygwin_2024 (x86_64/release)
 
 
 64 bit vs. 32 bit platform personality
diff -r 1f94d92b0dc2 -r a79280c7e8d5 Admin/components/bundled-windows
--- a/Admin/components/bundled-windows	Tue Mar 05 16:55:21 2024 +0100
+++ b/Admin/components/bundled-windows	Tue Mar 05 18:42:09 2024 +0100
@@ -1,3 +1,3 @@
 #additional components to be bundled for release
-cygwin-20230711-1
+cygwin-20240305
 windows_app-20240205
diff -r 1f94d92b0dc2 -r a79280c7e8d5 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Tue Mar 05 16:55:21 2024 +0100
+++ b/Admin/components/components.sha1	Tue Mar 05 18:42:09 2024 +0100
@@ -80,6 +80,7 @@
 6cd34e30e2e650f239d19725c3d15c206fb3a7cf cygwin-20221002.tar.gz
 fe8c541722f2fd6940f9e9948928b55fbc32d14b cygwin-20230711-1.tar.gz
 bc634cae08dea80238a830955894919af995cf06 cygwin-20230711.tar.gz
+ea23f766909632d8a6c0fefafbde467d1d289383 cygwin-20240305.tar.gz
 0fe549949a025d65d52d6deca30554de8fca3b6e e-1.5.tar.gz
 2e293256a134eb8e5b1a283361b15eb812fbfbf1 e-1.6-1.tar.gz
 e1919e72416cbd7ac8de5455caba8901acc7b44d e-1.6-2.tar.gz
diff -r 1f94d92b0dc2 -r a79280c7e8d5 NEWS
--- a/NEWS	Tue Mar 05 16:55:21 2024 +0100
+++ b/NEWS	Tue Mar 05 18:42:09 2024 +0100
@@ -9,6 +9,13 @@
 
 *** General ***
 
+* Dropped support for very old operating systems. The platform
+base-lines are now as follows:
+
+  - Ubuntu Linux 18.04 LTS
+  - macOS 11 Big Sur
+  - Windows 10 or Windows Server 2012 R2
+
 * The arm64-linux platform is now officially supported, although a few
 (non-essential) tools are missing:
 
@@ -174,9 +181,6 @@
 * Update to GHC stack 2.15.1 with support for all platforms, including
 ARM Linux and Apple Silicon.
 
-* No longer support for very old versions of macOS and Linux: base-line
-is Ubuntu Linux 18.04 LTS and macOS 11 Big Sur.
-
 * Isabelle/Scala supports mailing via SMTP, based on new system
 component javamail (previously javax.mail) from jakarta 2.1.2
 using eclipse angus 2.0.2/2.0.1.
diff -r 1f94d92b0dc2 -r a79280c7e8d5 src/Pure/Admin/component_cygwin.scala
--- a/src/Pure/Admin/component_cygwin.scala	Tue Mar 05 16:55:21 2024 +0100
+++ b/src/Pure/Admin/component_cygwin.scala	Tue Mar 05 18:42:09 2024 +0100
@@ -8,7 +8,7 @@
 
 
 object Component_Cygwin {
-  val default_mirror: String = "https://isabelle.sketis.net/cygwin_2023"
+  val default_mirror: String = "https://isabelle.sketis.net/cygwin_2024"
 
   val packages: List[String] = List("curl", "libgmp-devel", "nano", "openssh", "perl")
 
diff -r 1f94d92b0dc2 -r a79280c7e8d5 src/Pure/Build/build_benchmark.scala
--- a/src/Pure/Build/build_benchmark.scala	Tue Mar 05 16:55:21 2024 +0100
+++ b/src/Pure/Build/build_benchmark.scala	Tue Mar 05 18:42:09 2024 +0100
@@ -83,7 +83,7 @@
         val local_build_context = build_context.copy(store = Store(local_options))
 
         val build =
-          Build_Job.start_session(local_build_context, session, progress, No_Logger, server,
+          Build_Job.start_session(local_build_context, session, progress, new Logger, server,
             background, session.sources_shasum, input_shasum, node_info, false)
 
         val timing =
diff -r 1f94d92b0dc2 -r a79280c7e8d5 src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Tue Mar 05 16:55:21 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Tue Mar 05 18:42:09 2024 +0100
@@ -43,7 +43,6 @@
   sealed case class Task(
     name: String,
     deps: List[String],
-    info: JSON.Object.T,
     build_uuid: String
   ) {
     def is_ready: Boolean = deps.isEmpty
@@ -566,10 +565,9 @@
     object Pending {
       val name = Generic.name.make_primary_key
       val deps = SQL.Column.string("deps")
-      val info = SQL.Column.string("info")
       val build_uuid = Generic.build_uuid
 
-      val table = make_table(List(name, deps, info, build_uuid), name = "pending")
+      val table = make_table(List(name, deps, build_uuid), name = "pending")
     }
 
     def read_pending(db: SQL.Database): List[Task] =
@@ -579,9 +577,8 @@
         { res =>
           val name = res.string(Pending.name)
           val deps = res.string(Pending.deps)
-          val info = res.string(Pending.info)
           val build_uuid = res.string(Pending.build_uuid)
-          Task(name, split_lines(deps), JSON.Object.parse(info), build_uuid)
+          Task(name, split_lines(deps), build_uuid)
         })
 
     def update_pending(
@@ -601,8 +598,7 @@
           for (task <- insert) yield { (stmt: SQL.Statement) =>
             stmt.string(1) = task.name
             stmt.string(2) = cat_lines(task.deps)
-            stmt.string(3) = JSON.Format(task.info)
-            stmt.string(4) = task.build_uuid
+            stmt.string(3) = task.build_uuid
           })
       }
 
@@ -978,7 +974,7 @@
     val new_pending =
       List.from(
         for (session <- sessions1.iterator if !old_pending(session.name))
-          yield Build_Process.Task(session.name, session.deps, JSON.Object.empty, build_uuid))
+          yield Build_Process.Task(session.name, session.deps, build_uuid))
     val pending1 = new_pending ::: state.pending
 
     state.copy(sessions = sessions1, pending = pending1)
diff -r 1f94d92b0dc2 -r a79280c7e8d5 src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Tue Mar 05 16:55:21 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Tue Mar 05 18:42:09 2024 +0100
@@ -1328,7 +1328,7 @@
 
       val sessions = Build_Process.Sessions.empty.init(build_context, database_server, progress)
       def task(session: Build_Job.Session_Context): Build_Process.Task =
-        Build_Process.Task(session.name, session.deps, JSON.Object.empty, build_context.build_uuid)
+        Build_Process.Task(session.name, session.deps, build_context.build_uuid)
 
       val build_state =
         Build_Process.State(sessions = sessions, pending = sessions.iterator.map(task).toList)
diff -r 1f94d92b0dc2 -r a79280c7e8d5 src/Pure/Build/resources.scala
--- a/src/Pure/Build/resources.scala	Tue Mar 05 16:55:21 2024 +0100
+++ b/src/Pure/Build/resources.scala	Tue Mar 05 18:42:09 2024 +0100
@@ -24,7 +24,7 @@
 
 class Resources(
   val session_background: Sessions.Background,
-  val log: Logger = No_Logger,
+  val log: Logger = new Logger,
   command_timings: List[Properties.T] = Nil
 ) {
   resources =>
diff -r 1f94d92b0dc2 -r a79280c7e8d5 src/Pure/Concurrent/delay.scala
--- a/src/Pure/Concurrent/delay.scala	Tue Mar 05 16:55:21 2024 +0100
+++ b/src/Pure/Concurrent/delay.scala	Tue Mar 05 18:42:09 2024 +0100
@@ -9,11 +9,11 @@
 
 object Delay {
   // delayed event after first invocation
-  def first(delay: => Time, log: Logger = No_Logger, gui: Boolean = false)(event: => Unit): Delay =
+  def first(delay: => Time, log: Logger = new Logger, gui: Boolean = false)(event: => Unit): Delay =
     new Delay(true, delay, log, if (gui) GUI_Thread.later { event } else event )
 
   // delayed event after last invocation
-  def last(delay: => Time, log: Logger = No_Logger, gui: Boolean = false)(event: => Unit): Delay =
+  def last(delay: => Time, log: Logger = new Logger, gui: Boolean = false)(event: => Unit): Delay =
     new Delay(false, delay, log, if (gui) GUI_Thread.later { event } else event )
 }
 
diff -r 1f94d92b0dc2 -r a79280c7e8d5 src/Pure/General/logger.scala
--- a/src/Pure/General/logger.scala	Tue Mar 05 16:55:21 2024 +0100
+++ b/src/Pure/General/logger.scala	Tue Mar 05 18:42:09 2024 +0100
@@ -8,42 +8,59 @@
 
 
 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(progress: Progress): Logger =
-    new Logger { def apply(msg: => String): Unit = if (progress != null) progress.echo(msg) }
+  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 => new Logger
+    }
 
-  def make_system_log(progress: Progress, options: Options): Logger =
+  def make_progress(progress: => Progress, guard_time: Time = Time.min): Logger = {
+    val t = guard_time
+    new Logger {
+      override val guard_time: Time = t
+      override def output(msg: => String): Unit =
+        if (progress != null) progress.echo(msg)
+    }
+  }
+
+  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 "" => new Logger
+      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
+class Logger {
+  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 = {}
-}
-
-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 {
-    if (Platform.is_windows) System.out.println(msg)
-    else System.console.writer.println(msg)
+class System_Logger(override val guard_time: Time = Time.min)
+extends Logger {
+  override def output(msg: => String): Unit = synchronized {
+    if (System.console != null && System.console.writer != null) {
+      System.console.writer.println(msg)
+      System.console.writer.flush()
+    }
+    else if (System.out != null) {
+      System.out.println(msg)
+      System.out.flush()
+    }
   }
 }
diff -r 1f94d92b0dc2 -r a79280c7e8d5 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Tue Mar 05 16:55:21 2024 +0100
+++ b/src/Pure/General/sql.scala	Tue Mar 05 18:42:09 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 1f94d92b0dc2 -r a79280c7e8d5 src/Pure/General/time.scala
--- a/src/Pure/General/time.scala	Tue Mar 05 16:55:21 2024 +0100
+++ b/src/Pure/General/time.scala	Tue Mar 05 18:42:09 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 1f94d92b0dc2 -r a79280c7e8d5 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Tue Mar 05 16:55:21 2024 +0100
+++ b/src/Pure/PIDE/headless.scala	Tue Mar 05 18:42:09 2024 +0100
@@ -448,7 +448,7 @@
     def apply(
       options: Options,
       session_background: Sessions.Background,
-      log: Logger = No_Logger
+      log: Logger = new Logger
     ): Resources = new Resources(options, session_background, log = log)
 
     def make(
@@ -457,7 +457,7 @@
       session_dirs: List[Path] = Nil,
       include_sessions: List[String] = Nil,
       progress: Progress = new Progress,
-      log: Logger = No_Logger
+      log: Logger = new Logger
     ): Resources = {
       val session_background =
         Sessions.background(options, session_name, dirs = session_dirs,
@@ -605,7 +605,7 @@
   class Resources private[Headless](
     val options: Options,
     session_background: Sessions.Background,
-    log: Logger = No_Logger)
+    log: Logger = new Logger)
   extends isabelle.Resources(session_background.check_errors, log = log) {
     resources =>
 
diff -r 1f94d92b0dc2 -r a79280c7e8d5 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Tue Mar 05 16:55:21 2024 +0100
+++ b/src/Pure/Tools/dump.scala	Tue Mar 05 18:42:09 2024 +0100
@@ -142,7 +142,7 @@
 
     def sessions(
       logic: String = default_logic,
-      log: Logger = No_Logger
+      log: Logger = new Logger
     ): List[Session] = {
       /* partitions */
 
@@ -359,7 +359,7 @@
     logic: String,
     aspects: List[Aspect] = Nil,
     progress: Progress = new Progress,
-    log: Logger = No_Logger,
+    log: Logger = new Logger,
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
     output_dir: Path = default_output_dir,
diff -r 1f94d92b0dc2 -r a79280c7e8d5 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Tue Mar 05 16:55:21 2024 +0100
+++ b/src/Pure/Tools/server.scala	Tue Mar 05 18:42:09 2024 +0100
@@ -397,7 +397,7 @@
     name: String = default_name,
     port: Int = 0,
     existing_server: Boolean = false,
-    log: Logger = No_Logger
+    log: Logger = new Logger
   ): (Info, Option[Server]) = {
     using(SQLite.open_database(private_data.database, restrict = true)) { db =>
       private_data.transaction_lock(db, create = true) {
@@ -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 1f94d92b0dc2 -r a79280c7e8d5 src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Tue Mar 05 16:55:21 2024 +0100
+++ b/src/Pure/Tools/server_commands.scala	Tue Mar 05 18:42:09 2024 +0100
@@ -123,7 +123,7 @@
     def command(
       args: Args,
       progress: Progress = new Progress,
-      log: Logger = No_Logger
+      log: Logger = new Logger
     ) : (JSON.Object.T, (UUID.T, Headless.Session)) = {
       val (_, _, options, session_background) =
         try { Session_Build.command(args.build, progress = progress) }
diff -r 1f94d92b0dc2 -r a79280c7e8d5 src/Tools/VSCode/src/channel.scala
--- a/src/Tools/VSCode/src/channel.scala	Tue Mar 05 16:55:21 2024 +0100
+++ b/src/Tools/VSCode/src/channel.scala	Tue Mar 05 18:42:09 2024 +0100
@@ -17,7 +17,7 @@
 class Channel(
   in: InputStream,
   out: OutputStream,
-  log: Logger = No_Logger,
+  log: Logger = new Logger,
   verbose: Boolean = false
 ) {
   /* read message */
diff -r 1f94d92b0dc2 -r a79280c7e8d5 src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Tue Mar 05 16:55:21 2024 +0100
+++ b/src/Tools/VSCode/src/language_server.scala	Tue Mar 05 18:42:09 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,
@@ -91,7 +91,7 @@
         }
         catch {
           case exn: Throwable =>
-            val channel = new Channel(System.in, System.out, No_Logger)
+            val channel = new Channel(System.in, System.out, new Logger)
             channel.error_message(Exn.message(exn))
             throw(exn)
         }
@@ -108,7 +108,7 @@
   session_requirements: Boolean = false,
   session_no_build: Boolean = false,
   modes: List[String] = Nil,
-  log: Logger = No_Logger
+  log: Logger = new Logger
 ) {
   server =>
 
diff -r 1f94d92b0dc2 -r a79280c7e8d5 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Tue Mar 05 16:55:21 2024 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Tue Mar 05 18:42:09 2024 +0100
@@ -70,7 +70,7 @@
 class VSCode_Resources(
   val options: Options,
   session_background: Sessions.Background,
-  log: Logger = No_Logger)
+  log: Logger = new Logger)
 extends Resources(session_background, log = log) {
   resources =>