# HG changeset patch
# User wenzelm
# Date 1709926699 -3600
# Node ID 141df3fb25bfe2cb2891b0247b0e325f22b45412
# Parent  0c2a62a9f1361fe3480a966e00d59f41dc9f48c3
tuned;

diff -r 0c2a62a9f136 -r 141df3fb25bf src/HOL/Tools/Mirabelle/mirabelle.scala
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala	Fri Mar 08 20:29:05 2024 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala	Fri Mar 08 20:38:19 2024 +0100
@@ -212,7 +212,7 @@
         }
 
       val end_date = Date.now()
-      val elapsed_time = end_date.time - start_date.time
+      val elapsed_time = end_date - start_date
 
       progress.echo("\nFinished at " + Build_Log.print_date(end_date), verbose = true)
 
diff -r 0c2a62a9f136 -r 141df3fb25bf src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Fri Mar 08 20:29:05 2024 +0100
+++ b/src/Pure/Admin/build_log.scala	Fri Mar 08 20:38:19 2024 +0100
@@ -75,7 +75,7 @@
   def log_date(date: Date): String =
     String.format(Locale.ROOT, "%s.%05d",
       DateTimeFormatter.ofPattern("yyyy-MM-dd").format(date.rep),
-      java.lang.Long.valueOf((date.time - date.midnight.time).ms / 1000))
+      java.lang.Long.valueOf((date - date.midnight).ms / 1000))
 
   def log_subdir(date: Date): Path =
     Path.explode("log") + Path.explode(date.rep.getYear.toString)
diff -r 0c2a62a9f136 -r 141df3fb25bf src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Fri Mar 08 20:29:05 2024 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Fri Mar 08 20:38:19 2024 +0100
@@ -503,7 +503,7 @@
     def log(date: Date, msg: String): Unit = log_service.log(date, task_name, msg)
 
     def log_end(end_date: Date, err: Option[String]): Unit = {
-      val elapsed_time = end_date.time - start_date.time
+      val elapsed_time = end_date - start_date
       val msg =
         (if (err.isEmpty) "finished" else "ERROR " + err.get) +
         (if (elapsed_time.seconds < 3.0) "" else " (" + elapsed_time.message_hms + " elapsed time)")
diff -r 0c2a62a9f136 -r 141df3fb25bf src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Fri Mar 08 20:29:05 2024 +0100
+++ b/src/Pure/Build/build.scala	Fri Mar 08 20:38:19 2024 +0100
@@ -445,7 +445,7 @@
             build_hosts = build_hosts.toList)
         }
       val stop_date = progress.now()
-      val elapsed_time = stop_date.time - progress.start.time
+      val elapsed_time = stop_date - progress.start
 
       progress.echo("\nFinished at " + Build_Log.print_date(stop_date), verbose = true)
 
diff -r 0c2a62a9f136 -r 141df3fb25bf src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Fri Mar 08 20:29:05 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Fri Mar 08 20:38:19 2024 +0100
@@ -1055,7 +1055,7 @@
       val build_log_verbose = build_options.bool("build_log_verbose")
 
       val start = progress.now()
-      val start_time = start.time - build_start.time
+      val start_time = start - build_start
       val start_time_msg = build_log_verbose
 
       val node_info = next_node_info(state, session_name)
diff -r 0c2a62a9f136 -r 141df3fb25bf src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Fri Mar 08 20:29:05 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Fri Mar 08 20:38:19 2024 +0100
@@ -478,10 +478,10 @@
       if (graph.is_empty) start
       else graph.maximals.map(graph.get_node).map(_.end).maxBy(_.unix_epoch)
 
-    def duration: Time = end.time - start.time
+    def duration: Time = end - start
     def message: String = "Estimated " + duration.message_hms + " build time with " + generator
 
-    def deviation(other: Schedule): Time = Time.ms((end.time - other.end.time).ms.abs)
+    def deviation(other: Schedule): Time = Time.ms((end - other.end).ms.abs)
 
     def num_built(state: Build_Process.State): Int = graph.keys.count(state.results.contains)
     def elapsed(): Time = Time.now() - start.time
@@ -507,7 +507,7 @@
 
       def shift_elapsed(graph: Schedule.Graph, name: String): Schedule.Graph =
         graph.map_node(name, { node =>
-          val elapsed = start1.time - state.running(name).start_date.time
+          val elapsed = start1 - state.running(name).start_date
           node.copy(duration = node.duration - elapsed)
         })
 
@@ -1371,7 +1371,7 @@
     val generator_height = line_height + padding
     val hostname_height = generator_height + line_height + padding
     def time_height(time: Time): Double = time.seconds
-    def date_height(date: Date): Double = time_height(date.time - schedule.start.time)
+    def date_height(date: Date): Double = time_height(date - schedule.start)
 
     val hosts = graph.iterator.map(_._2._1).toList.groupBy(_.node_info.hostname)
 
@@ -1474,7 +1474,7 @@
         val duration_str = "(" + node.duration.message_hms + ")"
         val node_str =
           "on " + proper_string(node_info.toString.stripPrefix(node_info.hostname)).getOrElse("all")
-        val start_str = "Start: " + (node.start.time - schedule.start.time).message_hms
+        val start_str = "Start: " + (node.start - schedule.start).message_hms
 
         List(node.job_name, duration_str, node_str, start_str).foldLeft(0D)(add_text)
 
diff -r 0c2a62a9f136 -r 141df3fb25bf src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Fri Mar 08 20:29:05 2024 +0100
+++ b/src/Pure/Tools/dump.scala	Fri Mar 08 20:38:19 2024 +0100
@@ -465,7 +465,7 @@
         }
 
         val end_date = Date.now()
-        val timing = end_date.time - start_date.time
+        val timing = end_date - start_date
 
         progress.echo("\nFinished at " + Build_Log.print_date(end_date), verbose = true)
         progress.echo(timing.message_hms + " elapsed time")