# HG changeset patch
# User wenzelm
# Date 1260972905 -3600
# Node ID 3d654643cf56d8bba35b296ff4292f681987bb36
# Parent  3aea0882879ffe2baccfa1981b373f941d290d0b
filter out identical completions;

diff -r 3aea0882879f -r 3d654643cf56 src/Pure/Thy/completion.scala
--- a/src/Pure/Thy/completion.scala	Wed Dec 16 14:15:24 2009 +0100
+++ b/src/Pure/Thy/completion.scala	Wed Dec 16 15:15:05 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
         }