more strict discrimination: symbols vs. keywords could overlap;
authorwenzelm
Fri, 07 Mar 2014 20:32:48 +0100
changeset 55986 61b0021ed674
parent 55985 594afef0dd89
child 55987 52c22561996d
more strict discrimination: symbols vs. keywords could overlap;
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 =