--- a/src/Pure/Admin/build_status.scala Sat May 27 12:36:27 2017 +0200
+++ b/src/Pure/Admin/build_status.scala Sat May 27 12:52:36 2017 +0200
@@ -109,11 +109,8 @@
def present_errors(name: String): XML.Body =
if (errors.isEmpty) HTML.text(name + " (" + isabelle_version + ")")
else {
- val tooltip_errors =
- 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(HTML.span(HTML.text(name) ::: tooltip)) ::
- HTML.text(" (" + isabelle_version + ")")
+ HTML.tooltip_errors(HTML.text(name), errors.map(s => HTML.text(Symbol.decode(s)))) ::
+ HTML.text(" (" + isabelle_version + ")")
}
}