merged
authorwenzelm
Sat Oct 08 17:30:19 2016 +0200 (2016-10-08)
changeset 6411284c1ae86b9af
parent 64097 331fbf2a0d2d
parent 64111 b2290b9d0175
child 64113 86efd3d4dc98
merged
     1.1 --- a/src/Pure/General/date.scala	Sat Oct 08 13:50:25 2016 +0200
     1.2 +++ b/src/Pure/General/date.scala	Sat Oct 08 17:30:19 2016 +0200
     1.3 @@ -21,58 +21,54 @@
     1.4  
     1.5    object Format
     1.6    {
     1.7 -    def make(fmts: List[DateTimeFormatter], filter: String => String = s => s): Format =
     1.8 +    def make(fmts: List[DateTimeFormatter], tune: String => String = s => s): Format =
     1.9      {
    1.10        require(fmts.nonEmpty)
    1.11  
    1.12 -      @tailrec def parse_first(
    1.13 -        last_exn: Option[Throwable], fs: List[DateTimeFormatter], str: String): TemporalAccessor =
    1.14 -      {
    1.15 -        fs match {
    1.16 -          case Nil => throw last_exn.get
    1.17 -          case f :: rest =>
    1.18 -            try { ZonedDateTime.from(f.parse(str)) }
    1.19 -            catch { case exn: DateTimeParseException => parse_first(Some(exn), rest, str) }
    1.20 -        }
    1.21 -      }
    1.22        new Format {
    1.23          def apply(date: Date): String = fmts.head.format(date.rep)
    1.24          def parse(str: String): Date =
    1.25 -          new Date(ZonedDateTime.from(parse_first(None, fmts, filter(str))))
    1.26 +          new Date(ZonedDateTime.from(Formatter.try_variants(fmts, tune(str))))
    1.27        }
    1.28      }
    1.29  
    1.30 -    def make_variants(patterns: List[String],
    1.31 -      locales: List[Locale] = List(Locale.ROOT),
    1.32 -      filter: String => String = s => s): Format =
    1.33 -    {
    1.34 -      val fmts =
    1.35 -        patterns.flatMap(pat =>
    1.36 -          {
    1.37 -            val fmt = DateTimeFormatter.ofPattern(pat)
    1.38 -            locales.map(fmt.withLocale(_))
    1.39 -          })
    1.40 -      make(fmts, filter)
    1.41 -    }
    1.42 +    def apply(pats: String*): Format =
    1.43 +      make(pats.toList.map(Date.Formatter.pattern(_)))
    1.44  
    1.45 -    def apply(patterns: String*): Format =
    1.46 -      make(patterns.toList.map(DateTimeFormatter.ofPattern(_)))
    1.47 -
    1.48 -    val default: Format = apply("dd-MMM-uuuu HH:mm:ss xx")
    1.49 -    val date: Format = apply("dd-MMM-uuuu")
    1.50 -    val time: Format = apply("HH:mm:ss")
    1.51 +    val default: Format = Format("dd-MMM-uuuu HH:mm:ss xx")
    1.52 +    val date: Format = Format("dd-MMM-uuuu")
    1.53 +    val time: Format = Format("HH:mm:ss")
    1.54    }
    1.55  
    1.56    abstract class Format private
    1.57    {
    1.58      def apply(date: Date): String
    1.59      def parse(str: String): Date
    1.60 +
    1.61      def unapply(str: String): Option[Date] =
    1.62 -      try { Some(parse(str)) }
    1.63 -      catch { case _: DateTimeParseException => None }
    1.64 -    object Strict
    1.65 +      try { Some(parse(str)) } catch { case _: DateTimeParseException => None }
    1.66 +  }
    1.67 +
    1.68 +  object Formatter
    1.69 +  {
    1.70 +    def pattern(pat: String): DateTimeFormatter = DateTimeFormatter.ofPattern(pat)
    1.71 +
    1.72 +    def variants(pats: List[String], locs: List[Locale] = Nil): List[DateTimeFormatter] =
    1.73 +      pats.flatMap(pat => {
    1.74 +        val fmt = pattern(pat)
    1.75 +        if (locs.isEmpty) List(fmt) else locs.map(fmt.withLocale(_))
    1.76 +      })
    1.77 +
    1.78 +    @tailrec def try_variants(fmts: List[DateTimeFormatter], str: String,
    1.79 +      last_exn: Option[DateTimeParseException] = None): TemporalAccessor =
    1.80      {
    1.81 -      def unapply(s: String): Some[Date] = Some(parse(s))
    1.82 +      fmts match {
    1.83 +        case Nil =>
    1.84 +          throw last_exn.getOrElse(new DateTimeParseException("Failed to parse date", str, 0))
    1.85 +        case fmt :: rest =>
    1.86 +          try { ZonedDateTime.from(fmt.parse(str)) }
    1.87 +          catch { case exn: DateTimeParseException => try_variants(rest, str, Some(exn)) }
    1.88 +      }
    1.89      }
    1.90    }
    1.91  
    1.92 @@ -89,6 +85,9 @@
    1.93  
    1.94  sealed case class Date(rep: ZonedDateTime)
    1.95  {
    1.96 +  def to(zone: ZoneId): Date = new Date(rep.withZoneSameInstant(zone))
    1.97 +  def to_utc: Date = to(ZoneId.of("UTC"))
    1.98 +
    1.99    def time: Time = Time.instant(Instant.from(rep))
   1.100    def timezone: ZoneId = rep.getZone
   1.101  
     2.1 --- a/src/Pure/Tools/build_log.scala	Sat Oct 08 13:50:25 2016 +0200
     2.2 +++ b/src/Pure/Tools/build_log.scala	Sat Oct 08 17:30:19 2016 +0200
     2.3 @@ -1,16 +1,16 @@
     2.4  /*  Title:      Pure/Tools/build_log.scala
     2.5      Author:     Makarius
     2.6  
     2.7 -Build log parsing for historic versions, back to "build_history_base".
     2.8 +Build log parsing for current and historic formats.
     2.9  */
    2.10  
    2.11  package isabelle
    2.12  
    2.13  
    2.14 +import java.io.{File => JFile}
    2.15 +import java.time.ZoneId
    2.16 +import java.time.format.{DateTimeFormatter, DateTimeParseException}
    2.17  import java.util.Locale
    2.18 -import java.io.{File => JFile}
    2.19 -import java.time.ZonedDateTime
    2.20 -import java.time.format.{DateTimeFormatter, DateTimeParseException}
    2.21  
    2.22  import scala.collection.mutable
    2.23  import scala.util.matching.Regex
    2.24 @@ -18,6 +18,19 @@
    2.25  
    2.26  object Build_Log
    2.27  {
    2.28 +  /** directory content **/
    2.29 +
    2.30 +  def is_log(file: JFile): Boolean =
    2.31 +    List(".log", ".log.gz", ".log.xz").exists(ext => file.getName.endsWith(ext))
    2.32 +
    2.33 +  def isatest_files(dir: Path): List[JFile] =
    2.34 +    File.find_files(dir.file, file => is_log(file) && file.getName.startsWith("isatest-makeall-"))
    2.35 +
    2.36 +  def afp_test_files(dir: Path): List[JFile] =
    2.37 +    File.find_files(dir.file, file => is_log(file) && file.getName.startsWith("afp-test-devel-"))
    2.38 +
    2.39 +
    2.40 +
    2.41    /** settings **/
    2.42  
    2.43    object Settings
    2.44 @@ -49,6 +62,7 @@
    2.45    }
    2.46  
    2.47  
    2.48 +
    2.49    /** log file **/
    2.50  
    2.51    object Log_File
    2.52 @@ -75,6 +89,49 @@
    2.53      }
    2.54  
    2.55      def apply(path: Path): Log_File = apply(path.file)
    2.56 +
    2.57 +
    2.58 +    /* date format */
    2.59 +
    2.60 +    val Date_Format =
    2.61 +    {
    2.62 +      val fmts =
    2.63 +        Date.Formatter.variants(
    2.64 +          List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"),
    2.65 +          List(Locale.ENGLISH, Locale.GERMAN)) :::
    2.66 +        List(
    2.67 +          DateTimeFormatter.RFC_1123_DATE_TIME,
    2.68 +          Date.Formatter.pattern("EEE MMM d HH:mm:ss yyyy").withZone(ZoneId.of("Europe/Berlin")))
    2.69 +
    2.70 +      def tune_timezone(s: String): String =
    2.71 +        s match {
    2.72 +          case "CET" | "MET" => "GMT+1"
    2.73 +          case "CEST" | "MEST" => "GMT+2"
    2.74 +          case "EST" => "Europe/Berlin"
    2.75 +          case _ => s
    2.76 +        }
    2.77 +      def tune_weekday(s: String): String =
    2.78 +        s match {
    2.79 +          case "Die" => "Di"
    2.80 +          case "Mit" => "Mi"
    2.81 +          case "Don" => "Do"
    2.82 +          case "Fre" => "Fr"
    2.83 +          case "Sam" => "Sa"
    2.84 +          case "Son" => "So"
    2.85 +          case _ => s
    2.86 +        }
    2.87 +
    2.88 +      def tune(s: String): String =
    2.89 +        Word.implode(
    2.90 +          Word.explode(s) match {
    2.91 +            case a :: "M\uFFFDr" :: bs => tune_weekday(a) :: "Mär" :: bs.map(tune_timezone(_))
    2.92 +            case a :: bs => tune_weekday(a) :: bs.map(tune_timezone(_))
    2.93 +            case Nil => Nil
    2.94 +          }
    2.95 +        )
    2.96 +
    2.97 +      Date.Format.make(fmts, tune)
    2.98 +    }
    2.99    }
   2.100  
   2.101    class Log_File private(val name: String, val lines: List[String])
   2.102 @@ -89,6 +146,16 @@
   2.103        error("Error in log file " + quote(name) + ": " + msg)
   2.104  
   2.105  
   2.106 +    /* date format */
   2.107 +
   2.108 +    object Strict_Date
   2.109 +    {
   2.110 +      def unapply(s: String): Some[Date] =
   2.111 +        try { Some(Log_File.Date_Format.parse(s)) }
   2.112 +        catch { case exn: DateTimeParseException => log_file.err(exn.getMessage) }
   2.113 +    }
   2.114 +
   2.115 +
   2.116      /* inlined content */
   2.117  
   2.118      def find[A](f: String => Option[A]): Option[A] =
   2.119 @@ -130,6 +197,10 @@
   2.120  
   2.121      /* parse various formats */
   2.122  
   2.123 +    def parse_meta_info(): Meta_Info = Build_Log.parse_meta_info(log_file)
   2.124 +
   2.125 +    def parse_build_info(): Build_Info = Build_Log.parse_build_info(log_file)
   2.126 +
   2.127      def parse_session_info(
   2.128          default_name: String = "",
   2.129          command_timings: Boolean = false,
   2.130 @@ -137,74 +208,15 @@
   2.131          task_statistics: Boolean = false): Session_Info =
   2.132        Build_Log.parse_session_info(
   2.133          log_file, default_name, command_timings, ml_statistics, task_statistics)
   2.134 -
   2.135 -    def parse_header(): Header = Build_Log.parse_header(log_file)
   2.136 -
   2.137 -    def parse_build_info(): Build_Info = Build_Log.parse_build_info(log_file)
   2.138    }
   2.139  
   2.140  
   2.141 -  /* session log: produced by "isabelle build" */
   2.142  
   2.143 -  sealed case class Session_Info(
   2.144 -    session_name: String,
   2.145 -    session_timing: Properties.T,
   2.146 -    command_timings: List[Properties.T],
   2.147 -    ml_statistics: List[Properties.T],
   2.148 -    task_statistics: List[Properties.T])
   2.149 -
   2.150 -  private def parse_session_info(
   2.151 -    log_file: Log_File,
   2.152 -    default_name: String,
   2.153 -    command_timings: Boolean,
   2.154 -    ml_statistics: Boolean,
   2.155 -    task_statistics: Boolean): Session_Info =
   2.156 -  {
   2.157 -    val xml_cache = new XML.Cache()
   2.158 -
   2.159 -    val session_name =
   2.160 -      log_file.find_line("\fSession.name = ") match {
   2.161 -        case None => default_name
   2.162 -        case Some(name) if default_name == "" || default_name == name => name
   2.163 -        case Some(name) => log_file.err("log from different session " + quote(name))
   2.164 -      }
   2.165 -    val session_timing = log_file.find_props("\fTiming = ") getOrElse Nil
   2.166 -    val command_timings_ =
   2.167 -      if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil
   2.168 -    val ml_statistics_ =
   2.169 -      if (ml_statistics) log_file.filter_props("\fML_statistics = ") else Nil
   2.170 -    val task_statistics_ =
   2.171 -      if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil
   2.172 -
   2.173 -    Session_Info(session_name, session_timing, command_timings_, ml_statistics_, task_statistics_)
   2.174 -  }
   2.175 -
   2.176 -
   2.177 -  /* header and meta data */
   2.178 -
   2.179 -  val Date_Format =
   2.180 -    Date.Format.make_variants(
   2.181 -      List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"),
   2.182 -      List(Locale.ENGLISH, Locale.GERMAN),
   2.183 -      // workaround for jdk-8u102
   2.184 -      s => Word.implode(Word.explode(s).map({
   2.185 -        case "CET" | "MET" => "GMT+1"
   2.186 -        case "CEST" | "MEST" => "GMT+2"
   2.187 -        case "EST" => "GMT+1"  // FIXME ??
   2.188 -        case a => a })))
   2.189 -
   2.190 -  object Header_Kind extends Enumeration
   2.191 -  {
   2.192 -    val ISATEST = Value("isatest")
   2.193 -    val AFP_TEST = Value("afp-test")
   2.194 -    val JENKINS = Value("jenkins")
   2.195 -  }
   2.196 -
   2.197 -  sealed case class Header(
   2.198 -    kind: Header_Kind.Value, props: Properties.T, settings: List[(String, String)])
   2.199 +  /** meta info **/
   2.200  
   2.201    object Field
   2.202    {
   2.203 +    val build_engine = "build_engine"
   2.204      val build_host = "build_host"
   2.205      val build_start = "build_start"
   2.206      val build_end = "build_end"
   2.207 @@ -212,66 +224,110 @@
   2.208      val afp_version = "afp_version"
   2.209    }
   2.210  
   2.211 +  object Meta_Info
   2.212 +  {
   2.213 +    val empty: Meta_Info = Meta_Info(Nil, Nil)
   2.214 +  }
   2.215 +
   2.216 +  sealed case class Meta_Info(props: Properties.T, settings: List[(String, String)])
   2.217 +  {
   2.218 +    def is_empty: Boolean = props.isEmpty && settings.isEmpty
   2.219 +  }
   2.220 +
   2.221    object Isatest
   2.222    {
   2.223 -    val Test_Start = new Regex("""^------------------- starting test --- (.+) --- (.+)$""")
   2.224 -    val Test_End = new Regex("""^------------------- test (?:successful|FAILED) --- (.+) --- .*$""")
   2.225 +    val engine = "isatest"
   2.226 +    val Start = new Regex("""^------------------- starting test --- (.+) --- (.+)$""")
   2.227 +    val End = new Regex("""^------------------- test (?:successful|FAILED) --- (.+) --- .*$""")
   2.228      val Isabelle_Version = new Regex("""^Isabelle version: (\S+)$""")
   2.229      val No_AFP_Version = new Regex("""$.""")
   2.230    }
   2.231  
   2.232 -  object AFP
   2.233 +  object AFP_Test
   2.234    {
   2.235 -    val Test_Start = new Regex("""^Start test(?: for .+)? at ([^,]+), (.*)$""")
   2.236 -    val Test_Start_Old = new Regex("""^Start test(?: for .+)? at ([^,]+)$""")
   2.237 -    val Test_End = new Regex("""^End test on (.+), .+, elapsed time:.*$""")
   2.238 +    val engine = "afp-test"
   2.239 +    val Start = new Regex("""^Start test(?: for .+)? at ([^,]+), (.*)$""")
   2.240 +    val Start_Old = new Regex("""^Start test(?: for .+)? at ([^,]+)$""")
   2.241 +    val End = new Regex("""^End test on (.+), .+, elapsed time:.*$""")
   2.242      val Isabelle_Version = new Regex("""^Isabelle version: .* -- hg id (\S+)$""")
   2.243      val AFP_Version = new Regex("""^AFP version: .* -- hg id (\S+)$""")
   2.244 +    val Bad_Init = new Regex("""^cp:.*: Disc quota exceeded$""")
   2.245    }
   2.246  
   2.247 -  private def parse_header(log_file: Log_File): Header =
   2.248 +  object Jenkins
   2.249    {
   2.250 -    def parse(kind: Header_Kind.Value, start: Date, hostname: String,
   2.251 -      Test_End: Regex, Isabelle_Version: Regex, AFP_Version: Regex): Header =
   2.252 +    val engine = "jenkins"
   2.253 +    val Start = new Regex("""^Started .*$""")
   2.254 +    val Start_Date = new Regex("""^Build started at (.+)$""")
   2.255 +    val No_End = new Regex("""$.""")
   2.256 +    val Isabelle_Version = new Regex("""^Isabelle id (\S+)$""")
   2.257 +    val AFP_Version = new Regex("""^AFP id (\S+)$""")
   2.258 +    val CONFIGURATION = "=== CONFIGURATION ==="
   2.259 +    val BUILD = "=== BUILD ==="
   2.260 +    val FINISHED = "Finished: "
   2.261 +  }
   2.262 +
   2.263 +  private def parse_meta_info(log_file: Log_File): Meta_Info =
   2.264 +  {
   2.265 +    def parse(engine: String, host: String, start: Date,
   2.266 +      End: Regex, Isabelle_Version: Regex, AFP_Version: Regex): Meta_Info =
   2.267      {
   2.268 -      val start_date = Field.build_start -> start.toString
   2.269 +      val build_engine = if (engine == "") Nil else List(Field.build_engine -> engine)
   2.270 +      val build_host = if (host == "") Nil else List(Field.build_host -> host)
   2.271 +
   2.272 +      val start_date = List(Field.build_start -> start.toString)
   2.273        val end_date =
   2.274          log_file.lines.last match {
   2.275 -          case Test_End(Date_Format.Strict(end_date)) =>
   2.276 +          case End(log_file.Strict_Date(end_date)) =>
   2.277              List(Field.build_end -> end_date.toString)
   2.278            case _ => Nil
   2.279          }
   2.280  
   2.281 -      val build_host = if (hostname == "") Nil else List(Field.build_host -> hostname)
   2.282 -
   2.283        val isabelle_version =
   2.284          log_file.find_match(Isabelle_Version).map(Field.isabelle_version -> _)
   2.285 -
   2.286        val afp_version =
   2.287          log_file.find_match(AFP_Version).map(Field.afp_version -> _)
   2.288  
   2.289 -      Header(kind,
   2.290 -        start_date :: end_date ::: build_host :::
   2.291 -          isabelle_version.toList ::: afp_version.toList,
   2.292 +      Meta_Info(build_engine ::: build_host :::
   2.293 +          start_date ::: end_date ::: isabelle_version.toList ::: afp_version.toList,
   2.294          log_file.get_settings(Settings.all_settings))
   2.295      }
   2.296  
   2.297      log_file.lines match {
   2.298 -      case Isatest.Test_Start(Date_Format.Strict(start), hostname) :: _ =>
   2.299 -        parse(Header_Kind.ISATEST, start, hostname,
   2.300 -          Isatest.Test_End, Isatest.Isabelle_Version, Isatest.No_AFP_Version)
   2.301 -      case AFP.Test_Start(Date_Format.Strict(start), hostname) :: _ =>
   2.302 -        parse(Header_Kind.AFP_TEST, start, hostname,
   2.303 -          AFP.Test_End, AFP.Isabelle_Version, AFP.AFP_Version)
   2.304 -      case AFP.Test_Start_Old(Date_Format.Strict(start)) :: _ =>
   2.305 -        parse(Header_Kind.AFP_TEST, start, "",
   2.306 -          AFP.Test_End, AFP.Isabelle_Version, AFP.AFP_Version)
   2.307 -      case _ => log_file.err("cannot detect log header format")
   2.308 +      case Isatest.Start(log_file.Strict_Date(start), host) :: _ =>
   2.309 +        parse(Isatest.engine, host, start, Isatest.End,
   2.310 +          Isatest.Isabelle_Version, Isatest.No_AFP_Version)
   2.311 +
   2.312 +      case AFP_Test.Start(log_file.Strict_Date(start), host) :: _ =>
   2.313 +        parse(AFP_Test.engine, host, start, AFP_Test.End,
   2.314 +          AFP_Test.Isabelle_Version, AFP_Test.AFP_Version)
   2.315 +
   2.316 +      case AFP_Test.Start_Old(log_file.Strict_Date(start)) :: _ =>
   2.317 +        parse(AFP_Test.engine, "", start, AFP_Test.End,
   2.318 +          AFP_Test.Isabelle_Version, AFP_Test.AFP_Version)
   2.319 +
   2.320 +      case Jenkins.Start() :: _
   2.321 +      if log_file.lines.contains(Jenkins.CONFIGURATION) ||
   2.322 +         log_file.lines.last.startsWith(Jenkins.FINISHED) =>
   2.323 +        log_file.lines.dropWhile(_ != Jenkins.BUILD) match {
   2.324 +          case Jenkins.BUILD :: _ :: Jenkins.Start_Date(log_file.Strict_Date(start)) :: _ =>
   2.325 +            parse(Jenkins.engine, "", start.to(ZoneId.of("Europe/Berlin")), Jenkins.No_End,
   2.326 +              Jenkins.Isabelle_Version, Jenkins.AFP_Version)
   2.327 +          case _ => Meta_Info.empty
   2.328 +        }
   2.329 +
   2.330 +      case line :: _ if line.startsWith("\0") => Meta_Info.empty
   2.331 +      case List(Isatest.End(_)) => Meta_Info.empty
   2.332 +      case _ :: AFP_Test.Bad_Init() :: _ => Meta_Info.empty
   2.333 +      case Nil => Meta_Info.empty
   2.334 +
   2.335 +      case _ => log_file.err("cannot detect log file format")
   2.336      }
   2.337    }
   2.338  
   2.339  
   2.340 -  /* build info: produced by isabelle build */
   2.341 +
   2.342 +  /** build info: produced by isabelle build **/
   2.343  
   2.344    object Session_Status extends Enumeration
   2.345    {
   2.346 @@ -397,4 +453,41 @@
   2.347          }):_*)
   2.348      Build_Info(sessions)
   2.349    }
   2.350 +
   2.351 +
   2.352 +
   2.353 +  /** session info: produced by "isabelle build" **/
   2.354 +
   2.355 +  sealed case class Session_Info(
   2.356 +    session_name: String,
   2.357 +    session_timing: Properties.T,
   2.358 +    command_timings: List[Properties.T],
   2.359 +    ml_statistics: List[Properties.T],
   2.360 +    task_statistics: List[Properties.T])
   2.361 +
   2.362 +  private def parse_session_info(
   2.363 +    log_file: Log_File,
   2.364 +    default_name: String,
   2.365 +    command_timings: Boolean,
   2.366 +    ml_statistics: Boolean,
   2.367 +    task_statistics: Boolean): Session_Info =
   2.368 +  {
   2.369 +    val xml_cache = new XML.Cache()
   2.370 +
   2.371 +    val session_name =
   2.372 +      log_file.find_line("\fSession.name = ") match {
   2.373 +        case None => default_name
   2.374 +        case Some(name) if default_name == "" || default_name == name => name
   2.375 +        case Some(name) => log_file.err("log from different session " + quote(name))
   2.376 +      }
   2.377 +    val session_timing = log_file.find_props("\fTiming = ") getOrElse Nil
   2.378 +    val command_timings_ =
   2.379 +      if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil
   2.380 +    val ml_statistics_ =
   2.381 +      if (ml_statistics) log_file.filter_props("\fML_statistics = ") else Nil
   2.382 +    val task_statistics_ =
   2.383 +      if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil
   2.384 +
   2.385 +    Session_Info(session_name, session_timing, command_timings_, ml_statistics_, task_statistics_)
   2.386 +  }
   2.387  }
     3.1 --- a/src/Pure/Tools/build_stats.scala	Sat Oct 08 13:50:25 2016 +0200
     3.2 +++ b/src/Pure/Tools/build_stats.scala	Sat Oct 08 17:30:19 2016 +0200
     3.3 @@ -29,7 +29,7 @@
     3.4  
     3.5      val all_infos =
     3.6        Par_List.map((job_info: CI_API.Job_Info) =>
     3.7 -        (job_info.timestamp / 1000, job_info.read_output.parse_build_info), job_infos)
     3.8 +        (job_info.timestamp / 1000, job_info.read_main_log.parse_build_info), job_infos)
     3.9      val all_sessions =
    3.10        (Set.empty[String] /: all_infos)(
    3.11          { case (s, (_, info)) => s ++ info.sessions.keySet })
     4.1 --- a/src/Pure/Tools/ci_api.scala	Sat Oct 08 13:50:25 2016 +0200
     4.2 +++ b/src/Pure/Tools/ci_api.scala	Sat Oct 08 17:30:19 2016 +0200
     4.3 @@ -44,8 +44,8 @@
     4.4      output: URL,
     4.5      session_logs: List[(String, URL)])
     4.6    {
     4.7 -    def read_output(): Build_Log.Log_File = Build_Log.Log_File(job_name, Url.read(output))
     4.8 -    def read_log_file(name: String): Build_Log.Log_File =
     4.9 +    def read_main_log(): Build_Log.Log_File = Build_Log.Log_File(job_name, Url.read(output))
    4.10 +    def read_session_log(name: String): Build_Log.Log_File =
    4.11        Build_Log.Log_File(name,
    4.12          session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "")
    4.13    }