src/Pure/Tools/build_log.scala
changeset 64082 d57c7295f601
parent 64081 38bb09ed965b
child 64083 fef1a0a59c12
     1.1 --- a/src/Pure/Tools/build_log.scala	Fri Oct 07 11:45:30 2016 +0200
     1.2 +++ b/src/Pure/Tools/build_log.scala	Fri Oct 07 13:58:10 2016 +0200
     1.3 @@ -108,8 +108,13 @@
     1.4  
     1.5      /* parse various formats */
     1.6  
     1.7 -    def parse_session_info(session_name: String, full: Boolean): Session_Info =
     1.8 -      Build_Log.parse_session_info(log_file, session_name, full)
     1.9 +    def parse_session_info(
    1.10 +        session_name: String,
    1.11 +        command_timings: Boolean = false,
    1.12 +        ml_statistics: Boolean = false,
    1.13 +        task_statistics: Boolean = false): Session_Info =
    1.14 +      Build_Log.parse_session_info(
    1.15 +        log_file, session_name, command_timings, ml_statistics, task_statistics)
    1.16  
    1.17      def parse_header: Header = Build_Log.parse_header(log_file)
    1.18  
    1.19 @@ -126,22 +131,30 @@
    1.20      ml_statistics: List[Properties.T],
    1.21      task_statistics: List[Properties.T])
    1.22  
    1.23 -  private def parse_session_info(log_file: Log_File, name0: String, full: Boolean): Session_Info =
    1.24 +  private def parse_session_info(
    1.25 +    log_file: Log_File,
    1.26 +    default_name: String,
    1.27 +    command_timings: Boolean,
    1.28 +    ml_statistics: Boolean,
    1.29 +    task_statistics: Boolean): Session_Info =
    1.30    {
    1.31      val xml_cache = new XML.Cache()
    1.32  
    1.33      val session_name =
    1.34        log_file.find_line("\fSession.name = ") match {
    1.35 -        case None => name0
    1.36 -        case Some(name) if name0 == "" || name0 == name => name
    1.37 +        case None => default_name
    1.38 +        case Some(name) if default_name == "" || default_name == name => name
    1.39          case Some(name) => log_file.err("log from different session " + quote(name))
    1.40        }
    1.41      val session_timing = log_file.find_props("\fTiming = ") getOrElse Nil
    1.42 -    val command_timings = log_file.filter_props("\fcommand_timing = ")
    1.43 -    val ml_statistics = if (full) log_file.filter_props("\fML_statistics = ") else Nil
    1.44 -    val task_statistics = if (full) log_file.filter_props("\ftask_statistics = ") else Nil
    1.45 +    val command_timings_ =
    1.46 +      if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil
    1.47 +    val ml_statistics_ =
    1.48 +      if (ml_statistics) log_file.filter_props("\fML_statistics = ") else Nil
    1.49 +    val task_statistics_ =
    1.50 +      if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil
    1.51  
    1.52 -    Session_Info(session_name, session_timing, command_timings, ml_statistics, task_statistics)
    1.53 +    Session_Info(session_name, session_timing, command_timings_, ml_statistics_, task_statistics_)
    1.54    }
    1.55  
    1.56