src/Pure/General/completion.ML

   in pair int (list (pair string (pair string string))) (total, names) end;
 
 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;
 
 val markup_report =
   map_filter markup_element #> map XML.Elem #> YXML.string_of_body #> Markup.markup_report;