src/Pure/Admin/build_status.scala
changeset 65942 864a4892e43c
parent 65941 316c30b60ebc
child 65943 bf55ad5eaf75
     1.1 --- a/src/Pure/Admin/build_status.scala	Sat May 27 00:30:48 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Sat May 27 12:33:14 2017 +0200
     1.3 @@ -110,9 +110,9 @@
     1.4        if (errors.isEmpty) HTML.text(name + " (" + isabelle_version + ")")
     1.5        else {
     1.6          val tooltip_errors =
     1.7 -          errors.map(msg => HTML.pre(HTML.text(Symbol.decode(msg))) + HTML.error_message_class)
     1.8 -        val tooltip = List(HTML.div(tooltip_errors) + HTML.tooltip_class)
     1.9 -        HTML.span(HTML.text(name) ::: tooltip) + HTML.error_class ::
    1.10 +          errors.map(msg => HTML.error_message_class(HTML.pre(HTML.text(Symbol.decode(msg)))))
    1.11 +        val tooltip = List(HTML.tooltip_class(HTML.div(tooltip_errors)))
    1.12 +        HTML.error_class(HTML.span(HTML.text(name) ::: tooltip)) ::
    1.13          HTML.text(" (" + isabelle_version + ")")
    1.14        }
    1.15    }
    1.16 @@ -277,7 +277,7 @@
    1.17                case Nil => Nil
    1.18                case sessions =>
    1.19                  HTML.break :::
    1.20 -                List(HTML.span(HTML.text("Failed sessions:")) + HTML.error_message_class) :::
    1.21 +                List(HTML.error_message_class(HTML.span(HTML.text("Failed sessions:")))) :::
    1.22                  List(HTML.itemize(sessions.map(s => s.head.present_errors(s.name))))
    1.23              })
    1.24            }))))))
    1.25 @@ -420,7 +420,7 @@
    1.26                HTML.text(" (" + session.head.timing.message_resources + ")"))))) ::
    1.27          data_entry.sessions.flatMap(session =>
    1.28            List(
    1.29 -            HTML.section(session.name) + HTML.id("session_" + session.name),
    1.30 +            HTML.id("session_" + session.name)(HTML.section(session.name)),
    1.31              HTML.par(
    1.32                HTML.description(
    1.33                  List(
    1.34 @@ -437,9 +437,8 @@
    1.35                  proper_string(session.head.afp_version).map(s =>
    1.36                    HTML.text("AFP version:") -> HTML.text(s)).toList) ::
    1.37                session_plots.getOrElse(session.name, Nil).map(image =>
    1.38 -                HTML.image(image.name) +
    1.39 -                  HTML.width(image.width / 2) +
    1.40 -                  HTML.height(image.height / 2))))))
    1.41 +                HTML.width(image.width / 2)(HTML.height(image.height / 2)(
    1.42 +                  HTML.image(image.name))))))))
    1.43      }
    1.44    }
    1.45