tuned signature;
authorwenzelm
Sat May 27 12:52:36 2017 +0200 (2017-05-27)
changeset 6594479e4d94aa9ad
parent 65943 bf55ad5eaf75
child 65945 35652d0834f4
tuned signature;
src/Pure/Admin/build_status.scala
src/Pure/Thy/html.scala
     1.1 --- a/src/Pure/Admin/build_status.scala	Sat May 27 12:36:27 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Sat May 27 12:52:36 2017 +0200
     1.3 @@ -109,11 +109,8 @@
     1.4      def present_errors(name: String): XML.Body =
     1.5        if (errors.isEmpty) HTML.text(name + " (" + isabelle_version + ")")
     1.6        else {
     1.7 -        val tooltip_errors =
     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(HTML.span(HTML.text(name) ::: tooltip)) ::
    1.11 -        HTML.text(" (" + isabelle_version + ")")
    1.12 +        HTML.tooltip_errors(HTML.text(name), errors.map(s => HTML.text(Symbol.decode(s)))) ::
    1.13 +          HTML.text(" (" + isabelle_version + ")")
    1.14        }
    1.15    }
    1.16  
     2.1 --- a/src/Pure/Thy/html.scala	Sat May 27 12:36:27 2017 +0200
     2.2 +++ b/src/Pure/Thy/html.scala	Sat May 27 12:52:36 2017 +0200
     2.3 @@ -155,8 +155,14 @@
     2.4    val warning: Attribute = css_class("warning")
     2.5    val error: Attribute = css_class("error")
     2.6  
     2.7 -  // tooltips
     2.8 -  val tooltip_class: Attribute = css_class("tooltip")
     2.9 +
    2.10 +  /* tooltips */
    2.11 +
    2.12 +  def tooltip(item: XML.Body, tip: XML.Body): XML.Elem =
    2.13 +    span(item ::: List(css_class("tooltip")(div(tip))))
    2.14 +
    2.15 +  def tooltip_errors(item: XML.Body, msgs: List[XML.Body]): XML.Elem =
    2.16 +    HTML.error(tooltip(item, msgs.map(msg => error_message(pre(msg)))))
    2.17  
    2.18  
    2.19    /* document */