discontinued entity text color, notably historic red for classes;
tuned entity names;
--- 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;
--- 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*)
--- 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")