# HG changeset patch
# User wenzelm
# Date 1594475475 -7200
# Node ID 6a24ecc4ff1b740db535e87ac3ed656685364b3d
# Parent  c81e58a81b8c68428d3fce58c7efd806269728c4
clarified signature;

diff -r c81e58a81b8c -r 6a24ecc4ff1b src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sat Jul 11 15:23:22 2020 +0200
+++ b/src/Pure/Admin/build_history.scala	Sat Jul 11 15:51:15 2020 +0200
@@ -287,9 +287,9 @@
                 val session_timing =
                 {
                   val props = store.read_session_timing(db, session_name)
-                  val threads = Markup.Session_Timing.Threads.unapply(props) getOrElse "1"
-                  val timing = Markup.Timing_Properties.unapply(props) getOrElse Timing.zero
-                  "Timing " + session_name + " (" + threads + " threads, " + timing.message_resources + ")"
+                  Build.session_timing(session_name,
+                    Markup.Session_Timing.Threads.unapply(props) getOrElse 1,
+                    Markup.Timing_Properties.parse(props))
                 }
 
                 val theory_timings =
diff -r c81e58a81b8c -r 6a24ecc4ff1b src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Sat Jul 11 15:23:22 2020 +0200
+++ b/src/Pure/PIDE/markup.scala	Sat Jul 11 15:51:15 2020 +0200
@@ -402,6 +402,9 @@
           Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
         case _ => None
       }
+
+    def parse(props: Properties.T): isabelle.Timing =
+      unapply(props) getOrElse isabelle.Timing.zero
   }
 
   val TIMING = "timing"
@@ -577,7 +580,7 @@
   object Theory_Timing extends Properties_Function("theory_timing")
   object Session_Timing extends Properties_Function("session_timing")
   {
-    val Threads = new Properties.String("threads")
+    val Threads = new Properties.Int("threads")
   }
   object ML_Statistics extends Properties_Function("ML_statistics")
   object Task_Statistics extends Properties_Function("task_statistics")
diff -r c81e58a81b8c -r 6a24ecc4ff1b src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Jul 11 15:23:22 2020 +0200
+++ b/src/Pure/Tools/build.scala	Sat Jul 11 15:51:15 2020 +0200
@@ -489,6 +489,12 @@
     override def toString: String = rc.toString
   }
 
+  def session_finished(session_name: String, timing: Timing): String =
+    "Finished " + session_name + " (" + timing.message_resources + ")"
+
+  def session_timing(session_name: String, threads: Int, timing: Timing): String =
+    "Timing " + session_name + " (" + threads + " threads, " + timing.message_resources + ")"
+
   def build(
     options: Options,
     selection: Sessions.Selection = Sessions.Selection.empty,
@@ -678,9 +684,9 @@
             // messages
             process_result.err_lines.foreach(progress.echo)
 
-            if (process_result.ok)
-              progress.echo(
-                "Finished " + session_name + " (" + process_result.timing.message_resources + ")")
+            if (process_result.ok) {
+              progress.echo(session_finished(session_name, process_result.timing))
+            }
             else {
               progress.echo(session_name + " FAILED")
               if (!process_result.interrupted) progress.echo(process_result_tail.out)