more strict discrimination: symbols vs. keywords could overlap;
--- 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 =