src/Pure/General/completion.scala
changeset 57602 0f708666eb7c
parent 57589 e0e4ac981cf1
child 59073 dcecfcc56dce
--- 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)