no keyword completion within word context -- especially avoid its odd visual rendering;
authorwenzelm
Tue Jul 22 11:46:34 2014 +0200 (2014-07-22)
changeset 576020f708666eb7c
parent 57601 22e810680123
child 57603 0f58af858813
no keyword completion within word context -- especially avoid its odd visual rendering;
src/Pure/General/completion.scala
     1.1 --- a/src/Pure/General/completion.scala	Tue Jul 22 08:07:47 2014 +0200
     1.2 +++ b/src/Pure/General/completion.scala	Tue Jul 22 11:46:34 2014 +0200
     1.3 @@ -365,6 +365,8 @@
     1.4      val words_result =
     1.5        if (abbrevs_result.isDefined) None
     1.6        else {
     1.7 +        val word_context =
     1.8 +          caret < length && Completion.Word_Parsers.is_word_char(text.charAt(caret))
     1.9          val result =
    1.10            Completion.Word_Parsers.read_symbol(text.subSequence(0, caret)) match {
    1.11              case Some(symbol) => Some((symbol, ""))
    1.12 @@ -381,7 +383,7 @@
    1.13                    for {
    1.14                      complete_word <- complete_words
    1.15                      ok =
    1.16 -                      if (is_keyword(complete_word)) language_context.is_outer
    1.17 +                      if (is_keyword(complete_word)) !word_context && language_context.is_outer
    1.18                        else language_context.symbols
    1.19                      if ok
    1.20                      completion <- words_map.get_list(complete_word)