more accurate description;
authorwenzelm
Fri Mar 07 19:28:34 2014 +0100 (2014-03-07)
changeset 55982b719781c7396
parent 55981 66739f41d5b2
child 55983 fc5977bd4829
more accurate description;
src/Pure/General/completion.scala
     1.1 --- a/src/Pure/General/completion.scala	Fri Mar 07 17:07:30 2014 +0100
     1.2 +++ b/src/Pure/General/completion.scala	Fri Mar 07 19:28:34 2014 +0100
     1.3 @@ -334,7 +334,8 @@
     1.4      }
     1.5  
     1.6      val words_result =
     1.7 -      abbrevs_result orElse {
     1.8 +      if (abbrevs_result.isDefined) None
     1.9 +      else {
    1.10          val end =
    1.11            if (extend_word) Completion.Word_Parsers.extend_word(text, caret)
    1.12            else caret
    1.13 @@ -359,7 +360,7 @@
    1.14          }
    1.15        }
    1.16  
    1.17 -    words_result match {
    1.18 +    (abbrevs_result orElse words_result) match {
    1.19        case Some(((word, cs), end)) =>
    1.20          val range = Text.Range(- word.length, 0) + end + start
    1.21          val ds = cs.map(decode(_)).filter(_ != word)
    1.22 @@ -379,7 +380,7 @@
    1.23                val move = - s2.length
    1.24                val description =
    1.25                  if (move != 0) List(name1, "(template)")
    1.26 -                else if (keywords(name)) List(name1, "(keyword)")
    1.27 +                else if (words_result.isDefined && keywords(name)) List(name1, "(keyword)")
    1.28                  else if (Symbol.names.isDefinedAt(name) && name != name1)
    1.29                    List(name1, "(symbol " + quote(name) + ")")
    1.30                  else List(name1)