# HG changeset patch
# User wenzelm
# Date 1320782975 -3600
# Node ID 7797f5351ec4723896e8fc9da3080d98865306e7
# Parent  af607f4945f4109af7e01e278cd2954f286ef2ed
entity markup for bound variables;

diff -r af607f4945f4 -r 7797f5351ec4 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Tue Nov 08 17:47:22 2011 +0100
+++ b/src/Pure/General/name_space.ML	Tue Nov 08 21:09:35 2011 +0100
@@ -83,11 +83,7 @@
   id: serial};
 
 fun entry_markup def kind (name, {pos, id, ...}: entry) =
-  let
-    val props =
-      if def then (Markup.defN, string_of_int id) :: Position.properties_of pos
-      else (Markup.refN, string_of_int id) :: Position.def_properties_of pos;
-  in Markup.properties props (Markup.entity kind name) end;
+  Markup.properties (Position.entity_properties_of def id pos) (Markup.entity kind name);
 
 fun print_entry def kind (name, entry) =
   quote (Markup.markup (entry_markup def kind (name, entry)) name);
diff -r af607f4945f4 -r 7797f5351ec4 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Tue Nov 08 17:47:22 2011 +0100
+++ b/src/Pure/General/position.ML	Tue Nov 08 21:09:35 2011 +0100
@@ -29,6 +29,7 @@
   val of_properties: Properties.T -> T
   val properties_of: T -> Properties.T
   val def_properties_of: T -> Properties.T
+  val entity_properties_of: bool -> serial -> T -> Properties.T
   val default_properties: T -> Properties.T -> Properties.T
   val markup: T -> Markup.T -> Markup.T
   val is_reported: T -> bool
@@ -140,6 +141,10 @@
 
 val def_properties_of = properties_of #> (map (fn (x, y) => ("def_" ^ x, y)));
 
+fun entity_properties_of def id pos =
+  if def then (Markup.defN, string_of_int id) :: properties_of pos
+  else (Markup.refN, string_of_int id) :: def_properties_of pos;
+
 fun default_properties default props =
   if exists (member (op =) Markup.position_properties o #1) props then props
   else properties_of default @ props;
diff -r af607f4945f4 -r 7797f5351ec4 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Tue Nov 08 17:47:22 2011 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Tue Nov 08 21:09:35 2011 +0100
@@ -37,8 +37,11 @@
 
 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];
+fun markup_bound def ps (name, id) =
+  let val entity = Markup.entity "bound variable" name in
+    Markup.bound ::
+      map (fn pos => Markup.properties (Position.entity_properties_of def id pos) entity) ps
+  end;
 
 fun markup_entity ctxt c =
   (case Syntax.lookup_const (Proof_Context.syn_of ctxt) c of
@@ -219,9 +222,9 @@
               | NONE => Type.constraint (decodeT typ --> dummyT) (decode ps qs bs t))
           | decode _ qs bs (Abs (x, T, t)) =
               let
-                val id = serial_string ();
-                val _ = report qs (markup_bound true) id;
-              in Abs (x, T, decode [] [] (id :: bs) t) end
+                val id = serial ();
+                val _ = report qs (markup_bound true qs) (x, id);
+              in Abs (x, T, decode [] [] ((qs, (x, id)) :: bs) t) end
           | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u
           | decode ps _ _ (Const (a, T)) =
               (case try Lexicon.unmark_fixed a of
@@ -245,7 +248,7 @@
           | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T))
           | decode ps _ bs (t as Bound i) =
               (case try (nth bs) i of
-                SOME id => (report ps (markup_bound false) id; t)
+                SOME (qs, (x, id)) => (report ps (markup_bound false qs) (x, id); t)
               | NONE => t);
 
         val tm' = Exn.interruptible_capture (fn () => decode [] [] [] tm) ();