clarified signature;
authorwenzelm
Sat, 11 Jul 2020 16:41:55 +0200
changeset 72248 5c9984820caa
parent 72247 17a41deb5950
child 72249 940195fbb282
clarified signature;
src/Pure/Admin/build_history.scala
src/Pure/Tools/build.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 {
--- 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,