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;
--- 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; }
--- 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) =>