# HG changeset patch
# User wenzelm
# Date 1594479518 -7200
# Node ID 940195fbb2823e5c309de323e99374a09a6f81dc
# Parent  5c9984820caa313acaafe5f497fea01aa4427bcd
clarified messages;

diff -r 5c9984820caa -r 940195fbb282 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Sat Jul 11 16:41:55 2020 +0200
+++ b/src/Pure/Tools/build.ML	Sat Jul 11 16:58:38 2020 +0200
@@ -46,23 +46,15 @@
 
 (* session timing *)
 
-fun session_timing session_name verbose f x =
+fun session_timing f x =
   let
     val start = Timing.start ();
     val y = f x;
     val timing = Timing.result start;
 
     val threads = string_of_int (Multithreading.max_threads ());
-    val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
-      |> Real.fmt (StringCvt.FIX (SOME 2));
-
-    val timing_props = [("threads", threads)] @ Markup.timing_properties timing;
-    val _ = Output.protocol_message (Markup.session_timing :: timing_props) [];
-    val _ =
-      if verbose then
-        Output.physical_stderr ("Timing " ^ session_name ^ " (" ^
-          threads ^ " threads, " ^ Timing.message timing ^ ", factor " ^ factor ^ ")\n")
-      else ();
+    val props = [("threads", threads)] @ Markup.timing_properties timing;
+    val _ = Output.protocol_message (Markup.session_timing :: props) [];
   in y end;
 
 
@@ -211,7 +203,7 @@
     val res1 =
       theories |>
         (List.app (build_theories symbols bibtex_entries last_timing session_name master_dir)
-          |> session_timing session_name verbose
+          |> session_timing
           |> Exn.capture);
     val res2 = Exn.capture Session.finish ();
 
diff -r 5c9984820caa -r 940195fbb282 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Jul 11 16:41:55 2020 +0200
+++ b/src/Pure/Tools/build.scala	Sat Jul 11 16:58:38 2020 +0200
@@ -681,6 +681,8 @@
             // messages
             process_result.err_lines.foreach(progress.echo)
 
+            if (verbose) progress.echo(session_timing(session_name, build_log.session_timing))
+
             if (process_result.ok) {
               progress.echo(session_finished(session_name, process_result.timing))
             }