# HG changeset patch
# User wenzelm
# Date 1495881387 -7200
# Node ID bf55ad5eaf75448d5cdb301787f9c0ca1dfca9a9
# Parent  864a4892e43c5bd952a10d381a52c20de6c94708
tuned signature;

diff -r 864a4892e43c -r bf55ad5eaf75 src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Sat May 27 12:33:14 2017 +0200
+++ b/src/Pure/Admin/build_status.scala	Sat May 27 12:36:27 2017 +0200
@@ -110,9 +110,9 @@
       if (errors.isEmpty) HTML.text(name + " (" + isabelle_version + ")")
       else {
         val tooltip_errors =
-          errors.map(msg => HTML.error_message_class(HTML.pre(HTML.text(Symbol.decode(msg)))))
+          errors.map(msg => HTML.error_message(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.error(HTML.span(HTML.text(name) ::: tooltip)) ::
         HTML.text(" (" + isabelle_version + ")")
       }
   }
@@ -277,7 +277,7 @@
               case Nil => Nil
               case sessions =>
                 HTML.break :::
-                List(HTML.error_message_class(HTML.span(HTML.text("Failed sessions:")))) :::
+                List(HTML.error_message(HTML.span(HTML.text("Failed sessions:")))) :::
                 List(HTML.itemize(sessions.map(s => s.head.present_errors(s.name))))
             })
           }))))))
diff -r 864a4892e43c -r bf55ad5eaf75 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Sat May 27 12:33:14 2017 +0200
+++ b/src/Pure/Thy/html.scala	Sat May 27 12:36:27 2017 +0200
@@ -146,14 +146,14 @@
   /* messages */
 
   // background
-  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")
+  val writeln_message: Attribute = css_class("writeln_message")
+  val warning_message: Attribute = css_class("warning_message")
+  val error_message: Attribute = css_class("error_message")
 
   // underline
-  val writeln_class: Attribute = css_class("writeln")
-  val warning_class: Attribute = css_class("warning")
-  val error_class: Attribute = css_class("error")
+  val writeln: Attribute = css_class("writeln")
+  val warning: Attribute = css_class("warning")
+  val error: Attribute = css_class("error")
 
   // tooltips
   val tooltip_class: Attribute = css_class("tooltip")