no completion for complete keywords, to avoid confusion of 'assume' ~> 'assumes' etc.;
authorwenzelm
Sat, 08 Mar 2014 12:44:15 +0100
changeset 55994 1c42ebdb3a58
parent 55993 4c17e46c44c1
child 55995 ff7ee9c92d54
no completion for complete keywords, to avoid confusion of 'assume' ~> 'assumes' etc.;
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))
           })
       }