--- a/src/Pure/ML/ml_compiler_polyml.ML Thu Jul 16 14:40:23 2015 +0200
+++ b/src/Pure/ML/ml_compiler_polyml.ML Thu Jul 16 16:30:43 2015 +0200
@@ -45,9 +45,9 @@
fun reported_completions loc names =
let val pos = Exn_Properties.position_of loc in
- if is_reported pos then
+ if is_reported pos andalso not (null names) then
let
- val completion = Completion.names pos (map (fn a => (a, ("ML", ""))) names);
+ val completion = Completion.names pos (map (fn a => (a, ("ML", a))) names);
val xml = Completion.encode completion;
in cons (pos, fn () => Markup.completion, fn () => YXML.string_of_body xml) end
else I