more accurate description;
authorwenzelm
Fri Mar 07 20:12:38 2014 +0100 (2014-03-07)
changeset 559842aaecd737d75
parent 55983 fc5977bd4829
child 55985 594afef0dd89
more accurate description;
src/Pure/General/completion.scala
     1.1 --- a/src/Pure/General/completion.scala	Fri Mar 07 19:56:31 2014 +0100
     1.2 +++ b/src/Pure/General/completion.scala	Fri Mar 07 20:12:38 2014 +0100
     1.3 @@ -257,7 +257,7 @@
     1.4  }
     1.5  
     1.6  final class Completion private(
     1.7 -  keywords: Set[String] = Set.empty,
     1.8 +  keywords: Map[String, Boolean] = Map.empty,
     1.9    words_lex: Scan.Lexicon = Scan.Lexicon.empty,
    1.10    words_map: Multi_Map[String, String] = Multi_Map.empty,
    1.11    abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty,
    1.12 @@ -265,11 +265,14 @@
    1.13  {
    1.14    /* keywords */
    1.15  
    1.16 -  def + (keyword: String, replace: String): Completion =
    1.17 +  def is_keyword(name: String): Boolean = keywords.isDefinedAt(name)
    1.18 +  def is_keyword_template(name: String): Boolean = keywords.get(name) == Some(true)
    1.19 +
    1.20 +  def + (keyword: String, template: String): Completion =
    1.21      new Completion(
    1.22 -      keywords + keyword,
    1.23 +      keywords + (keyword -> (keyword != template)),
    1.24        words_lex + keyword,
    1.25 -      words_map + (keyword -> replace),
    1.26 +      words_map + (keyword -> template),
    1.27        abbrevs_lex,
    1.28        abbrevs_map)
    1.29  
    1.30 @@ -354,7 +357,7 @@
    1.31              val completions =
    1.32                for {
    1.33                  s <- words_lex.completions(word)
    1.34 -                if (if (keywords(s)) language_context.is_outer else language_context.symbols)
    1.35 +                if (if (is_keyword(s)) language_context.is_outer else language_context.symbols)
    1.36                  r <- words_map.get_list(s)
    1.37                } yield r
    1.38              if (completions.isEmpty) None
    1.39 @@ -384,10 +387,14 @@
    1.40                  }
    1.41                move = - s2.length
    1.42                description =
    1.43 -                if (move != 0) List(name1, "(template)")
    1.44 -                else if (words_result.isDefined && keywords(name0)) List(name1, "(keyword)")
    1.45 -                else if (Symbol.names.isDefinedAt(name0) && name0 != name1)
    1.46 -                  List(name1, "(symbol " + quote(name0) + ")")
    1.47 +                if (Symbol.names.isDefinedAt(name0)) {
    1.48 +                  if (name0 == name1) List(name0)
    1.49 +                  else List(name1, "(symbol " + quote(name0) + ")")
    1.50 +                }
    1.51 +                else if (move != 0 || is_keyword_template(name0))
    1.52 +                  List(name1, "(template)")
    1.53 +                else if (is_keyword(name0))
    1.54 +                  List(name1, "(keyword)")
    1.55                  else List(name1)
    1.56              }
    1.57              yield Completion.Item(range, original, name1, description, s1 + s2, move, immediate)