no completion for complete keywords, to avoid confusion of 'assume' ~> 'assumes' etc.;
authorwenzelm
Sat Mar 08 12:44:15 2014 +0100 (2014-03-08)
changeset 559941c42ebdb3a58
parent 55993 4c17e46c44c1
child 55995 ff7ee9c92d54
no completion for complete keywords, to avoid confusion of 'assume' ~> 'assumes' etc.;
src/Pure/General/completion.scala
     1.1 --- a/src/Pure/General/completion.scala	Sat Mar 08 12:31:23 2014 +0100
     1.2 +++ b/src/Pure/General/completion.scala	Sat Mar 08 12:44:15 2014 +0100
     1.3 @@ -358,15 +358,18 @@
     1.4            }
     1.5          opt_word.map(word =>
     1.6            {
     1.7 +            val complete_words = words_lex.completions(word)
     1.8              val completions =
     1.9 -              for {
    1.10 -                complete_word <- words_lex.completions(word)
    1.11 -                ok =
    1.12 -                  if (is_keyword(complete_word)) language_context.is_outer
    1.13 -                  else language_context.symbols
    1.14 -                if ok
    1.15 -                completion <- words_map.get_list(complete_word)
    1.16 -              } yield (complete_word, completion)
    1.17 +              if (complete_words.contains(word)) Nil
    1.18 +              else
    1.19 +                for {
    1.20 +                  complete_word <- complete_words
    1.21 +                  ok =
    1.22 +                    if (is_keyword(complete_word)) language_context.is_outer
    1.23 +                    else language_context.symbols
    1.24 +                  if ok
    1.25 +                  completion <- words_map.get_list(complete_word)
    1.26 +                } yield (complete_word, completion)
    1.27              (((word, completions), end))
    1.28            })
    1.29        }