# HG changeset patch
# User wenzelm
# Date 1494357932 -7200
# Node ID a880f41a8d0fe09a05aa47a91ffe1e5237b3d12a
# Parent  96b4799a2e04f0f6cd22a55ea6e8ef682319875e
tuned output;

diff -r 96b4799a2e04 -r a880f41a8d0f src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Tue May 09 21:06:11 2017 +0200
+++ b/src/Pure/Admin/build_status.scala	Tue May 09 21:25:32 2017 +0200
@@ -180,9 +180,13 @@
       HTML.output_document(
         List(HTML.title("Isabelle build status")),
         List(HTML.chapter("Isabelle build status"),
-          HTML.itemize(data.entries.map({ case data_entry =>
-            List(HTML.link(clean_name(data_entry.name) + "/index.html", HTML.text(data_entry.name)))
-          })))))
+          HTML.par(
+            List(HTML.itemize(
+              List(HTML.bold(HTML.text("status date: ")) :: HTML.text(data.date.toString))))),
+          HTML.par(
+            List(HTML.itemize(data.entries.map({ case data_entry =>
+              List(HTML.link(clean_name(data_entry.name) + "/index.html",
+                HTML.text(data_entry.name))) })))))))
 
     for (data_entry <- data.entries) {
       val data_name = data_entry.name
@@ -280,8 +284,8 @@
           HTML.par(
             List(HTML.itemize(
               List(
-                HTML.bold(HTML.text("build host: ")) :: HTML.text(commas(data_entry.hosts)),
-                HTML.bold(HTML.text("status date: ")) :: HTML.text(data.date.toString))))) ::
+                HTML.bold(HTML.text("status date: ")) :: HTML.text(data.date.toString),
+                HTML.bold(HTML.text("build host: ")) :: HTML.text(commas(data_entry.hosts)))))) ::
           HTML.par(
             List(HTML.itemize(
               data_entry.sessions.map(session =>
@@ -292,6 +296,8 @@
               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))) ::