src/Pure/Admin/build_status.scala
changeset 65794 a880f41a8d0f
parent 65792 c58752102b34
child 65795 c60b1a2c3abc
     1.1 --- a/src/Pure/Admin/build_status.scala	Tue May 09 21:06:11 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Tue May 09 21:25:32 2017 +0200
     1.3 @@ -180,9 +180,13 @@
     1.4        HTML.output_document(
     1.5          List(HTML.title("Isabelle build status")),
     1.6          List(HTML.chapter("Isabelle build status"),
     1.7 -          HTML.itemize(data.entries.map({ case data_entry =>
     1.8 -            List(HTML.link(clean_name(data_entry.name) + "/index.html", HTML.text(data_entry.name)))
     1.9 -          })))))
    1.10 +          HTML.par(
    1.11 +            List(HTML.itemize(
    1.12 +              List(HTML.bold(HTML.text("status date: ")) :: HTML.text(data.date.toString))))),
    1.13 +          HTML.par(
    1.14 +            List(HTML.itemize(data.entries.map({ case data_entry =>
    1.15 +              List(HTML.link(clean_name(data_entry.name) + "/index.html",
    1.16 +                HTML.text(data_entry.name))) })))))))
    1.17  
    1.18      for (data_entry <- data.entries) {
    1.19        val data_name = data_entry.name
    1.20 @@ -280,8 +284,8 @@
    1.21            HTML.par(
    1.22              List(HTML.itemize(
    1.23                List(
    1.24 -                HTML.bold(HTML.text("build host: ")) :: HTML.text(commas(data_entry.hosts)),
    1.25 -                HTML.bold(HTML.text("status date: ")) :: HTML.text(data.date.toString))))) ::
    1.26 +                HTML.bold(HTML.text("status date: ")) :: HTML.text(data.date.toString),
    1.27 +                HTML.bold(HTML.text("build host: ")) :: HTML.text(commas(data_entry.hosts)))))) ::
    1.28            HTML.par(
    1.29              List(HTML.itemize(
    1.30                data_entry.sessions.map(session =>
    1.31 @@ -292,6 +296,8 @@
    1.32                HTML.section(session.name) + HTML.id("session_" + session.name),
    1.33                HTML.par(
    1.34                  HTML.itemize(List(
    1.35 +                  HTML.bold(HTML.text("status date: ")) :: HTML.text(data.date.toString),
    1.36 +                  HTML.bold(HTML.text("build host: ")) :: HTML.text(commas(data_entry.hosts)),
    1.37                    HTML.bold(HTML.text("timing: ")) :: HTML.text(session.timing.message_resources),
    1.38                    HTML.bold(HTML.text("ML timing: ")) ::
    1.39                      HTML.text(session.ml_timing.message_resources))) ::