# HG changeset patch
# User wenzelm
# Date 1676113782 -3600
# Node ID b9bf4c0bd47d4df6021d49ef00791739f2999fc9
# Parent  02308a0ddf30327faba346833c41870a711f9553
clarified signature: more explicit types;

diff -r 02308a0ddf30 -r b9bf4c0bd47d src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Feb 11 11:42:13 2023 +0100
+++ b/src/Pure/Tools/build.scala	Sat Feb 11 12:09:42 2023 +0100
@@ -59,13 +59,12 @@
       val graph = sessions_structure.build_graph
       val names = graph.keys
 
-      val timings =
-        names.map(name => (name, Build_Process.Session_Timing.load(progress, store, name)))
+      val timings = names.map(Build_Process.Session_Timing.load(_, store, progress = progress))
       val command_timings =
-        timings.map({ case (name, (ts, _)) => (name, ts) }).toMap.withDefaultValue(Nil)
+        timings.map(timing => timing.session -> timing.command_timings).toMap.withDefaultValue(Nil)
       val session_timing =
         make_session_timing(sessions_structure,
-          timings.map({ case (name, (_, t)) => (name, t) }).toMap)
+          timings.map(timing => timing.session -> timing.elapsed.seconds).toMap)
 
       object Ordering extends scala.math.Ordering[String] {
         def compare(name1: String, name2: String): Int =
diff -r 02308a0ddf30 -r b9bf4c0bd47d src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Sat Feb 11 11:42:13 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Sat Feb 11 12:09:42 2023 +0100
@@ -11,28 +11,30 @@
 object Build_Process {
   /* timings from session database */
 
-  type Session_Timing = (List[Properties.T], Double)
+  object Session_Timing {
+    def empty(session: String): Session_Timing = new Session_Timing(session, Time.zero, Nil)
 
-  object Session_Timing {
-    val empty: Session_Timing = (Nil, 0.0)
-
-    def load(progress: Progress, store: Sessions.Store, session_name: String): Session_Timing = {
-      store.try_open_database(session_name) match {
-        case None => empty
+    def load(
+      session: String,
+      store: Sessions.Store,
+      progress: Progress = new Progress
+    ): Session_Timing = {
+      store.try_open_database(session) match {
+        case None => empty(session)
         case Some(db) =>
           def ignore_error(msg: String) = {
             progress.echo_warning("Ignoring bad database " + db +
-              " for session " + quote(session_name) + (if (msg == "") "" else ":\n" + msg))
-            empty
+              " for session " + quote(session) + (if (msg == "") "" else ":\n" + msg))
+            empty(session)
           }
           try {
-            val command_timings = store.read_command_timings(db, session_name)
-            val session_timing =
-              store.read_session_timing(db, session_name) match {
-                case Markup.Elapsed(t) => t
-                case _ => 0.0
+            val command_timings = store.read_command_timings(db, session)
+            val elapsed =
+              store.read_session_timing(db, session) match {
+                case Markup.Elapsed(s) => Time.seconds(s)
+                case _ => Time.zero
               }
-            (command_timings, session_timing)
+            new Session_Timing(session, elapsed, command_timings)
           }
           catch {
             case ERROR(msg) => ignore_error(msg)
@@ -43,4 +45,13 @@
       }
     }
   }
+
+  final class Session_Timing(
+    val session: String,
+    val elapsed: Time,
+    val command_timings: List[Properties.T]
+  ) {
+    override def toString: String =
+      session + (if (elapsed.is_relevant) " (" + elapsed.message_hms + " elapsed time)" else "")
+  }
 }