diff -r c12a3edcd8e4 -r ffabc0083786 src/Pure/Isar/completion.scala
--- a/src/Pure/Isar/completion.scala	Fri Aug 30 12:59:28 2013 +0200
+++ b/src/Pure/Isar/completion.scala	Fri Aug 30 13:24:14 2013 +0200
@@ -11,7 +11,7 @@
 
 object Completion
 {
-  /* items */
+  /* result */
 
   sealed case class Item(
     original: String,
@@ -20,6 +20,8 @@
     immediate: Boolean)
   { override def toString: String = description }
 
+  sealed case class Result(original: String, unique: Boolean, items: List[Item])
+
 
   /* init */
 
@@ -92,8 +94,7 @@
 
   /* complete */
 
-  def complete(decode: Boolean, explicit: Boolean, line: CharSequence)
-    : Option[(String, List[Completion.Item])] =
+  def complete(decode: Boolean, explicit: Boolean, line: CharSequence): Option[Completion.Result] =
   {
     val raw_result =
       abbrevs_lex.parse(abbrevs_lex.keyword, new Library.Reverse(line)) match {
@@ -115,13 +116,14 @@
       }
     raw_result match {
       case Some((word, cs)) =>
-        val ds = (if (decode) cs.map(Symbol.decode(_)).sorted else cs)
+        val ds = (if (decode) cs.map(Symbol.decode(_)).sorted else cs).filter(_ != word)
         if (ds.isEmpty) None
         else {
           val immediate =
             !Completion.is_word(word) &&
             Character.codePointCount(word, 0, word.length) > 1
-          Some((word, ds.map(s => Completion.Item(word, s, s, explicit || immediate))))
+          val items = ds.map(s => Completion.Item(word, s, s, explicit || immediate))
+          Some(Completion.Result(word, cs.length == 1, items))
         }
       case None => None
     }