# HG changeset patch
# User wenzelm
# Date 1493625902 -7200
# Node ID 1b84d4109215269f4afa036238b079d8521ec09c
# Parent  0fbaa92863310d5df8dbc9a1adbdae1ad63d68c4
clarified signature;

diff -r 0fbaa9286331 -r 1b84d4109215 src/Pure/Admin/build_stats.scala
--- a/src/Pure/Admin/build_stats.scala	Mon May 01 09:52:11 2017 +0200
+++ b/src/Pure/Admin/build_stats.scala	Mon May 01 10:05:02 2017 +0200
@@ -29,7 +29,7 @@
 
     val all_infos =
       Par_List.map((job_info: Jenkins.Job_Info) =>
-        (job_info.timestamp / 1000, job_info.read_main_log.parse_build_info()), job_infos)
+        (job_info.timestamp / 1000, job_info.read_log_file.parse_build_info()), job_infos)
     val all_sessions =
       (Set.empty[String] /: all_infos)(
         { case (s, (_, info)) => s ++ info.sessions.keySet })
diff -r 0fbaa9286331 -r 1b84d4109215 src/Pure/Admin/jenkins.scala
--- a/src/Pure/Admin/jenkins.scala	Mon May 01 09:52:11 2017 +0200
+++ b/src/Pure/Admin/jenkins.scala	Mon May 01 10:05:02 2017 +0200
@@ -42,22 +42,21 @@
   sealed case class Job_Info(
     job_name: String,
     timestamp: Long,
-    output: URL,
+    main_log: URL,
     session_logs: List[(String, String, URL)])
   {
-    def date: Date = Date(Time.ms(timestamp), ZoneId.of("Europe/Berlin"))
-    def log_filename: Path =
-      Build_Log.log_filename(Build_Log.Jenkins.engine, date, List(job_name))
+    val date: Date = Date(Time.ms(timestamp), ZoneId.of("Europe/Berlin"))
+    val log_filename: Path = Build_Log.log_filename(Build_Log.Jenkins.engine, date, List(job_name))
 
-    def read_main_log(): Build_Log.Log_File =
-      Build_Log.Log_File(log_filename.implode, Url.read(output))
-
-    def session_log(name: String, ext: String): Option[URL] =
-      session_logs.collectFirst({ case (a, b, url) if a == name && b == ext => url })
+    def read_log_file(): Build_Log.Log_File =
+      Build_Log.Log_File(log_filename.implode, Url.read(main_log))
 
     def read_ml_statistics(store: Sessions.Store, session_name: String): List[Properties.T] =
     {
-      session_log(session_name, "db") match {
+      def get_log(ext: String): Option[URL] =
+        session_logs.collectFirst({ case (a, b, url) if a == session_name && b == ext => url })
+
+      get_log("db") match {
         case Some(url) =>
           Isabelle_System.with_tmp_file(session_name, "db") { database =>
             Bytes.write(database, Bytes.read(url))
@@ -65,7 +64,7 @@
               store.read_build_log(db, session_name, ml_statistics = true)).ml_statistics
           }
         case None =>
-          session_log(session_name, "gz") match {
+          get_log("gz") match {
             case Some(url) =>
               val log_file = Build_Log.Log_File(session_name, Url.read_gzip(url))
               log_file.parse_session_info(ml_statistics = true).ml_statistics
@@ -88,14 +87,14 @@
       timestamp <- JSON.long(build, "timestamp")
     } yield {
       val job_prefix = root() + "/job/" + job_name + "/" + number
-      val output = Url(job_prefix + "/consoleText")
+      val main_log = Url(job_prefix + "/consoleText")
       val session_logs =
         for {
           artifact <- JSON.array(build, "artifacts").getOrElse(Nil)
           log_path <- JSON.string(artifact, "relativePath")
           (name, ext) <- (log_path match { case Session_Log(a, b) => Some((a, b)) case _ => None })
         } yield (name, ext, Url(job_prefix + "/artifact/" + log_path))
-      Job_Info(job_name, timestamp, output, session_logs)
+      Job_Info(job_name, timestamp, main_log, session_logs)
     }
   }
 }