# HG changeset patch
# User wenzelm
# Date 1377806882 -7200
# Node ID 45be26b98ca6e9feb135a1bf4e4c48d76ea065af
# Parent  814eee60e1b15d9bf859535e0120c8980f229885
preserve original word -- relevant for true uniqueness of immediate completion;

diff -r 814eee60e1b1 -r 45be26b98ca6 src/Pure/Isar/completion.scala
--- a/src/Pure/Isar/completion.scala	Thu Aug 29 21:53:29 2013 +0200
+++ b/src/Pure/Isar/completion.scala	Thu Aug 29 22:08:02 2013 +0200
@@ -105,7 +105,7 @@
       }
     raw_result match {
       case Some((word, cs)) =>
-        val ds = (if (decode) cs.map(Symbol.decode(_)).sorted else cs).filter(_ != word)
+        val ds = (if (decode) cs.map(Symbol.decode(_)).sorted else cs)
         if (ds.isEmpty) None
         else Some((word, ds.map(s => Completion.Item(word, s, s))))
       case None => None