discontinued specific entity markup, which causes confusion with "kind" names with spaces (e.g. "type name");
authorwenzelm
Sat Mar 10 23:28:42 2012 +0100 (2012-03-10 ago)
changeset 46865659dcbafe4bf
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
     1.1 --- a/etc/isabelle.css	Sat Mar 10 23:00:32 2012 +0100
     1.2 +++ b/etc/isabelle.css	Sat Mar 10 23:28:42 2012 +0100
     1.3 @@ -20,9 +20,6 @@
     1.4  .hidden         { font-size: 1px; visibility: hidden; }
     1.5  
     1.6  .binding        { color: #336655; }
     1.7 -.entity_class   { color: red; }
     1.8 -.entity_type    { }
     1.9 -.entity_constant { }
    1.10  .tfree          { color: #A020F0; }
    1.11  .tvar           { color: #A020F0; }
    1.12  .free           { color: blue; }
     2.1 --- a/src/Pure/Thy/html.scala	Sat Mar 10 23:00:32 2012 +0100
     2.2 +++ b/src/Pure/Thy/html.scala	Sat Mar 10 23:28:42 2012 +0100
     2.3 @@ -60,9 +60,7 @@
     2.4      def html_spans(tree: XML.Tree): XML.Body =
     2.5        tree match {
     2.6          case XML.Elem(m @ Markup(name, props), ts) =>
     2.7 -          val span_class =
     2.8 -            m match { case Isabelle_Markup.Entity(kind, _) => name + "_" + kind case _ => name }
     2.9 -          val html_span = span(span_class, ts.flatMap(html_spans))
    2.10 +          val html_span = span(name, ts.flatMap(html_spans))
    2.11            if (original_data) List(XML.Elem(Markup.Data, List(tree, html_span)))
    2.12            else List(html_span)
    2.13          case XML.Text(txt) =>