# HG changeset patch
# User wenzelm
# Date 1437057043 -7200
# Node ID 18299765542e9ef739cbee8f4e33303c775ba2fe
# Parent  4ac4b314d93c79ae6613b8ac32d3a6ea810f4390
clarified boundary cases of completion;

diff -r 4ac4b314d93c -r 18299765542e src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Thu Jul 16 14:40:23 2015 +0200
+++ b/src/Pure/General/completion.scala	Thu Jul 16 16:30:43 2015 +0200
@@ -199,7 +199,8 @@
             if (kind == "") (name, quote(decode(name)))
             else
              (Long_Name.qualify(kind, name),
-              Word.implode(Word.explode('_', kind)) + " " + quote(decode(name)))
+              Word.implode(Word.explode('_', kind)) +
+              (if (xname == name) "" else " " + quote(decode(name))))
           description = List(xname1, "(" + descr_name + ")")
         } yield Item(range, original, full_name, description, xname1, 0, true)
 
diff -r 4ac4b314d93c -r 18299765542e src/Pure/ML/ml_compiler_polyml.ML
--- 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