src/Pure/General/completion.scala
changeset 60732 18299765542e
parent 60215 5fb4990dfc73
child 61100 4d9efd5004c8
--- 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)