src/Pure/Admin/build_status.scala
changeset 65835 5ec497351636
parent 65804 73ed0ebac3b0
child 65836 3b4877fbd9cb
     1.1 --- a/src/Pure/Admin/build_status.scala	Sun May 14 20:36:51 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Sun May 14 21:34:36 2017 +0200
     1.3 @@ -209,8 +209,8 @@
     1.4          List(HTML.title("Isabelle build status")),
     1.5          List(HTML.chapter("Isabelle build status"),
     1.6            HTML.par(
     1.7 -            List(HTML.itemize(
     1.8 -              List(HTML.bold(HTML.text("status date: ")) :: HTML.text(data.date.toString))))),
     1.9 +            List(HTML.description(
    1.10 +              List(HTML.text("status date:") -> HTML.text(data.date.toString))))),
    1.11            HTML.par(
    1.12              List(HTML.itemize(data.entries.map({ case data_entry =>
    1.13                List(HTML.link(clean_name(data_entry.name) + "/index.html",
    1.14 @@ -313,10 +313,10 @@
    1.15            List(HTML.title("Isabelle build status for " + data_name)),
    1.16            HTML.chapter("Isabelle build status for " + data_name) ::
    1.17            HTML.par(
    1.18 -            List(HTML.itemize(
    1.19 +            List(HTML.description(
    1.20                List(
    1.21 -                HTML.bold(HTML.text("status date: ")) :: HTML.text(data.date.toString),
    1.22 -                HTML.bold(HTML.text("build host: ")) :: HTML.text(commas(data_entry.hosts)))))) ::
    1.23 +                HTML.text("status date:") -> HTML.text(data.date.toString),
    1.24 +                HTML.text("build host:") -> HTML.text(commas(data_entry.hosts)))))) ::
    1.25            HTML.par(
    1.26              List(HTML.itemize(
    1.27                data_entry.sessions.map(session =>
    1.28 @@ -326,14 +326,14 @@
    1.29              List(
    1.30                HTML.section(session.name) + HTML.id("session_" + session.name),
    1.31                HTML.par(
    1.32 -                HTML.itemize(List(
    1.33 -                  HTML.bold(HTML.text("timing: ")) :: HTML.text(session.timing.message_resources),
    1.34 -                  HTML.bold(HTML.text("ML timing: ")) ::
    1.35 -                    HTML.text(session.ml_timing.message_resources)) :::
    1.36 +                HTML.description(
    1.37 +                  List(
    1.38 +                    HTML.text("timing:") -> HTML.text(session.timing.message_resources),
    1.39 +                    HTML.text("ML timing:") -> HTML.text(session.ml_timing.message_resources)) :::
    1.40                    proper_string(session.isabelle_version).map(s =>
    1.41 -                    HTML.bold(HTML.text("Isabelle version: ")) :: HTML.text(s)).toList :::
    1.42 +                    HTML.text("Isabelle version:") -> HTML.text(s)).toList :::
    1.43                    proper_string(session.afp_version).map(s =>
    1.44 -                    HTML.bold(HTML.text("AFP version: ")) :: HTML.text(s)).toList) ::
    1.45 +                    HTML.text("AFP version:") -> HTML.text(s)).toList) ::
    1.46                  session_plots.getOrElse(session.name, Nil).map(plot_name =>
    1.47                    HTML.image(plot_name) +
    1.48                      HTML.width(image_width / 2) +