--- a/src/Pure/General/position.ML Wed May 27 16:43:34 2020 +0200
+++ b/src/Pure/General/position.ML Wed May 27 20:02:02 2020 +0200
@@ -38,6 +38,7 @@
val properties_of: T -> Properties.T
val offset_properties_of: T -> Properties.T
val def_properties_of: T -> Properties.T
+ val entity_markup: string -> string * T -> Markup.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
@@ -203,6 +204,9 @@
val def_properties_of = properties_of #> map (fn (x, y) => ("def_" ^ x, y));
+fun entity_markup kind (name, pos) =
+ Markup.entity kind name |> Markup.properties (def_properties_of pos);
+
fun entity_properties_of def serial pos =
if def then (Markup.defN, Value.print_int serial) :: properties_of pos
else (Markup.refN, Value.print_int serial) :: def_properties_of pos;