tuned;

--- a/src/Pure/Admin/build_log.scala	Fri Mar 17 11:35:03 2017 +0100
+++ b/src/Pure/Admin/build_log.scala	Fri Mar 17 19:14:11 2017 +0100
@@ -555,22 +555,16 @@
     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 => 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_ =
-      if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil
-    val ml_statistics_ =
-      if (ml_statistics) log_file.filter_props(ML_STATISTICS_MARKER) 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 =
+        log_file.find_line("\fSession.name = ") match {
+          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))
+        },
+      session_timing = log_file.find_props("\fTiming = ") getOrElse Nil,
+      command_timings = if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil,
+      ml_statistics = if (ml_statistics) log_file.filter_props(ML_STATISTICS_MARKER) else Nil,
+      task_statistics = if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil)
   }
 }