src/Pure/Admin/build_status.scala
changeset 65943 bf55ad5eaf75
parent 65942 864a4892e43c
child 65944 79e4d94aa9ad
     1.1 --- a/src/Pure/Admin/build_status.scala	Sat May 27 12:33:14 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Sat May 27 12:36:27 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.error_message_class(HTML.pre(HTML.text(Symbol.decode(msg)))))
     1.8 +          errors.map(msg => HTML.error_message(HTML.pre(HTML.text(Symbol.decode(msg)))))
     1.9          val tooltip = List(HTML.tooltip_class(HTML.div(tooltip_errors)))
    1.10 -        HTML.error_class(HTML.span(HTML.text(name) ::: tooltip)) ::
    1.11 +        HTML.error(HTML.span(HTML.text(name) ::: tooltip)) ::
    1.12          HTML.text(" (" + isabelle_version + ")")
    1.13        }
    1.14    }
    1.15 @@ -277,7 +277,7 @@
    1.16                case Nil => Nil
    1.17                case sessions =>
    1.18                  HTML.break :::
    1.19 -                List(HTML.error_message_class(HTML.span(HTML.text("Failed sessions:")))) :::
    1.20 +                List(HTML.error_message(HTML.span(HTML.text("Failed sessions:")))) :::
    1.21                  List(HTML.itemize(sessions.map(s => s.head.present_errors(s.name))))
    1.22              })
    1.23            }))))))