clarified Markup.CLASS vs. HTML.CLASS;

--- a/src/Pure/General/markup.scala	Sat Jun 25 18:29:51 2011 +0200
+++ b/src/Pure/General/markup.scala	Sat Jun 25 19:19:13 2011 +0200
@@ -147,7 +147,7 @@
 
   /* logical entities */
 
-  val TCLASS = "tclass"
+  val CLASS = "class"
   val TYCON = "tycon"
   val FIXED = "fixed"
   val CONST = "constant"
@@ -289,7 +289,6 @@
   val Serial = new Long_Property("serial")
 
   val MESSAGE = "message"
-  val CLASS = "class"
 
   val INIT = "init"
   val STATUS = "status"

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