clarified description;
authorwenzelm
Sat Mar 08 12:31:23 2014 +0100 (2014-03-08)
changeset 559934c17e46c44c1
parent 55992 1e7f04ba8196
child 55994 1c42ebdb3a58
clarified description;
tuned;
src/Pure/General/completion.scala
     1.1 --- a/src/Pure/General/completion.scala	Sat Mar 08 11:50:12 2014 +0100
     1.2 +++ b/src/Pure/General/completion.scala	Sat Mar 08 12:31:23 2014 +0100
     1.3 @@ -334,7 +334,7 @@
     1.4                val ok =
     1.5                  if (a == Completion.antiquote) language_context.antiquotes
     1.6                  else language_context.symbols || Completion.default_abbrs.isDefinedAt(a)
     1.7 -              if (ok) Some(((a, abbrevs.map(_._2)), caret))
     1.8 +              if (ok) Some(((a, abbrevs), caret))
     1.9                else None
    1.10            }
    1.11          case _ => None
    1.12 @@ -360,27 +360,30 @@
    1.13            {
    1.14              val completions =
    1.15                for {
    1.16 -                s <- words_lex.completions(word)
    1.17 -                if (if (is_keyword(s)) language_context.is_outer else language_context.symbols)
    1.18 -                r <- words_map.get_list(s)
    1.19 -              } yield r
    1.20 +                complete_word <- words_lex.completions(word)
    1.21 +                ok =
    1.22 +                  if (is_keyword(complete_word)) language_context.is_outer
    1.23 +                  else language_context.symbols
    1.24 +                if ok
    1.25 +                completion <- words_map.get_list(complete_word)
    1.26 +              } yield (complete_word, completion)
    1.27              (((word, completions), end))
    1.28            })
    1.29        }
    1.30  
    1.31      (abbrevs_result orElse words_result) match {
    1.32 -      case Some(((original, completions0), end)) if !completions0.isEmpty =>
    1.33 +      case Some(((original, completions), end)) if !completions.isEmpty =>
    1.34          val range = Text.Range(- original.length, 0) + end + start
    1.35          val immediate =
    1.36            explicit ||
    1.37              (!Completion.Word_Parsers.is_word(original) &&
    1.38                Character.codePointCount(original, 0, original.length) > 1)
    1.39 -        val unique = completions0.length == 1
    1.40 +        val unique = completions.length == 1
    1.41  
    1.42 -        val completions1 = completions0.map(decode(_))
    1.43          val items =
    1.44            for {
    1.45 -            (name0, name1) <- completions0 zip completions1
    1.46 +            (complete_word, name0) <- completions
    1.47 +            name1 = decode(name0)
    1.48              if name1 != original
    1.49              (s1, s2) =
    1.50                space_explode(Completion.caret_indicator, name1) match {
    1.51 @@ -393,10 +396,10 @@
    1.52                  if (name0 == name1) List(name0)
    1.53                  else List(name1, "(symbol " + quote(name0) + ")")
    1.54                }
    1.55 -              else if (move != 0 || is_keyword_template(name0))
    1.56 -                List(name1, "(template)")
    1.57 -              else if (is_keyword(name0))
    1.58 -                List(name1, "(keyword)")
    1.59 +              else if (is_keyword_template(complete_word))
    1.60 +                List(name1, "(template " + quote(complete_word) + ")")
    1.61 +              else if (move != 0) List(name1, "(template)")
    1.62 +              else if (is_keyword(complete_word)) List(name1, "(keyword)")
    1.63                else List(name1)
    1.64            }
    1.65            yield Completion.Item(range, original, name1, description, s1 + s2, move, immediate)