src/Pure/Admin/build_log.scala
changeset 65290 6c1d7d5c2165
parent 65276 fa1a5efee2ec
child 65318 342efc382558
     1.1 --- a/src/Pure/Admin/build_log.scala	Fri Mar 17 11:35:03 2017 +0100
     1.2 +++ b/src/Pure/Admin/build_log.scala	Fri Mar 17 19:14:11 2017 +0100
     1.3 @@ -555,22 +555,16 @@
     1.4      ml_statistics: Boolean,
     1.5      task_statistics: Boolean): Session_Info =
     1.6    {
     1.7 -    val xml_cache = new XML.Cache()
     1.8 -
     1.9 -    val session_name =
    1.10 -      log_file.find_line("\fSession.name = ") match {
    1.11 -        case None => default_name
    1.12 -        case Some(name) if default_name == "" || default_name == name => name
    1.13 -        case Some(name) => log_file.err("log from different session " + quote(name))
    1.14 -      }
    1.15 -    val session_timing = log_file.find_props("\fTiming = ") getOrElse Nil
    1.16 -    val command_timings_ =
    1.17 -      if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil
    1.18 -    val ml_statistics_ =
    1.19 -      if (ml_statistics) log_file.filter_props(ML_STATISTICS_MARKER) else Nil
    1.20 -    val task_statistics_ =
    1.21 -      if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil
    1.22 -
    1.23 -    Session_Info(session_name, session_timing, command_timings_, ml_statistics_, task_statistics_)
    1.24 +    Session_Info(
    1.25 +      session_name =
    1.26 +        log_file.find_line("\fSession.name = ") match {
    1.27 +          case None => default_name
    1.28 +          case Some(name) if default_name == "" || default_name == name => name
    1.29 +          case Some(name) => log_file.err("log from different session " + quote(name))
    1.30 +        },
    1.31 +      session_timing = log_file.find_props("\fTiming = ") getOrElse Nil,
    1.32 +      command_timings = if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil,
    1.33 +      ml_statistics = if (ml_statistics) log_file.filter_props(ML_STATISTICS_MARKER) else Nil,
    1.34 +      task_statistics = if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil)
    1.35    }
    1.36  }