diff -r cdcf2fcf3f54 -r f8b0271cc744 src/Pure/General/position.ML
--- 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;