# 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 "") + } }