# HG changeset patch
# User wenzelm
# Date 1495400266 -7200
# Node ID bbad8162d6786cd46a2f8524bbedb18bcde7f77e
# Parent  5869111183177d958572f7b7064c551817415674
clarified signature;

diff -r 586911118317 -r bbad8162d678 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Sun May 21 21:36:31 2017 +0200
+++ b/src/Pure/Thy/html.scala	Sun May 21 22:57:46 2017 +0200
@@ -92,6 +92,7 @@
   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)
 
 
   /* structured markup operators */
@@ -105,9 +106,6 @@
   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")
@@ -124,13 +122,6 @@
   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", _)))
 
@@ -147,6 +138,21 @@
     XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil)
 
 
+  /* messages */
+
+  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")
+
+  def writeln_message(msg: String): XML.Elem = par(text(msg)) + writeln_message_class
+  def warning_message(msg: String): XML.Elem = par(text(msg)) + warning_message_class
+  def error_message(msg: String): XML.Elem = par(text(msg)) + error_message_class
+
+  def writeln_message_span(msg: String): XML.Elem = span(text(msg)) + writeln_message_class
+  def warning_message_span(msg: String): XML.Elem = span(text(msg)) + warning_message_class
+  def error_message_span(msg: String): XML.Elem = span(text(msg)) + error_message_class
+
+
   /* document */
 
   val header: String =