# HG changeset patch
# User wenzelm
# Date 1475841490 -7200
# Node ID d57c7295f60184d4a0726c589eabf4c2cedea1f3
# Parent  38bb09ed965b6ce70443d6419c0569c7c9feb321
clarified signature;

diff -r 38bb09ed965b -r d57c7295f601 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Oct 07 11:45:30 2016 +0200
+++ b/src/Pure/Tools/build.scala	Fri Oct 07 13:58:10 2016 +0200
@@ -477,7 +477,7 @@
       }
 
       try {
-        val info = Build_Log.Log_File(name, text).parse_session_info(name, false)
+        val info = Build_Log.Log_File(name, text).parse_session_info(name, command_timings = true)
         val session_timing = Markup.Elapsed.unapply(info.session_timing) getOrElse 0.0
         (info.command_timings, session_timing)
       }
diff -r 38bb09ed965b -r d57c7295f601 src/Pure/Tools/build_log.scala
--- a/src/Pure/Tools/build_log.scala	Fri Oct 07 11:45:30 2016 +0200
+++ b/src/Pure/Tools/build_log.scala	Fri Oct 07 13:58:10 2016 +0200
@@ -108,8 +108,13 @@
 
     /* parse various formats */
 
-    def parse_session_info(session_name: String, full: Boolean): Session_Info =
-      Build_Log.parse_session_info(log_file, session_name, full)
+    def parse_session_info(
+        session_name: String,
+        command_timings: Boolean = false,
+        ml_statistics: Boolean = false,
+        task_statistics: Boolean = false): Session_Info =
+      Build_Log.parse_session_info(
+        log_file, session_name, command_timings, ml_statistics, task_statistics)
 
     def parse_header: Header = Build_Log.parse_header(log_file)
 
@@ -126,22 +131,30 @@
     ml_statistics: List[Properties.T],
     task_statistics: List[Properties.T])
 
-  private def parse_session_info(log_file: Log_File, name0: String, full: Boolean): Session_Info =
+  private def parse_session_info(
+    log_file: Log_File,
+    default_name: String,
+    command_timings: Boolean,
+    ml_statistics: Boolean,
+    task_statistics: Boolean): Session_Info =
   {
     val xml_cache = new XML.Cache()
 
     val session_name =
       log_file.find_line("\fSession.name = ") match {
-        case None => name0
-        case Some(name) if name0 == "" || name0 == name => name
+        case None => default_name
+        case Some(name) if default_name == "" || default_name == name => name
         case Some(name) => log_file.err("log from different session " + quote(name))
       }
     val session_timing = log_file.find_props("\fTiming = ") getOrElse Nil
-    val command_timings = log_file.filter_props("\fcommand_timing = ")
-    val ml_statistics = if (full) log_file.filter_props("\fML_statistics = ") else Nil
-    val task_statistics = if (full) log_file.filter_props("\ftask_statistics = ") else Nil
+    val command_timings_ =
+      if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil
+    val ml_statistics_ =
+      if (ml_statistics) log_file.filter_props("\fML_statistics = ") else Nil
+    val task_statistics_ =
+      if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil
 
-    Session_Info(session_name, session_timing, command_timings, ml_statistics, task_statistics)
+    Session_Info(session_name, session_timing, command_timings_, ml_statistics_, task_statistics_)
   }
 
 
diff -r 38bb09ed965b -r d57c7295f601 src/Pure/Tools/ci_api.scala
--- a/src/Pure/Tools/ci_api.scala	Fri Oct 07 11:45:30 2016 +0200
+++ b/src/Pure/Tools/ci_api.scala	Fri Oct 07 13:58:10 2016 +0200
@@ -45,12 +45,9 @@
     session_logs: List[(String, URL)])
   {
     def read_output(): Build_Log.Log_File = Build_Log.Log_File(job_name, Url.read(output))
-    def read_log(name: String, full: Boolean): Build_Log.Session_Info =
-    {
-      val text =
-        session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse ""
-      Build_Log.Log_File(name, text).parse_session_info(name, full)
-    }
+    def read_log_file(name: String): Build_Log.Log_File =
+      Build_Log.Log_File(name,
+        session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "")
   }
 
   def build_job_builds(job_name: String): List[Job_Info] =