# HG changeset patch
# User wenzelm
# Date 1394279055 -3600
# Node ID 1c42ebdb3a58deabc0f355d4d479c22e2252584e
# Parent  4c17e46c44c1f5337a56c9a8e33ba5d01b80fbf6
no completion for complete keywords, to avoid confusion of 'assume' ~> 'assumes' etc.;

diff -r 4c17e46c44c1 -r 1c42ebdb3a58 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Sat Mar 08 12:31:23 2014 +0100
+++ b/src/Pure/General/completion.scala	Sat Mar 08 12:44:15 2014 +0100
@@ -358,15 +358,18 @@
           }
         opt_word.map(word =>
           {
+            val complete_words = words_lex.completions(word)
             val completions =
-              for {
-                complete_word <- words_lex.completions(word)
-                ok =
-                  if (is_keyword(complete_word)) language_context.is_outer
-                  else language_context.symbols
-                if ok
-                completion <- words_map.get_list(complete_word)
-              } yield (complete_word, completion)
+              if (complete_words.contains(word)) Nil
+              else
+                for {
+                  complete_word <- complete_words
+                  ok =
+                    if (is_keyword(complete_word)) language_context.is_outer
+                    else language_context.symbols
+                  if ok
+                  completion <- words_map.get_list(complete_word)
+                } yield (complete_word, completion)
             (((word, completions), end))
           })
       }