--- a/src/Pure/Admin/build_history.scala Sat Jul 11 16:37:32 2020 +0200
+++ b/src/Pure/Admin/build_history.scala Sat Jul 11 16:41:55 2020 +0200
@@ -292,12 +292,7 @@
catch { case ERROR(_) => Nil }
val session_timing =
- {
- val props = store.read_session_timing(db, session_name)
- Build.session_timing(session_name,
- Markup.Session_Timing.Threads.unapply(props) getOrElse 1,
- Markup.Timing_Properties.parse(props))
- }
+ Build.session_timing(session_name, store.read_session_timing(db, session_name))
val session_sources =
store.read_build(db, session_name).map(_.sources) match {
--- a/src/Pure/Tools/build.scala Sat Jul 11 16:37:32 2020 +0200
+++ b/src/Pure/Tools/build.scala Sat Jul 11 16:41:55 2020 +0200
@@ -490,6 +490,11 @@
def session_timing(session_name: String, threads: Int, timing: Timing): String =
"Timing " + session_name + " (" + threads + " threads, " + timing.message_factor + ")"
+ def session_timing(session_name: String, props: Properties.T): String =
+ session_timing(session_name,
+ Markup.Session_Timing.Threads.unapply(props) getOrElse 1,
+ Markup.Timing_Properties.parse(props))
+
def build(
options: Options,
selection: Sessions.Selection = Sessions.Selection.empty,