--- a/src/Pure/General/completion.ML Sun Nov 25 21:11:38 2018 +0100
+++ b/src/Pure/General/completion.ML Tue Nov 27 16:20:08 2018 +0100
@@ -12,7 +12,7 @@
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
@@ -57,12 +57,12 @@
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);