# HG changeset patch
# User wenzelm
# Date 1406022394 -7200
# Node ID 0f708666eb7c7a495a34a655b92b3c674ec8fa2c
# Parent  22e810680123507269af8b35714a14514250c733
no keyword completion within word context -- especially avoid its odd visual rendering;

diff -r 22e810680123 -r 0f708666eb7c src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Tue Jul 22 08:07:47 2014 +0200
+++ b/src/Pure/General/completion.scala	Tue Jul 22 11:46:34 2014 +0200
@@ -365,6 +365,8 @@
     val words_result =
       if (abbrevs_result.isDefined) None
       else {
+        val word_context =
+          caret < length && Completion.Word_Parsers.is_word_char(text.charAt(caret))
         val result =
           Completion.Word_Parsers.read_symbol(text.subSequence(0, caret)) match {
             case Some(symbol) => Some((symbol, ""))
@@ -381,7 +383,7 @@
                   for {
                     complete_word <- complete_words
                     ok =
-                      if (is_keyword(complete_word)) language_context.is_outer
+                      if (is_keyword(complete_word)) !word_context && language_context.is_outer
                       else language_context.symbols
                     if ok
                     completion <- words_map.get_list(complete_word)