# HG changeset patch
# User wenzelm
# Date 1495395391 -7200
# Node ID 5869111183177d958572f7b7064c551817415674
# Parent  1b004f5974af4df47923959ef43189f36df7eade
HTML rendering based on Isabelle/jEdit colors;

diff -r 1b004f5974af -r 586911118317 etc/isabelle.css
--- a/etc/isabelle.css	Sun May 21 21:43:00 2017 +0200
+++ b/etc/isabelle.css	Sun May 21 21:36:31 2017 +0200
@@ -75,3 +75,13 @@
 .comment        { color: #CC0000; }
 .improper       { color: #FF5050; }
 .bad            { background-color: #FF6A6A; }
+
+
+/* message background */
+
+.writeln_message      { background-color: #F0F0F0; }
+.information_message  { background-color: #DCEAF3; }
+.tracing_message      { background-color: #F0F8FF; }
+.warning_message      { background-color: #EEE8AA; }
+.legacy_message       { background-color: #EEE8AA; }
+.error_message        { background-color: #FFC1C1; }
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", _)))