more strict discrimination: symbols vs. keywords could overlap;
authorwenzelm
Fri Mar 07 20:32:48 2014 +0100 (2014-03-07)
changeset 5598661b0021ed674
parent 55985 594afef0dd89
child 55987 52c22561996d
more strict discrimination: symbols vs. keywords could overlap;
src/Pure/General/completion.scala
     1.1 --- a/src/Pure/General/completion.scala	Fri Mar 07 20:24:14 2014 +0100
     1.2 +++ b/src/Pure/General/completion.scala	Fri Mar 07 20:32:48 2014 +0100
     1.3 @@ -265,8 +265,9 @@
     1.4  {
     1.5    /* keywords */
     1.6  
     1.7 -  private def is_keyword(name: String): Boolean = keywords.isDefinedAt(name)
     1.8 -  private def is_keyword_template(name: String): Boolean = keywords.get(name) == Some(true)
     1.9 +  private def is_symbol(name: String): Boolean = Symbol.names.isDefinedAt(name)
    1.10 +  private def is_keyword(name: String): Boolean = !is_symbol(name) && keywords.isDefinedAt(name)
    1.11 +  private def is_keyword_template(name: String): Boolean = is_keyword(name) && keywords(name)
    1.12  
    1.13    def + (keyword: String, template: String): Completion =
    1.14      new Completion(
    1.15 @@ -281,9 +282,6 @@
    1.16  
    1.17    /* symbols with abbreviations */
    1.18  
    1.19 -  private def is_symbol(name: String): Boolean =
    1.20 -    Symbol.names.isDefinedAt(name)
    1.21 -
    1.22    private def add_symbols(): Completion =
    1.23    {
    1.24      val words =