# HG changeset patch
# User wenzelm
# Date 1495882356 -7200
# Node ID 79e4d94aa9ad3e18e0334d5a871a669adac6f4c9
# Parent  bf55ad5eaf75448d5cdb301787f9c0ca1dfca9a9
tuned signature;

diff -r bf55ad5eaf75 -r 79e4d94aa9ad src/Pure/Admin/build_status.scala
--- 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 + ")")
       }
   }
 
diff -r bf55ad5eaf75 -r 79e4d94aa9ad src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Sat May 27 12:36:27 2017 +0200
+++ b/src/Pure/Thy/html.scala	Sat May 27 12:52:36 2017 +0200
@@ -155,8 +155,14 @@
   val warning: Attribute = css_class("warning")
   val error: Attribute = css_class("error")
 
-  // tooltips
-  val tooltip_class: Attribute = css_class("tooltip")
+
+  /* tooltips */
+
+  def tooltip(item: XML.Body, tip: XML.Body): XML.Elem =
+    span(item ::: List(css_class("tooltip")(div(tip))))
+
+  def tooltip_errors(item: XML.Body, msgs: List[XML.Body]): XML.Elem =
+    HTML.error(tooltip(item, msgs.map(msg => error_message(pre(msg)))))
 
 
   /* document */