# HG changeset patch
# User wenzelm
# Date 1495881194 -7200
# Node ID 864a4892e43c5bd952a10d381a52c20de6c94708
# Parent  316c30b60ebc331c0e39491bf16f2db7e27fe8ef
clarified signature;

diff -r 316c30b60ebc -r 864a4892e43c src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Sat May 27 00:30:48 2017 +0200
+++ b/src/Pure/Admin/build_status.scala	Sat May 27 12:33:14 2017 +0200
@@ -110,9 +110,9 @@
       if (errors.isEmpty) HTML.text(name + " (" + isabelle_version + ")")
       else {
         val tooltip_errors =
-          errors.map(msg => HTML.pre(HTML.text(Symbol.decode(msg))) + HTML.error_message_class)
-        val tooltip = List(HTML.div(tooltip_errors) + HTML.tooltip_class)
-        HTML.span(HTML.text(name) ::: tooltip) + HTML.error_class ::
+          errors.map(msg => HTML.error_message_class(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.text(" (" + isabelle_version + ")")
       }
   }
@@ -277,7 +277,7 @@
               case Nil => Nil
               case sessions =>
                 HTML.break :::
-                List(HTML.span(HTML.text("Failed sessions:")) + HTML.error_message_class) :::
+                List(HTML.error_message_class(HTML.span(HTML.text("Failed sessions:")))) :::
                 List(HTML.itemize(sessions.map(s => s.head.present_errors(s.name))))
             })
           }))))))
@@ -420,7 +420,7 @@
               HTML.text(" (" + session.head.timing.message_resources + ")"))))) ::
         data_entry.sessions.flatMap(session =>
           List(
-            HTML.section(session.name) + HTML.id("session_" + session.name),
+            HTML.id("session_" + session.name)(HTML.section(session.name)),
             HTML.par(
               HTML.description(
                 List(
@@ -437,9 +437,8 @@
                 proper_string(session.head.afp_version).map(s =>
                   HTML.text("AFP version:") -> HTML.text(s)).toList) ::
               session_plots.getOrElse(session.name, Nil).map(image =>
-                HTML.image(image.name) +
-                  HTML.width(image.width / 2) +
-                  HTML.height(image.height / 2))))))
+                HTML.width(image.width / 2)(HTML.height(image.height / 2)(
+                  HTML.image(image.name))))))))
     }
   }
 
diff -r 316c30b60ebc -r 864a4892e43c src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Sat May 27 00:30:48 2017 +0200
+++ b/src/Pure/Thy/html.scala	Sat May 27 12:33:14 2017 +0200
@@ -89,10 +89,13 @@
 
   /* attributes */
 
-  def id(s: String): XML.Attribute = ("id" -> s)
-  def width(w: Int): XML.Attribute = ("width" -> w.toString)
-  def height(h: Int): XML.Attribute = ("height" -> h.toString)
-  def css_class(name: String): XML.Attribute = ("class" -> name)
+  class Attribute(name: String, value: String)
+  { def apply(elem: XML.Elem): XML.Elem = elem + (name -> value) }
+
+  def id(s: String) = new Attribute("id", s)
+  def width(w: Int) = new Attribute("width", w.toString)
+  def height(h: Int) = new Attribute("height", h.toString)
+  def css_class(name: String) = new Attribute("class", name)
 
 
   /* structured markup operators */
@@ -143,17 +146,17 @@
   /* messages */
 
   // background
-  val writeln_message_class: XML.Attribute = css_class("writeln_message")
-  val warning_message_class: XML.Attribute = css_class("warning_message")
-  val error_message_class: XML.Attribute = css_class("error_message")
+  val writeln_message_class: Attribute = css_class("writeln_message")
+  val warning_message_class: Attribute = css_class("warning_message")
+  val error_message_class: Attribute = css_class("error_message")
 
   // underline
-  val writeln_class: XML.Attribute = css_class("writeln")
-  val warning_class: XML.Attribute = css_class("warning")
-  val error_class: XML.Attribute = css_class("error")
+  val writeln_class: Attribute = css_class("writeln")
+  val warning_class: Attribute = css_class("warning")
+  val error_class: Attribute = css_class("error")
 
   // tooltips
-  val tooltip_class: XML.Attribute = css_class("tooltip")
+  val tooltip_class: Attribute = css_class("tooltip")
 
 
   /* document */