# HG changeset patch
# User wenzelm
# Date 1321016840 -3600
# Node ID 388fb71623dda4bf3d1c30e86d881955853f760b
# Parent  304437f4386946be8e2e11b9589da026bbf06598
discontinued entity text color, notably historic red for classes;
tuned entity names;

diff -r 304437f43869 -r 388fb71623dd src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Fri Nov 11 12:52:57 2011 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Nov 11 14:07:20 2011 +0100
@@ -59,7 +59,7 @@
 fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var];
 
 fun markup_bound def ps (name, id) =
-  let val entity = Markup.entity "bound variable" name in
+  let val entity = Markup.entity Markup.boundN name in
     Markup.bound ::
       map (fn pos => Markup.properties (Position.entity_properties_of def id pos) entity) ps
   end;
diff -r 304437f43869 -r 388fb71623dd src/Pure/variable.ML
--- a/src/Pure/variable.ML	Fri Nov 11 12:52:57 2011 +0100
+++ b/src/Pure/variable.ML	Fri Nov 11 14:07:20 2011 +0100
@@ -81,7 +81,7 @@
 (** local context data **)
 
 type fixes = string Name_Space.table;
-val empty_fixes: fixes = Name_Space.empty_table "fixed variable";
+val empty_fixes: fixes = Name_Space.empty_table Markup.fixedN;
 
 datatype data = Data of
  {is_body: bool,                        (*inner body mode*)
diff -r 304437f43869 -r 388fb71623dd src/Tools/jEdit/src/isabelle_markup.scala
--- a/src/Tools/jEdit/src/isabelle_markup.scala	Fri Nov 11 12:52:57 2011 +0100
+++ b/src/Tools/jEdit/src/isabelle_markup.scala	Fri Nov 11 14:07:20 2011 +0100
@@ -127,9 +127,6 @@
     case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color
   }
 
-  private val text_entity_colors: Map[String, Color] =
-    Map(Markup.CLASS -> get_color("red"))
-
   private val text_colors: Map[String, Color] =
     Map(
       Markup.STRING -> get_color("black"),
@@ -157,10 +154,7 @@
 
   val text_color: Markup_Tree.Select[Color] =
   {
-    case Text.Info(_, XML.Elem(Markup.Entity(kind, _), _))
-    if text_entity_colors.isDefinedAt(kind) => text_entity_colors(kind)
-    case Text.Info(_, XML.Elem(Markup(m, _), _))
-    if text_colors.isDefinedAt(m) => text_colors(m)
+    case Text.Info(_, XML.Elem(Markup(m, _), _)) if text_colors.isDefinedAt(m) => text_colors(m)
   }
 
   private val tooltips: Map[String, String] =
@@ -170,12 +164,12 @@
       Markup.TERM -> "term",
       Markup.PROP -> "proposition",
       Markup.TOKEN_RANGE -> "inner syntax token",
-      Markup.FREE -> "free variable (globally fixed)",
-      Markup.SKOLEM -> "skolem variable (locally fixed)",
-      Markup.BOUND -> "bound variable (internally fixed)",
-      Markup.VAR -> "schematic variable",
-      Markup.TFREE -> "free type variable",
-      Markup.TVAR -> "schematic type variable",
+      Markup.FREE -> "free",
+      Markup.SKOLEM -> "locally fixed",
+      Markup.BOUND -> "bound",
+      Markup.VAR -> "schematic",
+      Markup.TFREE -> "free type",
+      Markup.TVAR -> "schematic type",
       Markup.ML_SOURCE -> "ML source",
       Markup.DOC_SOURCE -> "document source")