src/Pure/General/completion.scala
changeset 55993 4c17e46c44c1
parent 55992 1e7f04ba8196
child 55994 1c42ebdb3a58
equal deleted inserted replaced
55992:1e7f04ba8196 55993:4c17e46c44c1
   332             case Nil => None
   332             case Nil => None
   333             case (a, _) :: _ =>
   333             case (a, _) :: _ =>
   334               val ok =
   334               val ok =
   335                 if (a == Completion.antiquote) language_context.antiquotes
   335                 if (a == Completion.antiquote) language_context.antiquotes
   336                 else language_context.symbols || Completion.default_abbrs.isDefinedAt(a)
   336                 else language_context.symbols || Completion.default_abbrs.isDefinedAt(a)
   337               if (ok) Some(((a, abbrevs.map(_._2)), caret))
   337               if (ok) Some(((a, abbrevs), caret))
   338               else None
   338               else None
   339           }
   339           }
   340         case _ => None
   340         case _ => None
   341       }
   341       }
   342     }
   342     }
   358           }
   358           }
   359         opt_word.map(word =>
   359         opt_word.map(word =>
   360           {
   360           {
   361             val completions =
   361             val completions =
   362               for {
   362               for {
   363                 s <- words_lex.completions(word)
   363                 complete_word <- words_lex.completions(word)
   364                 if (if (is_keyword(s)) language_context.is_outer else language_context.symbols)
   364                 ok =
   365                 r <- words_map.get_list(s)
   365                   if (is_keyword(complete_word)) language_context.is_outer
   366               } yield r
   366                   else language_context.symbols
       
   367                 if ok
       
   368                 completion <- words_map.get_list(complete_word)
       
   369               } yield (complete_word, completion)
   367             (((word, completions), end))
   370             (((word, completions), end))
   368           })
   371           })
   369       }
   372       }
   370 
   373 
   371     (abbrevs_result orElse words_result) match {
   374     (abbrevs_result orElse words_result) match {
   372       case Some(((original, completions0), end)) if !completions0.isEmpty =>
   375       case Some(((original, completions), end)) if !completions.isEmpty =>
   373         val range = Text.Range(- original.length, 0) + end + start
   376         val range = Text.Range(- original.length, 0) + end + start
   374         val immediate =
   377         val immediate =
   375           explicit ||
   378           explicit ||
   376             (!Completion.Word_Parsers.is_word(original) &&
   379             (!Completion.Word_Parsers.is_word(original) &&
   377               Character.codePointCount(original, 0, original.length) > 1)
   380               Character.codePointCount(original, 0, original.length) > 1)
   378         val unique = completions0.length == 1
   381         val unique = completions.length == 1
   379 
   382 
   380         val completions1 = completions0.map(decode(_))
       
   381         val items =
   383         val items =
   382           for {
   384           for {
   383             (name0, name1) <- completions0 zip completions1
   385             (complete_word, name0) <- completions
       
   386             name1 = decode(name0)
   384             if name1 != original
   387             if name1 != original
   385             (s1, s2) =
   388             (s1, s2) =
   386               space_explode(Completion.caret_indicator, name1) match {
   389               space_explode(Completion.caret_indicator, name1) match {
   387                 case List(s1, s2) => (s1, s2)
   390                 case List(s1, s2) => (s1, s2)
   388                 case _ => (name1, "")
   391                 case _ => (name1, "")
   391             description =
   394             description =
   392               if (is_symbol(name0)) {
   395               if (is_symbol(name0)) {
   393                 if (name0 == name1) List(name0)
   396                 if (name0 == name1) List(name0)
   394                 else List(name1, "(symbol " + quote(name0) + ")")
   397                 else List(name1, "(symbol " + quote(name0) + ")")
   395               }
   398               }
   396               else if (move != 0 || is_keyword_template(name0))
   399               else if (is_keyword_template(complete_word))
   397                 List(name1, "(template)")
   400                 List(name1, "(template " + quote(complete_word) + ")")
   398               else if (is_keyword(name0))
   401               else if (move != 0) List(name1, "(template)")
   399                 List(name1, "(keyword)")
   402               else if (is_keyword(complete_word)) List(name1, "(keyword)")
   400               else List(name1)
   403               else List(name1)
   401           }
   404           }
   402           yield Completion.Item(range, original, name1, description, s1 + s2, move, immediate)
   405           yield Completion.Item(range, original, name1, description, s1 + s2, move, immediate)
   403 
   406 
   404         if (items.isEmpty) None
   407         if (items.isEmpty) None