clarified signature;
authorwenzelm
Fri Oct 07 13:58:10 2016 +0200 (2016-10-07)
changeset 64082d57c7295f601
parent 64081 38bb09ed965b
child 64083 fef1a0a59c12
clarified signature;
src/Pure/Tools/build.scala
src/Pure/Tools/build_log.scala
src/Pure/Tools/ci_api.scala
     1.1 --- a/src/Pure/Tools/build.scala	Fri Oct 07 11:45:30 2016 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Fri Oct 07 13:58:10 2016 +0200
     1.3 @@ -477,7 +477,7 @@
     1.4        }
     1.5  
     1.6        try {
     1.7 -        val info = Build_Log.Log_File(name, text).parse_session_info(name, false)
     1.8 +        val info = Build_Log.Log_File(name, text).parse_session_info(name, command_timings = true)
     1.9          val session_timing = Markup.Elapsed.unapply(info.session_timing) getOrElse 0.0
    1.10          (info.command_timings, session_timing)
    1.11        }
     2.1 --- a/src/Pure/Tools/build_log.scala	Fri Oct 07 11:45:30 2016 +0200
     2.2 +++ b/src/Pure/Tools/build_log.scala	Fri Oct 07 13:58:10 2016 +0200
     2.3 @@ -108,8 +108,13 @@
     2.4  
     2.5      /* parse various formats */
     2.6  
     2.7 -    def parse_session_info(session_name: String, full: Boolean): Session_Info =
     2.8 -      Build_Log.parse_session_info(log_file, session_name, full)
     2.9 +    def parse_session_info(
    2.10 +        session_name: String,
    2.11 +        command_timings: Boolean = false,
    2.12 +        ml_statistics: Boolean = false,
    2.13 +        task_statistics: Boolean = false): Session_Info =
    2.14 +      Build_Log.parse_session_info(
    2.15 +        log_file, session_name, command_timings, ml_statistics, task_statistics)
    2.16  
    2.17      def parse_header: Header = Build_Log.parse_header(log_file)
    2.18  
    2.19 @@ -126,22 +131,30 @@
    2.20      ml_statistics: List[Properties.T],
    2.21      task_statistics: List[Properties.T])
    2.22  
    2.23 -  private def parse_session_info(log_file: Log_File, name0: String, full: Boolean): Session_Info =
    2.24 +  private def parse_session_info(
    2.25 +    log_file: Log_File,
    2.26 +    default_name: String,
    2.27 +    command_timings: Boolean,
    2.28 +    ml_statistics: Boolean,
    2.29 +    task_statistics: Boolean): Session_Info =
    2.30    {
    2.31      val xml_cache = new XML.Cache()
    2.32  
    2.33      val session_name =
    2.34        log_file.find_line("\fSession.name = ") match {
    2.35 -        case None => name0
    2.36 -        case Some(name) if name0 == "" || name0 == name => name
    2.37 +        case None => default_name
    2.38 +        case Some(name) if default_name == "" || default_name == name => name
    2.39          case Some(name) => log_file.err("log from different session " + quote(name))
    2.40        }
    2.41      val session_timing = log_file.find_props("\fTiming = ") getOrElse Nil
    2.42 -    val command_timings = log_file.filter_props("\fcommand_timing = ")
    2.43 -    val ml_statistics = if (full) log_file.filter_props("\fML_statistics = ") else Nil
    2.44 -    val task_statistics = if (full) log_file.filter_props("\ftask_statistics = ") else Nil
    2.45 +    val command_timings_ =
    2.46 +      if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil
    2.47 +    val ml_statistics_ =
    2.48 +      if (ml_statistics) log_file.filter_props("\fML_statistics = ") else Nil
    2.49 +    val task_statistics_ =
    2.50 +      if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil
    2.51  
    2.52 -    Session_Info(session_name, session_timing, command_timings, ml_statistics, task_statistics)
    2.53 +    Session_Info(session_name, session_timing, command_timings_, ml_statistics_, task_statistics_)
    2.54    }
    2.55  
    2.56  
     3.1 --- a/src/Pure/Tools/ci_api.scala	Fri Oct 07 11:45:30 2016 +0200
     3.2 +++ b/src/Pure/Tools/ci_api.scala	Fri Oct 07 13:58:10 2016 +0200
     3.3 @@ -45,12 +45,9 @@
     3.4      session_logs: List[(String, URL)])
     3.5    {
     3.6      def read_output(): Build_Log.Log_File = Build_Log.Log_File(job_name, Url.read(output))
     3.7 -    def read_log(name: String, full: Boolean): Build_Log.Session_Info =
     3.8 -    {
     3.9 -      val text =
    3.10 -        session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse ""
    3.11 -      Build_Log.Log_File(name, text).parse_session_info(name, full)
    3.12 -    }
    3.13 +    def read_log_file(name: String): Build_Log.Log_File =
    3.14 +      Build_Log.Log_File(name,
    3.15 +        session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "")
    3.16    }
    3.17  
    3.18    def build_job_builds(job_name: String): List[Job_Info] =