1.1 --- a/src/Pure/General/markup.scala	Sat Jun 25 18:29:51 2011 +0200
     1.2 +++ b/src/Pure/General/markup.scala	Sat Jun 25 19:19:13 2011 +0200
     1.3 @@ -147,7 +147,7 @@
     1.4  
     1.5    /* logical entities */
     1.6  
     1.7 -  val TCLASS = "tclass"
     1.8 +  val CLASS = "class"
     1.9    val TYCON = "tycon"
    1.10    val FIXED = "fixed"
    1.11    val CONST = "constant"
    1.12 @@ -289,7 +289,6 @@
    1.13    val Serial = new Long_Property("serial")
    1.14  
    1.15    val MESSAGE = "message"
    1.16 -  val CLASS = "class"
    1.17  
    1.18    val INIT = "init"
    1.19    val STATUS = "status"

     2.1 --- a/src/Tools/jEdit/src/html_panel.scala	Sat Jun 25 18:29:51 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/html_panel.scala	Sat Jun 25 19:19:13 2011 +0200
     2.3 @@ -168,7 +168,7 @@
     2.4          current_body.flatMap(div =>
     2.5            Pretty.formatted(List(div), current_margin, Pretty.font_metric(current_font_metrics))
     2.6              .map(t =>
     2.7 -              XML.Elem(Markup(HTML.PRE, List((Markup.CLASS, Markup.MESSAGE))),
     2.8 +              XML.Elem(Markup(HTML.PRE, List((HTML.CLASS, Markup.MESSAGE))),
     2.9                  HTML.spans(system.symbols, t, true))))
    2.10        val doc =
    2.11          builder.parse(