# HG changeset patch
# User wenzelm
# Date 1309022353 -7200
# Node ID 07a9cbf2376f646c8db7f4c98c02e63325d3b471
# Parent  b416425c7ad048819d866494077c51bf5b36984a
clarified Markup.CLASS vs. HTML.CLASS;

diff -r b416425c7ad0 -r 07a9cbf2376f src/Pure/General/markup.scala
--- 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"
diff -r b416425c7ad0 -r 07a9cbf2376f src/Tools/jEdit/src/html_panel.scala
--- 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(