src/Pure/Isar/proof_context.ML

     val class_space = Type.class_space tsig;
 
     val name = Type.cert_class tsig (Name_Space.intern class_space xname)
       handle TYPE (msg, _, _) =>
         error (msg ^ Position.here pos ^
-          Markup.markup_report (Completion.reported_text
-            (Name_Space.completion (Context.Proof ctxt) class_space (K true) (xname, pos))));
+          Completion.markup_report
+            [Name_Space.completion (Context.Proof ctxt) class_space (K true) (xname, pos)]);
     val reports =
       if Context_Position.is_reported ctxt pos
       then [(pos, Name_Space.markup class_space name)] else [];
   in (name, reports) end;
 

 
 (* constant names *)
 
 fun consts_completion_message ctxt (c, ps) =
   ps |> map (fn pos =>
-    Name_Space.completion (Context.Proof ctxt) (Consts.space_of (consts_of ctxt)) (K true) (c, pos)
-    |> Completion.reported_text)
-  |> implode
-  |> Markup.markup_report;
+    Name_Space.completion (Context.Proof ctxt) (Consts.space_of (consts_of ctxt)) (K true) (c, pos))
+  |> Completion.markup_report;
 
 fun check_const {proper, strict} ctxt (c, ps) =
   let
     val _ =
       Name.reject_internal (c, ps) handle ERROR msg =>