diff -r 1b004f5974af -r 586911118317 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Sun May 21 21:43:00 2017 +0200
+++ b/src/Pure/Thy/html.scala	Sun May 21 21:36:31 2017 +0200
@@ -105,6 +105,9 @@
   class Heading(name: String) extends Operator(name)
   { def apply(txt: String): XML.Elem = super.apply(text(txt)) }
 
+  class Span(class_name: String)
+  { def apply(body: XML.Body): XML.Elem = XML.elem("span", body) + ("class" -> class_name) }
+
   val div = new Operator("div")
   val span = new Operator("span")
   val pre = new Operator("pre")
@@ -121,6 +124,13 @@
   val paragraph = new Heading("h5")
   val subparagraph = new Heading("h6")
 
+  val writeln_message = new Span("writeln_message")
+  val information_message = new Span("information_message")
+  val tracing_message = new Span("tracing_message")
+  val warning_message = new Span("warning_message")
+  val legacy_message = new Span("legacy_message")
+  val error_message = new Span("error_message")
+
   def itemize(items: List[XML.Body]): XML.Elem =
     XML.elem("ul", items.map(XML.elem("li", _)))