more HTML output;
authorwenzelm
Sun, 07 May 2017 16:31:39 +0200
changeset 65755 21b4bfa6d204
parent 65754 05c6a29c9132
child 65756 2c6b5dd59db3
more HTML output;
src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Sun May 07 16:14:49 2017 +0200
+++ b/src/Pure/Admin/build_status.scala	Sun May 07 16:31:39 2017 +0200
@@ -225,9 +225,15 @@
               HTML.text(" (" + entries.head.timing.message_resources + ")") })) ::
           sessions.flatMap({ case (name, entries) =>
             List(
-              HTML.section(name + " (" + entries.head.timing.message_resources + ")") +
-                HTML.id("session_" + name),
-              HTML.par(List(HTML.image(name + ".png")))) })))
+              HTML.section(name) + HTML.id("session_" + name),
+              HTML.par(
+                List(
+                  HTML.itemize(List(
+                    HTML.bold(HTML.text("last timing: ")) ::
+                      HTML.text(entries.head.timing.message_resources),
+                    HTML.bold(HTML.text("last ML timing: ")) ::
+                      HTML.text(entries.head.ml_timing.message_resources))),
+                  HTML.image(name + ".png")))) })))
     }
 
     val heading = "Build status (" + data.date + ")"