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