# HG changeset patch
# User wenzelm
# Date 1594478515 -7200
# Node ID 5c9984820caa313acaafe5f497fea01aa4427bcd
# Parent  17a41deb595040610bf4c2ff499fde365395bd3a
clarified signature;

diff -r 17a41deb5950 -r 5c9984820caa src/Pure/Admin/build_history.scala
--- 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 {
diff -r 17a41deb5950 -r 5c9984820caa src/Pure/Tools/build.scala
--- 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,