# HG changeset patch
# User wenzelm
# Date 1494359026 -7200
# Node ID 7d1c5150af70419a7fa28c0a17996d7d3ddda6d2
# Parent  c60b1a2c3abc4a7b241046b9293fd7c56bd8f5e6
more output;

diff -r c60b1a2c3abc -r 7d1c5150af70 src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Tue May 09 21:27:34 2017 +0200
+++ b/src/Pure/Admin/build_status.scala	Tue May 09 21:43:46 2017 +0200
@@ -63,6 +63,10 @@
   {
     require(entries.nonEmpty)
 
+    def pull_date: Date = entries.head.pull_date
+    def isabelle_version: String = entries.head.isabelle_version
+    def afp_version: String = entries.head.afp_version
+
     def timing: Timing = entries.head.timing
     def ml_timing: Timing = entries.head.ml_timing
     def order: Long = - timing.elapsed.ms
@@ -70,7 +74,8 @@
     def check_timing: Boolean = entries.length >= 3
     def check_heap: Boolean = entries.forall(_.heap_size > 0)
   }
-  sealed case class Entry(date: Date, timing: Timing, ml_timing: Timing, heap_size: Long)
+  sealed case class Entry(pull_date: Date, isabelle_version: String, afp_version: String,
+    timing: Timing, ml_timing: Timing, heap_size: Long)
 
   def read_data(options: Options,
     progress: Progress = No_Progress,
@@ -94,6 +99,8 @@
           List(
             Build_Log.Data.pull_date,
             Build_Log.Prop.build_host,
+            Build_Log.Prop.isabelle_version,
+            Build_Log.Prop.afp_version,
             Build_Log.Settings.ISABELLE_BUILD_OPTIONS,
             Build_Log.Settings.ML_PLATFORM,
             Build_Log.Data.session_name,
@@ -133,15 +140,20 @@
                 (if (threads == 1) "" else ", " + threads + " threads")
 
             val entry =
-              Entry(res.date(Build_Log.Data.pull_date),
-                res.timing(
-                  Build_Log.Data.timing_elapsed,
-                  Build_Log.Data.timing_cpu,
-                  Build_Log.Data.timing_gc),
-                res.timing(
-                  Build_Log.Data.ml_timing_elapsed,
-                  Build_Log.Data.ml_timing_cpu,
-                  Build_Log.Data.ml_timing_gc),
+              Entry(
+                pull_date = res.date(Build_Log.Data.pull_date),
+                isabelle_version = res.string(Build_Log.Prop.isabelle_version),
+                afp_version = res.string(Build_Log.Prop.afp_version),
+                timing =
+                  res.timing(
+                    Build_Log.Data.timing_elapsed,
+                    Build_Log.Data.timing_cpu,
+                    Build_Log.Data.timing_gc),
+                ml_timing =
+                  res.timing(
+                    Build_Log.Data.ml_timing_elapsed,
+                    Build_Log.Data.ml_timing_cpu,
+                    Build_Log.Data.ml_timing_gc),
                 heap_size = res.long(Build_Log.Data.heap_size))
 
             res.get_string(Build_Log.Prop.build_host).foreach(host =>
@@ -206,7 +218,7 @@
               File.write(data_file,
                 cat_lines(
                   session.entries.map(entry =>
-                    List(entry.date.unix_epoch.toString,
+                    List(entry.pull_date.unix_epoch.toString,
                       entry.timing.elapsed.minutes,
                       entry.timing.resources.minutes,
                       entry.ml_timing.elapsed.minutes,
@@ -298,11 +310,13 @@
               HTML.section(session.name) + HTML.id("session_" + session.name),
               HTML.par(
                 HTML.itemize(List(
-                  HTML.bold(HTML.text("status date: ")) :: HTML.text(data.date.toString),
-                  HTML.bold(HTML.text("build host: ")) :: HTML.text(commas(data_entry.hosts)),
                   HTML.bold(HTML.text("timing: ")) :: HTML.text(session.timing.message_resources),
                   HTML.bold(HTML.text("ML timing: ")) ::
-                    HTML.text(session.ml_timing.message_resources))) ::
+                    HTML.text(session.ml_timing.message_resources)) :::
+                  proper_string(session.isabelle_version).map(s =>
+                    HTML.bold(HTML.text("Isabelle version: ")) :: HTML.text(s)).toList :::
+                  proper_string(session.afp_version).map(s =>
+                    HTML.bold(HTML.text("AFP version: ")) :: HTML.text(s)).toList) ::
                 session_plots.getOrElse(session.name, Nil).map(plot_name =>
                   HTML.image(plot_name) +
                     HTML.width(image_size._1 / 2) +