# HG changeset patch
# User wenzelm
# Date 1698922660 -3600
# Node ID 4222955f3b6967657728aa6148096b1c50d5b486
# Parent  b7d355b2b176898d251f2cd1df307db7668ec9d1
clarified signature: explicit Progress date;

diff -r b7d355b2b176 -r 4222955f3b69 src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Thu Nov 02 10:29:24 2023 +0100
+++ b/src/Pure/System/progress.scala	Thu Nov 02 11:57:40 2023 +0100
@@ -182,6 +182,9 @@
 }
 
 class Progress {
+  def now(): Date = Date.now()
+  val start: Date = now()
+
   def verbose: Boolean = false
   final def do_output(message: Progress.Message): Boolean = !message.verbose || verbose
 
@@ -276,6 +279,9 @@
 extends Progress {
   database_progress =>
 
+  override def now(): Date = db.now()
+  override val start: Date = now()
+
   if (UUID.unapply(context_uuid).isEmpty) {
     error("Bad Database_Progress.context_uuid: " + quote(context_uuid))
   }
@@ -307,7 +313,6 @@
         val java = ProcessHandle.current()
         val java_pid = java.pid
         val java_start = Date.instant(java.info.startInstant.get)
-        val now = db.now()
 
         stmt.string(1) = _agent_uuid
         stmt.string(2) = context_uuid
@@ -315,8 +320,8 @@
         stmt.string(4) = hostname
         stmt.long(5) = java_pid
         stmt.date(6) = java_start
-        stmt.date(7) = now
-        stmt.date(8) = now
+        stmt.date(7) = start
+        stmt.date(8) = start
         stmt.date(9) = None
         stmt.long(10) = 0L
       })