--- a/src/Pure/Isar/proof_context.ML Mon Nov 12 14:02:33 2018 +0100
+++ b/src/Pure/Isar/proof_context.ML Mon Nov 12 15:14:12 2018 +0100
@@ -450,8 +450,8 @@
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 [];
@@ -535,10 +535,8 @@
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