# HG changeset patch
# User wenzelm
# Date 1260972939 -3600
# Node ID 61e19e96828f1fcc6f417719f44bdd566b3cfac4
# Parent  3a77e8862e59d3238bb2521053f688b5700ff3f4# Parent  3d654643cf56d8bba35b296ff4292f681987bb36
merged

diff -r 3a77e8862e59 -r 61e19e96828f src/Pure/Thy/completion.scala
--- a/src/Pure/Thy/completion.scala	Wed Dec 16 14:24:18 2009 +0100
+++ b/src/Pure/Thy/completion.scala	Wed Dec 16 15:15:39 2009 +0100
@@ -116,13 +116,14 @@
     abbrevs_lex.parse(abbrevs_lex.keyword, new Completion.Reverse(line)) match {
       case abbrevs_lex.Success(rev_a, _) =>
         val (word, c) = abbrevs_map(rev_a)
-        Some(word, List(c))
+        if (word == c) None
+        else Some(word, List(c))
       case _ =>
         Completion.Parse.read(line) match {
           case Some(word) =>
-            words_lex.completions(word) match {
+            words_lex.completions(word).map(words_map(_)).filter(_ != word) match {
               case Nil => None
-              case cs => Some(word, cs.map(words_map(_)).sort(Completion.length_ord _))
+              case cs => Some (word, cs.sort(Completion.length_ord _))
             }
           case None => None
         }