# HG changeset patch
# User wenzelm
# Date 1394374868 -3600
# Node ID 2df1e7bca361af0e1e9af12319e1661dc914bc16
# Parent  899ad5a3ad0095815b833bd374652715b87db188
do allow replacement of words where this is appropriate, notably symbol abbrevs and keyword templates (see also 1c42ebdb3a58);

diff -r 899ad5a3ad00 -r 2df1e7bca361 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Sat Mar 08 23:03:15 2014 +0100
+++ b/src/Pure/General/completion.scala	Sun Mar 09 15:21:08 2014 +0100
@@ -272,7 +272,8 @@
 
   private def is_symbol(name: String): Boolean = Symbol.names.isDefinedAt(name)
   private def is_keyword(name: String): Boolean = !is_symbol(name) && keywords.isDefinedAt(name)
-  private def is_keyword_template(name: String): Boolean = is_keyword(name) && keywords(name)
+  private def is_keyword_template(name: String, template: Boolean): Boolean =
+    is_keyword(name) && keywords(name) == template
 
   def + (keyword: String, template: String): Completion =
     new Completion(
@@ -366,7 +367,7 @@
               val complete_words = words_lex.completions(word)
               val full_word = word + underscores
               val completions =
-                if (complete_words.contains(full_word)) Nil
+                if (complete_words.contains(full_word) && is_keyword_template(full_word, false)) Nil
                 else
                   for {
                     complete_word <- complete_words
@@ -405,7 +406,7 @@
                 if (name0 == name1) List(name0)
                 else List(name1, "(symbol " + quote(name0) + ")")
               }
-              else if (is_keyword_template(complete_word))
+              else if (is_keyword_template(complete_word, true))
                 List(name1, "(template " + quote(complete_word) + ")")
               else if (move != 0) List(name1, "(template)")
               else if (is_keyword(complete_word)) List(name1, "(keyword)")