--- 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;