equal
deleted
inserted
replaced
59 in pair int (list (pair string (pair string string))) (total, names) end; |
59 in pair int (list (pair string (pair string string))) (total, names) end; |
60 |
60 |
61 fun markup_element completion = |
61 fun markup_element completion = |
62 let val {pos, names, ...} = dest completion in |
62 let val {pos, names, ...} = dest completion in |
63 if Position.is_reported pos andalso not (null names) then |
63 if Position.is_reported pos andalso not (null names) then |
64 SOME (Position.markup pos Markup.completion, encode completion) |
64 SOME (Position.markup_properties pos Markup.completion, encode completion) |
65 else NONE |
65 else NONE |
66 end; |
66 end; |
67 |
67 |
68 val markup_report = |
68 val markup_report = |
69 map_filter markup_element #> map XML.Elem #> YXML.string_of_body #> Markup.markup_report; |
69 map_filter markup_element #> map XML.Elem #> YXML.string_of_body #> Markup.markup_report; |