src/Pure/General/completion.ML

--- a/src/Pure/General/completion.ML	Thu Sep 12 19:46:08 2024 +0200
+++ b/src/Pure/General/completion.ML	Thu Sep 12 19:52:01 2024 +0200
@@ -61,7 +61,7 @@
 fun markup_element completion =
   let val {pos, names, ...} = dest completion in
     if Position.is_reported pos andalso not (null names) then
-      SOME (Position.markup pos Markup.completion, encode completion)
+      SOME (Position.markup_properties pos Markup.completion, encode completion)
     else NONE
   end;