tuned signature;
authorwenzelm
Sat May 27 12:36:27 2017 +0200 (2017-05-27)
changeset 65943bf55ad5eaf75
parent 65942 864a4892e43c
child 65944 79e4d94aa9ad
tuned signature;
src/Pure/Admin/build_status.scala
src/Pure/Thy/html.scala
     1.1 --- a/src/Pure/Admin/build_status.scala	Sat May 27 12:33:14 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Sat May 27 12:36:27 2017 +0200
     1.3 @@ -110,9 +110,9 @@
     1.4        if (errors.isEmpty) HTML.text(name + " (" + isabelle_version + ")")
     1.5        else {
     1.6          val tooltip_errors =
     1.7 -          errors.map(msg => HTML.error_message_class(HTML.pre(HTML.text(Symbol.decode(msg)))))
     1.8 +          errors.map(msg => HTML.error_message(HTML.pre(HTML.text(Symbol.decode(msg)))))
     1.9          val tooltip = List(HTML.tooltip_class(HTML.div(tooltip_errors)))
    1.10 -        HTML.error_class(HTML.span(HTML.text(name) ::: tooltip)) ::
    1.11 +        HTML.error(HTML.span(HTML.text(name) ::: tooltip)) ::
    1.12          HTML.text(" (" + isabelle_version + ")")
    1.13        }
    1.14    }
    1.15 @@ -277,7 +277,7 @@
    1.16                case Nil => Nil
    1.17                case sessions =>
    1.18                  HTML.break :::
    1.19 -                List(HTML.error_message_class(HTML.span(HTML.text("Failed sessions:")))) :::
    1.20 +                List(HTML.error_message(HTML.span(HTML.text("Failed sessions:")))) :::
    1.21                  List(HTML.itemize(sessions.map(s => s.head.present_errors(s.name))))
    1.22              })
    1.23            }))))))
     2.1 --- a/src/Pure/Thy/html.scala	Sat May 27 12:33:14 2017 +0200
     2.2 +++ b/src/Pure/Thy/html.scala	Sat May 27 12:36:27 2017 +0200
     2.3 @@ -146,14 +146,14 @@
     2.4    /* messages */
     2.5  
     2.6    // background
     2.7 -  val writeln_message_class: Attribute = css_class("writeln_message")
     2.8 -  val warning_message_class: Attribute = css_class("warning_message")
     2.9 -  val error_message_class: Attribute = css_class("error_message")
    2.10 +  val writeln_message: Attribute = css_class("writeln_message")
    2.11 +  val warning_message: Attribute = css_class("warning_message")
    2.12 +  val error_message: Attribute = css_class("error_message")
    2.13  
    2.14    // underline
    2.15 -  val writeln_class: Attribute = css_class("writeln")
    2.16 -  val warning_class: Attribute = css_class("warning")
    2.17 -  val error_class: Attribute = css_class("error")
    2.18 +  val writeln: Attribute = css_class("writeln")
    2.19 +  val warning: Attribute = css_class("warning")
    2.20 +  val error: Attribute = css_class("error")
    2.21  
    2.22    // tooltips
    2.23    val tooltip_class: Attribute = css_class("tooltip")