# HG changeset patch
# User wenzelm
# Date 1496323190 -7200
# Node ID 50daca61efd6f9d0bedaaa1a5acf0cbe24d74785
# Parent  fa787e233214d431568731bc4044a0e58fe8ab6d
tuned signature;

diff -r fa787e233214 -r 50daca61efd6 src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Thu Jun 01 12:27:20 2017 +0200
+++ b/src/Pure/Admin/build_status.scala	Thu Jun 01 15:19:50 2017 +0200
@@ -273,7 +273,7 @@
               case Nil => Nil
               case sessions =>
                 HTML.break :::
-                List(HTML.error_message(HTML.span(HTML.text("Failed sessions:")))) :::
+                List(HTML.span(HTML.error_message, HTML.text("Failed sessions:"))) :::
                 List(HTML.itemize(sessions.map(s => s.head.present_errors(s.name))))
             })
           }))))))
@@ -416,7 +416,7 @@
               HTML.text(" (" + session.head.timing.message_resources + ")"))))) ::
         data_entry.sessions.flatMap(session =>
           List(
-            HTML.id("session_" + session.name)(HTML.section(session.name)),
+            HTML.section(HTML.id("session_" + session.name), session.name),
             HTML.par(
               HTML.description(
                 List(
diff -r fa787e233214 -r 50daca61efd6 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Thu Jun 01 12:27:20 2017 +0200
+++ b/src/Pure/Thy/html.scala	Thu Jun 01 15:19:50 2017 +0200
@@ -82,14 +82,17 @@
 
   /* attributes */
 
-  class Attribute(name: String, value: String)
-  { def apply(elem: XML.Elem): XML.Elem = elem + (name -> value) }
+  class Attribute(val name: String, value: String)
+  {
+    def xml: XML.Attribute = name -> value
+    def apply(elem: XML.Elem): XML.Elem = elem + xml
+  }
 
-  def id(s: String) = new Attribute("id", s)
-  def css_class(name: String) = new Attribute("class", name)
+  def id(s: String): Attribute = new Attribute("id", s)
+  def css_class(name: String): Attribute = new Attribute("class", name)
 
-  def width(w: Int) = new Attribute("width", w.toString)
-  def height(h: Int) = new Attribute("height", h.toString)
+  def width(w: Int): Attribute = new Attribute("width", w.toString)
+  def height(h: Int): Attribute = new Attribute("height", h.toString)
   def size(w: Int, h: Int)(elem: XML.Elem): XML.Elem = width(w)(height(h)(elem))
 
 
@@ -98,11 +101,19 @@
   def text(txt: String): XML.Body = if (txt.isEmpty) Nil else List(XML.Text(txt))
   val break: XML.Body = List(XML.elem("br"))
 
-  class Operator(name: String)
-  { def apply(body: XML.Body): XML.Elem = XML.elem(name, body) }
+  class Operator(val name: String)
+  {
+    def apply(body: XML.Body): XML.Elem = XML.elem(name, body)
+    def apply(att: Attribute, body: XML.Body): XML.Elem = att(apply(body))
+    def apply(c: String, body: XML.Body): XML.Elem = apply(css_class(c), body)
+  }
 
   class Heading(name: String) extends Operator(name)
-  { def apply(txt: String): XML.Elem = super.apply(text(txt)) }
+  {
+    def apply(txt: String): XML.Elem = super.apply(text(txt))
+    def apply(att: Attribute, txt: String): XML.Elem = super.apply(att, text(txt))
+    def apply(c: String, txt: String): XML.Elem = super.apply(c, text(txt))
+  }
 
   val div = new Operator("div")
   val span = new Operator("span")
@@ -135,7 +146,7 @@
   def image(src: String, alt: String = ""): XML.Elem =
     XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil)
 
-  def source(src: String): XML.Elem = css_class("source")(div(List(pre(text(src)))))
+  def source(src: String): XML.Elem = div("source", List(pre(text(src))))
 
   def style(s: String): XML.Elem = XML.elem("style", text(s))
 
@@ -156,7 +167,7 @@
   /* tooltips */
 
   def tooltip(item: XML.Body, tip: XML.Body): XML.Elem =
-    span(item ::: List(css_class("tooltip")(div(tip))))
+    span(item ::: List(div("tooltip", tip)))
 
   def tooltip_errors(item: XML.Body, msgs: List[XML.Body]): XML.Elem =
     HTML.error(tooltip(item, msgs.map(msg => error_message(pre(msg)))))
diff -r fa787e233214 -r 50daca61efd6 src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Thu Jun 01 12:27:20 2017 +0200
+++ b/src/Pure/Thy/present.scala	Thu Jun 01 15:19:50 2017 +0200
@@ -52,12 +52,12 @@
       HTML.chapter(title) ::
        (if (sessions.isEmpty) Nil
         else
-          List(HTML.css_class("sessions")(HTML.div(List(
-            HTML.description(
+          List(HTML.div("sessions",
+            List(HTML.description(
               sessions.map({ case (name, description) =>
                 (List(HTML.link(name + "/index.html", HTML.text(name))),
                   if (description == "") Nil
-                  else List(HTML.pre(HTML.text(description)))) }))))))))
+                  else List(HTML.pre(HTML.text(description)))) })))))))
   }
 
   def make_global_index(browser_info: Path)