preserve original word -- relevant for true uniqueness of immediate completion;

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