# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1467707183 -7200
# Node ID 3395fe5e38939c6f7915225dd6005dd81d578dd3
# Parent  0d6adf2d5035be8c2cc5d8ce624769cc32d0fa73
more accurate total timing

diff -r 0d6adf2d5035 -r 3395fe5e3893 src/Pure/Tools/ci_profile.scala
--- a/src/Pure/Tools/ci_profile.scala	Tue Jul 05 09:50:20 2016 +0200
+++ b/src/Pure/Tools/ci_profile.scala	Tue Jul 05 10:26:23 2016 +0200
@@ -19,10 +19,11 @@
     println(name + "=" + Outer_Syntax.quote_string(value))
   }
 
-  private def build(options: Options): Build.Results =
+  private def build(options: Options): (Build.Results, Time) =
   {
     val progress = new Console_Progress(true)
-    progress.interrupt_handler {
+    val start_time = Time.now()
+    val results = progress.interrupt_handler {
       Build.build_selection(
         options = options,
         progress = progress,
@@ -34,6 +35,8 @@
         system_mode = true,
         selection = select_sessions _)
     }
+    val end_time = Time.now()
+    (results, end_time - start_time)
   }
 
   private def load_properties(): JProperties =
@@ -85,14 +88,16 @@
     println(s"Build for Isabelle id $isabelle_id")
     pre_hook(args)
 
-    val results = build(options)
+    val (results, elapsed_time) = build(options)
 
     print_section("TIMING")
 
     val groups = results.sessions.map(results.info).flatMap(_.groups)
     for (group <- groups)
       println(s"Group $group: " + compute_timing(results, Some(group)).message_resources)
-    println("Overall: " + compute_timing(results, None).message_resources)
+
+    val total_timing = compute_timing(results, None).copy(elapsed = elapsed_time)
+    println("Overall: " + total_timing.message_resources)
 
     if (!results.ok) {
       print_section("FAILED SESSIONS")