decode_term: some context-sensitive markup;
more informative Markup.entity and Name_Space.markup_entry;
Markup.const: use "constant" to make it coincide with name space kind;

--- a/src/Pure/General/markup.ML	Sun Mar 27 19:51:51 2011 +0200
+++ b/src/Pure/General/markup.ML	Sun Mar 27 20:55:01 2011 +0200
@@ -16,7 +16,7 @@
   val name: string -> T -> T
   val kindN: string
   val bindingN: string val binding: string -> T
-  val entityN: string val entity: string -> T
+  val entityN: string val entity: string -> string -> T
   val defN: string
   val refN: string
   val lineN: string
@@ -174,7 +174,9 @@
 (* formal entities *)
 
 val (bindingN, binding) = markup_string "binding" nameN;
-val (entityN, entity) = markup_string "entity" nameN;
+
+val entityN = "entity";
+fun entity kind name = (entityN, [(kindN, kind), (nameN, name)]);
 
 val defN = "def";
 val refN = "ref";
@@ -218,7 +220,7 @@
 val (fixed_declN, fixed_decl) = markup_string "fixed_decl" nameN;
 val (fixedN, fixed) = markup_string "fixed" nameN;
 val (const_declN, const_decl) = markup_string "const_decl" nameN;
-val (constN, const) = markup_string "const" nameN;
+val (constN, const) = markup_string "constant" nameN;
 val (fact_declN, fact_decl) = markup_string "fact_decl" nameN;
 val (factN, fact) = markup_string "fact" nameN;
 val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;

--- a/src/Pure/General/name_space.ML	Sun Mar 27 19:51:51 2011 +0200
+++ b/src/Pure/General/name_space.ML	Sun Mar 27 20:55:01 2011 +0200
@@ -24,6 +24,7 @@
   val kind_of: T -> string
   val the_entry: T -> string ->
     {concealed: bool, group: serial option, theory_name: string, pos: Position.T, id: serial}
+  val markup_entry: T -> string -> Markup.T
   val is_concealed: T -> string -> bool
   val intern: T -> xstring -> string
   val extern_flags: {long_names: bool, short_names: bool, unique_names: bool} ->
@@ -79,15 +80,18 @@
   pos: Position.T,
   id: serial};
 
-fun str_of_entry def (name, {pos, id, ...}: entry) =
+fun entry_markup def kind (name, {pos, id, ...}: entry) =
   let
     val occurrence = (if def then Markup.defN else Markup.refN, string_of_int id);
     val props = occurrence :: Position.properties_of pos;
-  in Markup.markup (Markup.properties props (Markup.entity name)) name end;
+  in Markup.properties props (Markup.entity kind name) end;
+
+fun print_entry def kind (name, entry) =
+  quote (Markup.markup (entry_markup def kind (name, entry)) name);
 
 fun err_dup kind entry1 entry2 =
   error ("Duplicate " ^ kind ^ " declaration " ^
-    quote (str_of_entry true entry1) ^ " vs. " ^ quote (str_of_entry true entry2));
+    print_entry true kind entry1 ^ " vs. " ^ print_entry true kind entry2);
 
 
 (* datatype T *)
@@ -117,6 +121,11 @@
     NONE => error ("Unknown " ^ kind ^ " " ^ quote name)
   | SOME (_, entry) => entry);
 
+fun markup_entry (Name_Space {kind, entries, ...}) name =
+  (case Symtab.lookup entries name of
+    NONE => Markup.malformed
+  | SOME (_, entry) => entry_markup false kind (name, entry));
+
 fun is_concealed space name = #concealed (the_entry space name);
 
 

--- a/src/Pure/Isar/proof_context.ML	Sun Mar 27 19:51:51 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Mar 27 20:55:01 2011 +0200
@@ -261,6 +261,7 @@
 fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
 
 val consts_of = #1 o #consts o rep_context;
+val const_space = Consts.space_of o consts_of;
 val the_const_constraint = Consts.the_constraint o consts_of;
 
 val facts_of = #facts o rep_context;
@@ -665,10 +666,13 @@
 in
 
 fun term_context ctxt : Syntax.term_context =
-  {get_sort = get_sort ctxt,
-   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)};
+ {get_sort = get_sort ctxt,
+  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};
 
 val decode_term = Syntax.decode_term o term_context;
 

--- a/src/Pure/Syntax/type_ext.ML	Sun Mar 27 19:51:51 2011 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Sun Mar 27 20:55:01 2011 +0200
@@ -129,20 +129,20 @@
 
 (* decode_term -- transform parse tree into raw term *)
 
-val markup_const = Markup.const;
-fun markup_free x = Markup.name x Markup.free;
-fun markup_var xi = Markup.name (Term.string_of_vname xi) Markup.var;
-
 fun markup_bound def id =
   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};
+  get_free: string -> string option,
+  markup_const: string -> Markup.T,
+  markup_free: string -> Markup.T,
+  markup_var: indexname -> Markup.T};
 
-fun decode_term ({get_sort, get_const, get_free}: term_context) tm =
+fun decode_term (term_context: term_context) tm =
   let
+    val {get_sort, get_const, get_free, markup_const, markup_free, markup_var} = term_context;
     val decodeT = typ_of_term (get_sort (term_sorts tm));
 
     val reports = Unsynchronized.ref ([]: (Position.T * Markup.T) list);