--- 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 */