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