more informative markup_free;

--- a/src/Pure/Isar/proof_context.ML	Wed Mar 30 21:07:48 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Mar 30 22:03:50 2011 +0200
@@ -670,9 +670,11 @@
   get_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a)))
     handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)),
   get_free = intern_skolem ctxt (Variable.def_type ctxt false),
-  markup_const = Name_Space.markup_entry (const_space ctxt),
-  markup_free = fn x => Markup.name x Markup.free,
-  markup_var = fn xi => Markup.name (Term.string_of_vname xi) Markup.var};
+  markup_const = fn x => [Name_Space.markup_entry (const_space ctxt) x],
+  markup_free = fn x =>
+    [if can Name.dest_skolem x then Markup.skolem else Markup.free] @
+    (if Variable.is_fixed ctxt x then [] else [Markup.hilite]),
+  markup_var = fn xi => [Markup.name (Term.string_of_vname xi) Markup.var]};
 
 val decode_term = Syntax.decode_term o term_context;
 

--- a/src/Pure/Syntax/type_ext.ML	Wed Mar 30 21:07:48 2011 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Wed Mar 30 22:03:50 2011 +0200
@@ -130,15 +130,15 @@
 (* decode_term -- transform parse tree into raw term *)
 
 fun markup_bound def id =
-  Markup.properties [(if def then Markup.defN else Markup.refN, id)] Markup.bound;
+  [Markup.properties [(if def then Markup.defN else Markup.refN, id)] Markup.bound];
 
 type term_context =
  {get_sort: (indexname * sort) list -> indexname -> sort,
   get_const: string -> bool * string,
   get_free: string -> string option,
-  markup_const: string -> Markup.T,
-  markup_free: string -> Markup.T,
-  markup_var: indexname -> Markup.T};
+  markup_const: string -> Markup.T list,
+  markup_free: string -> Markup.T list,
+  markup_var: indexname -> Markup.T list};
 
 fun decode_term (term_context: term_context) tm =
   let
@@ -148,8 +148,8 @@
     val reports = Unsynchronized.ref ([]: (Position.T * Markup.T) list);
     fun report [] _ _ = ()
       | report ps markup x =
-          let val m = markup x
-          in Unsynchronized.change reports (fold (fn p => cons (p, m)) ps) end;
+          let val ms = markup x
+          in Unsynchronized.change reports (fold (fn p => fold (fn m => cons (p, m)) ms) ps) end;
 
     fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
           (case decode_position typ of