--- 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))))
})
}))))))
--- 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")