src/Pure/ML/ml_compiler_polyml.ML
changeset 60732 18299765542e
parent 60731 4ac4b314d93c
child 60744 4eba53a0ac3d
--- 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