src/Pure/General/position.ML

--- a/src/Pure/General/position.ML	Tue Aug 24 13:39:37 2021 +0200
+++ b/src/Pure/General/position.ML	Tue Aug 24 14:56:55 2021 +0200
@@ -42,7 +42,7 @@
   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 make_entity_markup: bool -> serial -> string -> string * T -> Markup.T
   val markup: T -> Markup.T -> Markup.T
   val is_reported: T -> bool
   val is_reported_range: T -> bool
@@ -215,9 +215,12 @@
 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;
+fun make_entity_markup def serial kind (name, pos) =
+  let
+    val props =
+      if def then (Markup.defN, Value.print_int serial) :: properties_of pos
+      else (Markup.refN, Value.print_int serial) :: def_properties_of pos;
+  in Markup.entity kind name |> Markup.properties props end;
 
 val markup = Markup.properties o properties_of;