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;