# HG changeset patch
# User wenzelm
# Date 1394216914 -3600
# Node ID b719781c739632195f825e351cf150516a1b9ac1
# Parent  66739f41d5b22be2f08bff4f1353abb20420b60f
more accurate description;

diff -r 66739f41d5b2 -r b719781c7396 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Fri Mar 07 17:07:30 2014 +0100
+++ b/src/Pure/General/completion.scala	Fri Mar 07 19:28:34 2014 +0100
@@ -334,7 +334,8 @@
     }
 
     val words_result =
-      abbrevs_result orElse {
+      if (abbrevs_result.isDefined) None
+      else {
         val end =
           if (extend_word) Completion.Word_Parsers.extend_word(text, caret)
           else caret
@@ -359,7 +360,7 @@
         }
       }
 
-    words_result match {
+    (abbrevs_result orElse words_result) match {
       case Some(((word, cs), end)) =>
         val range = Text.Range(- word.length, 0) + end + start
         val ds = cs.map(decode(_)).filter(_ != word)
@@ -379,7 +380,7 @@
               val move = - s2.length
               val description =
                 if (move != 0) List(name1, "(template)")
-                else if (keywords(name)) List(name1, "(keyword)")
+                else if (words_result.isDefined && keywords(name)) List(name1, "(keyword)")
                 else if (Symbol.names.isDefinedAt(name) && name != name1)
                   List(name1, "(symbol " + quote(name) + ")")
                 else List(name1)