# HG changeset patch # User wenzelm # Date 1394278283 -3600 # Node ID 4c17e46c44c1f5337a56c9a8e33ba5d01b80fbf6 # Parent 1e7f04ba8196febc9bf15ddffd09ba81bb2462eb clarified description; tuned; diff -r 1e7f04ba8196 -r 4c17e46c44c1 src/Pure/General/completion.scala --- a/src/Pure/General/completion.scala Sat Mar 08 11:50:12 2014 +0100 +++ b/src/Pure/General/completion.scala Sat Mar 08 12:31:23 2014 +0100 @@ -334,7 +334,7 @@ val ok = if (a == Completion.antiquote) language_context.antiquotes else language_context.symbols || Completion.default_abbrs.isDefinedAt(a) - if (ok) Some(((a, abbrevs.map(_._2)), caret)) + if (ok) Some(((a, abbrevs), caret)) else None } case _ => None @@ -360,27 +360,30 @@ { val completions = for { - s <- words_lex.completions(word) - if (if (is_keyword(s)) language_context.is_outer else language_context.symbols) - r <- words_map.get_list(s) - } yield r + complete_word <- words_lex.completions(word) + ok = + if (is_keyword(complete_word)) language_context.is_outer + else language_context.symbols + if ok + completion <- words_map.get_list(complete_word) + } yield (complete_word, completion) (((word, completions), end)) }) } (abbrevs_result orElse words_result) match { - case Some(((original, completions0), end)) if !completions0.isEmpty => + case Some(((original, completions), end)) if !completions.isEmpty => val range = Text.Range(- original.length, 0) + end + start val immediate = explicit || (!Completion.Word_Parsers.is_word(original) && Character.codePointCount(original, 0, original.length) > 1) - val unique = completions0.length == 1 + val unique = completions.length == 1 - val completions1 = completions0.map(decode(_)) val items = for { - (name0, name1) <- completions0 zip completions1 + (complete_word, name0) <- completions + name1 = decode(name0) if name1 != original (s1, s2) = space_explode(Completion.caret_indicator, name1) match { @@ -393,10 +396,10 @@ if (name0 == name1) List(name0) else List(name1, "(symbol " + quote(name0) + ")") } - else if (move != 0 || is_keyword_template(name0)) - List(name1, "(template)") - else if (is_keyword(name0)) - List(name1, "(keyword)") + else if (is_keyword_template(complete_word)) + List(name1, "(template " + quote(complete_word) + ")") + else if (move != 0) List(name1, "(template)") + else if (is_keyword(complete_word)) List(name1, "(keyword)") else List(name1) } yield Completion.Item(range, original, name1, description, s1 + s2, move, immediate)