# HG changeset patch
# User wenzelm
# Date 1709899501 -3600
# Node ID 4b23abde5d0b1d3082557d9b71dc9d02235fdca8
# Parent  80a30835f48f4be4e765f0e0ab5466fdefbde6c9
more accurate progress.now(), notably for Database_Progress;

diff -r 80a30835f48f -r 4b23abde5d0b src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Fri Mar 08 11:09:44 2024 +0100
+++ b/src/Pure/Admin/build_history.scala	Fri Mar 08 13:05:01 2024 +0100
@@ -184,7 +184,7 @@
         clean_archives = clean_archives)
 
     val build_host = proper_string(hostname) getOrElse Isabelle_System.hostname()
-    val build_history_date = Date.now()
+    val build_history_date = progress.now()
     val build_group_id = build_host + ":" + build_history_date.time.ms
 
     var first_build = true
@@ -246,7 +246,7 @@
         Isabelle_System.copy_dir(isabelle_base_log, isabelle_output_log)
       }
 
-      val build_start = Date.now()
+      val build_start = progress.now()
       val build_args1 = List("-v", "-j" + processes) ::: afp_build_args ::: build_args
 
       val build_result =
@@ -255,7 +255,7 @@
         .bash("bin/isabelle build " + Bash.strings(build_args1),
           redirect = true, echo = true, strict = false)
 
-      val build_end = Date.now()
+      val build_end = progress.now()
 
       val store = Store(options + "build_database_server=false")
 
diff -r 80a30835f48f -r 4b23abde5d0b src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Fri Mar 08 11:09:44 2024 +0100
+++ b/src/Pure/Build/build.scala	Fri Mar 08 13:05:01 2024 +0100
@@ -443,7 +443,7 @@
             export_files = export_files,
             build_hosts = build_hosts.toList)
         }
-      val stop_date = Date.now()
+      val stop_date = progress.now()
       val elapsed_time = stop_date.time - progress.start.time
 
       progress.echo("\nFinished at " + Build_Log.print_date(stop_date), verbose = true)
diff -r 80a30835f48f -r 4b23abde5d0b src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Fri Mar 08 11:09:44 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Fri Mar 08 13:05:01 2024 +0100
@@ -1066,7 +1066,8 @@
           build_deps.background(session_name), sources_shasum, input_shasum, node_info, store_heap)
 
       val job =
-        Build_Process.Job(session_name, worker_uuid, build_uuid, node_info, Date.now(), Some(build))
+        Build_Process.Job(
+          session_name, worker_uuid, build_uuid, node_info, progress.now(), Some(build))
 
       state.add_running(job)
     }