discontinued specific entity markup, which causes confusion with "kind" names with spaces (e.g. "type name");
authorwenzelm
Sat, 10 Mar 2012 23:28:42 +0100
changeset 46865 659dcbafe4bf
parent 46864 6eb62a79d02a
child 46866 b190913c3c41
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;
etc/isabelle.css
src/Pure/Thy/html.scala
--- 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) =>