more informative markup for fixed variables (via name space entry);
uniform markup for undeclared entities;
tuned;

--- a/src/Pure/General/name_space.ML	Wed Apr 27 20:28:27 2011 +0200
+++ b/src/Pure/General/name_space.ML	Wed Apr 27 20:37:56 2011 +0200
@@ -130,7 +130,7 @@
 
 fun markup (Name_Space {kind, entries, ...}) name =
   (case Symtab.lookup entries name of
-    NONE => Markup.malformed
+    NONE => Markup.hilite
   | SOME (_, entry) => entry_markup false kind (name, entry));
 
 fun is_concealed space name = #concealed (the_entry space name);

--- a/src/Pure/Syntax/syntax_phases.ML	Wed Apr 27 20:28:27 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Wed Apr 27 20:37:56 2011 +0200
@@ -31,8 +31,9 @@
 
 fun markup_free ctxt x =
   [if can Name.dest_skolem x then Markup.skolem else Markup.free] @
-  (if not (Variable.is_body ctxt) orelse Variable.is_fixed ctxt x then []
-   else [Markup.hilite]);
+  (if Variable.is_body ctxt orelse Variable.is_fixed ctxt x
+   then [Variable.markup_fixed ctxt x]
+   else []);
 
 fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var];
 

--- a/src/Pure/variable.ML	Wed Apr 27 20:28:27 2011 +0200
+++ b/src/Pure/variable.ML	Wed Apr 27 20:37:56 2011 +0200
@@ -32,10 +32,11 @@
   val lookup_const: Proof.context -> string -> string option
   val is_const: Proof.context -> string -> bool
   val declare_const: string * string -> Proof.context -> Proof.context
-  val fixed_ord: Proof.context -> string * string -> order
   val is_fixed: Proof.context -> string -> bool
   val newly_fixed: Proof.context -> Proof.context -> string -> bool
+  val fixed_ord: Proof.context -> string * string -> order
   val intern_fixed: Proof.context -> string -> string
+  val markup_fixed: Proof.context -> string -> Markup.T
   val lookup_fixed: Proof.context -> string -> string option
   val revert_fixed: Proof.context -> string -> string
   val add_fixed_names: Proof.context -> term -> string list -> string list
@@ -154,6 +155,7 @@
 
 val names_of = #names o rep_data;
 val fixes_of = #fixes o rep_data;
+val fixes_space = #1 o fixes_of;
 val binds_of = #binds o rep_data;
 val type_occs_of = #type_occs o rep_data;
 val maxidx_of = #maxidx o rep_data;
@@ -289,12 +291,12 @@
 
 (* specialized name space *)
 
-fun fixed_ord ctxt = Name_Space.entry_ord (#1 (fixes_of ctxt));
-
-fun is_fixed ctxt x = can (Name_Space.the_entry (#1 (fixes_of ctxt))) x;
+fun is_fixed ctxt x = can (Name_Space.the_entry (fixes_space ctxt)) x;
 fun newly_fixed inner outer x = is_fixed inner x andalso not (is_fixed outer x);
 
-fun intern_fixed ctxt = Name_Space.intern (#1 (fixes_of ctxt));
+val fixed_ord = Name_Space.entry_ord o fixes_space;
+val intern_fixed = Name_Space.intern o fixes_space;
+val markup_fixed = Name_Space.markup o fixes_space;
 
 fun lookup_fixed ctxt x =
   let val x' = intern_fixed ctxt x