src/Pure/General/completion.ML

   type T
   val names: Position.T -> name list -> T
   val none: T
   val make: string * Position.T -> ((string -> bool) -> name list) -> T
   val encode: T -> XML.body
-  val markup_element: T -> Markup.T * XML.body
+  val markup_element: T -> (Markup.T * XML.body) option
   val markup_report: T list -> string
   val make_report: string * Position.T -> ((string -> bool) -> name list) -> string
   val suppress_abbrevs: string -> Markup.T list
   val check_option: Options.T -> Proof.context -> string * Position.T -> string
   val check_option_value:

   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
-      (Position.markup pos Markup.completion, encode completion)
-    else (Markup.empty, [])
+      SOME (Position.markup pos Markup.completion, encode completion)
+    else NONE
   end;
 
 val markup_report =
-  map (markup_element #> XML.Elem) #> YXML.string_of_body #> Markup.markup_report;
+  map_filter markup_element #> map XML.Elem #> YXML.string_of_body #> Markup.markup_report;
 
 val make_report = markup_report oo (single oo make);
 
 
 (* suppress short abbreviations *)