# HG changeset patch
# User wenzelm
# Date 1489774451 -3600
# Node ID 6c1d7d5c2165cf2bba532df21769e956f0f2deec
# Parent  86d93effc3df6e9cb5c76efc07e30b867910a3bf
tuned;

diff -r 86d93effc3df -r 6c1d7d5c2165 src/Pure/Admin/build_log.scala
--- 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)
   }
 }