# HG changeset patch
# User wenzelm
# Date 1494790476 -7200
# Node ID 5ec49735163689c34159ec40e5be11741b30b9e5
# Parent  67a6e0f166c2449f15652bd09541f5bd8a88598e
prefer logical markup;

diff -r 67a6e0f166c2 -r 5ec497351636 src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Sun May 14 20:36:51 2017 +0200
+++ b/src/Pure/Admin/build_status.scala	Sun May 14 21:34:36 2017 +0200
@@ -209,8 +209,8 @@
         List(HTML.title("Isabelle build status")),
         List(HTML.chapter("Isabelle build status"),
           HTML.par(
-            List(HTML.itemize(
-              List(HTML.bold(HTML.text("status date: ")) :: HTML.text(data.date.toString))))),
+            List(HTML.description(
+              List(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",
@@ -313,10 +313,10 @@
           List(HTML.title("Isabelle build status for " + data_name)),
           HTML.chapter("Isabelle build status for " + data_name) ::
           HTML.par(
-            List(HTML.itemize(
+            List(HTML.description(
               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.text("status date:") -> HTML.text(data.date.toString),
+                HTML.text("build host:") -> HTML.text(commas(data_entry.hosts)))))) ::
           HTML.par(
             List(HTML.itemize(
               data_entry.sessions.map(session =>
@@ -326,14 +326,14 @@
             List(
               HTML.section(session.name) + HTML.id("session_" + session.name),
               HTML.par(
-                HTML.itemize(List(
-                  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.description(
+                  List(
+                    HTML.text("timing:") -> HTML.text(session.timing.message_resources),
+                    HTML.text("ML timing:") -> HTML.text(session.ml_timing.message_resources)) :::
                   proper_string(session.isabelle_version).map(s =>
-                    HTML.bold(HTML.text("Isabelle version: ")) :: HTML.text(s)).toList :::
+                    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) ::
+                    HTML.text("AFP version:") -> HTML.text(s)).toList) ::
                 session_plots.getOrElse(session.name, Nil).map(plot_name =>
                   HTML.image(plot_name) +
                     HTML.width(image_width / 2) +