# HG changeset patch
# User wenzelm
# Date 1394220768 -3600
# Node ID 61b0021ed674e42df6817f7eac9dbc736e29bd12
# Parent  594afef0dd89e32ae74a3268018a0b82c5463712
more strict discrimination: symbols vs. keywords could overlap;

diff -r 594afef0dd89 -r 61b0021ed674 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Fri Mar 07 20:24:14 2014 +0100
+++ b/src/Pure/General/completion.scala	Fri Mar 07 20:32:48 2014 +0100
@@ -265,8 +265,9 @@
 {
   /* keywords */
 
-  private def is_keyword(name: String): Boolean = keywords.isDefinedAt(name)
-  private def is_keyword_template(name: String): Boolean = keywords.get(name) == Some(true)
+  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)
 
   def + (keyword: String, template: String): Completion =
     new Completion(
@@ -281,9 +282,6 @@
 
   /* symbols with abbreviations */
 
-  private def is_symbol(name: String): Boolean =
-    Symbol.names.isDefinedAt(name)
-
   private def add_symbols(): Completion =
   {
     val words =