do allow replacement of words where this is appropriate, notably symbol abbrevs and keyword templates (see also 1c42ebdb3a58);
authorwenzelm
Sun Mar 09 15:21:08 2014 +0100 (2014-03-09)
changeset 560012df1e7bca361
parent 56000 899ad5a3ad00
child 56002 2028467b4df4
do allow replacement of words where this is appropriate, notably symbol abbrevs and keyword templates (see also 1c42ebdb3a58);
src/Pure/General/completion.scala
     1.1 --- a/src/Pure/General/completion.scala	Sat Mar 08 23:03:15 2014 +0100
     1.2 +++ b/src/Pure/General/completion.scala	Sun Mar 09 15:21:08 2014 +0100
     1.3 @@ -272,7 +272,8 @@
     1.4  
     1.5    private def is_symbol(name: String): Boolean = Symbol.names.isDefinedAt(name)
     1.6    private def is_keyword(name: String): Boolean = !is_symbol(name) && keywords.isDefinedAt(name)
     1.7 -  private def is_keyword_template(name: String): Boolean = is_keyword(name) && keywords(name)
     1.8 +  private def is_keyword_template(name: String, template: Boolean): Boolean =
     1.9 +    is_keyword(name) && keywords(name) == template
    1.10  
    1.11    def + (keyword: String, template: String): Completion =
    1.12      new Completion(
    1.13 @@ -366,7 +367,7 @@
    1.14                val complete_words = words_lex.completions(word)
    1.15                val full_word = word + underscores
    1.16                val completions =
    1.17 -                if (complete_words.contains(full_word)) Nil
    1.18 +                if (complete_words.contains(full_word) && is_keyword_template(full_word, false)) Nil
    1.19                  else
    1.20                    for {
    1.21                      complete_word <- complete_words
    1.22 @@ -405,7 +406,7 @@
    1.23                  if (name0 == name1) List(name0)
    1.24                  else List(name1, "(symbol " + quote(name0) + ")")
    1.25                }
    1.26 -              else if (is_keyword_template(complete_word))
    1.27 +              else if (is_keyword_template(complete_word, true))
    1.28                  List(name1, "(template " + quote(complete_word) + ")")
    1.29                else if (move != 0) List(name1, "(template)")
    1.30                else if (is_keyword(complete_word)) List(name1, "(keyword)")