# HG changeset patch
# User wenzelm
# Date 1331418522 -3600
# Node ID 659dcbafe4bf635b831985cf2e78cc3b9653923a
# Parent  6eb62a79d02acc67b3746282ff71cf33797502d9
discontinued specific entity markup, which causes confusion with "kind" names with spaces (e.g. "type name");
uniform treatment of "class" entities in input and output;

diff -r 6eb62a79d02a -r 659dcbafe4bf etc/isabelle.css
--- a/etc/isabelle.css	Sat Mar 10 23:00:32 2012 +0100
+++ b/etc/isabelle.css	Sat Mar 10 23:28:42 2012 +0100
@@ -20,9 +20,6 @@
 .hidden         { font-size: 1px; visibility: hidden; }
 
 .binding        { color: #336655; }
-.entity_class   { color: red; }
-.entity_type    { }
-.entity_constant { }
 .tfree          { color: #A020F0; }
 .tvar           { color: #A020F0; }
 .free           { color: blue; }
diff -r 6eb62a79d02a -r 659dcbafe4bf src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Sat Mar 10 23:00:32 2012 +0100
+++ b/src/Pure/Thy/html.scala	Sat Mar 10 23:28:42 2012 +0100
@@ -60,9 +60,7 @@
     def html_spans(tree: XML.Tree): XML.Body =
       tree match {
         case XML.Elem(m @ Markup(name, props), ts) =>
-          val span_class =
-            m match { case Isabelle_Markup.Entity(kind, _) => name + "_" + kind case _ => name }
-          val html_span = span(span_class, ts.flatMap(html_spans))
+          val html_span = span(name, ts.flatMap(html_spans))
           if (original_data) List(XML.Elem(Markup.Data, List(tree, html_span)))
           else List(html_span)
         case XML.Text(txt) =>