--- 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; }
--- 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", _)))