--- 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)