--- a/src/Pure/Admin/build_status.scala Sat May 27 12:33:14 2017 +0200
+++ b/src/Pure/Admin/build_status.scala Sat May 27 12:36:27 2017 +0200
@@ -110,9 +110,9 @@
if (errors.isEmpty) HTML.text(name + " (" + isabelle_version + ")")
else {
val tooltip_errors =
- errors.map(msg => HTML.error_message_class(HTML.pre(HTML.text(Symbol.decode(msg)))))
+ errors.map(msg => HTML.error_message(HTML.pre(HTML.text(Symbol.decode(msg)))))
val tooltip = List(HTML.tooltip_class(HTML.div(tooltip_errors)))
- HTML.error_class(HTML.span(HTML.text(name) ::: tooltip)) ::
+ HTML.error(HTML.span(HTML.text(name) ::: tooltip)) ::
HTML.text(" (" + isabelle_version + ")")
}
}
@@ -277,7 +277,7 @@
case Nil => Nil
case sessions =>
HTML.break :::
- List(HTML.error_message_class(HTML.span(HTML.text("Failed sessions:")))) :::
+ List(HTML.error_message(HTML.span(HTML.text("Failed sessions:")))) :::
List(HTML.itemize(sessions.map(s => s.head.present_errors(s.name))))
})
}))))))