tuned signature;
authorwenzelm
Sat Oct 08 15:45:47 2016 +0200 (2016-10-08)
changeset 64106b7ff61d50b19
parent 64105 d93bd6d253c6
child 64107 87d32aa83410
tuned signature;
src/Pure/Tools/build_stats.scala
src/Pure/Tools/ci_api.scala
     1.1 --- a/src/Pure/Tools/build_stats.scala	Sat Oct 08 15:39:42 2016 +0200
     1.2 +++ b/src/Pure/Tools/build_stats.scala	Sat Oct 08 15:45:47 2016 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4  
     1.5      val all_infos =
     1.6        Par_List.map((job_info: CI_API.Job_Info) =>
     1.7 -        (job_info.timestamp / 1000, job_info.read_output.parse_build_info), job_infos)
     1.8 +        (job_info.timestamp / 1000, job_info.read_main_log.parse_build_info), job_infos)
     1.9      val all_sessions =
    1.10        (Set.empty[String] /: all_infos)(
    1.11          { case (s, (_, info)) => s ++ info.sessions.keySet })
     2.1 --- a/src/Pure/Tools/ci_api.scala	Sat Oct 08 15:39:42 2016 +0200
     2.2 +++ b/src/Pure/Tools/ci_api.scala	Sat Oct 08 15:45:47 2016 +0200
     2.3 @@ -44,8 +44,8 @@
     2.4      output: URL,
     2.5      session_logs: List[(String, URL)])
     2.6    {
     2.7 -    def read_output(): Build_Log.Log_File = Build_Log.Log_File(job_name, Url.read(output))
     2.8 -    def read_log_file(name: String): Build_Log.Log_File =
     2.9 +    def read_main_log(): Build_Log.Log_File = Build_Log.Log_File(job_name, Url.read(output))
    2.10 +    def read_session_log(name: String): Build_Log.Log_File =
    2.11        Build_Log.Log_File(name,
    2.12          session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "")
    2.13    }