src/Pure/General/completion.scala
changeset 55977 ec4830499634
parent 55914 c5b752d549e3
child 55978 56645c447ee9
equal deleted inserted replaced
55976:43815ee659bc 55977:ec4830499634
   134           case XML.Elem(Markup(Markup.COMPLETION, _), body) =>
   134           case XML.Elem(Markup(Markup.COMPLETION, _), body) =>
   135             try {
   135             try {
   136               val (total, names) =
   136               val (total, names) =
   137               {
   137               {
   138                 import XML.Decode._
   138                 import XML.Decode._
   139                 pair(int, list(pair(string, string)))(body)
   139                 pair(int, list(pair(string, pair(string, string))))(body)
   140               }
   140               }
   141               Some(Names(info.range, total, names))
   141               Some(Names(info.range, total, names))
   142             }
   142             }
   143             catch { case _: XML.Error => None }
   143             catch { case _: XML.Error => None }
   144           case XML.Elem(Markup(Markup.NO_COMPLETION, _), _) =>
   144           case XML.Elem(Markup(Markup.NO_COMPLETION, _), _) =>
   146           case _ => None
   146           case _ => None
   147         }
   147         }
   148     }
   148     }
   149   }
   149   }
   150 
   150 
   151   sealed case class Names(range: Text.Range, total: Int, names: List[(String, String)])
   151   sealed case class Names(
       
   152     range: Text.Range, total: Int, names: List[(String, (String, String))])
   152   {
   153   {
   153     def no_completion: Boolean = total == 0 && names.isEmpty
   154     def no_completion: Boolean = total == 0 && names.isEmpty
   154 
   155 
   155     def complete(
   156     def complete(
   156       history: Completion.History,
   157       history: Completion.History,
   157       decode: Boolean,
   158       do_decode: Boolean,
   158       original: String): Option[Completion.Result] =
   159       original: String): Option[Completion.Result] =
   159     {
   160     {
       
   161       def decode(s: String): String = if (do_decode) Symbol.decode(s) else s
   160       val items =
   162       val items =
   161         for {
   163         for {
   162           (xname, name) <- names
   164           (xname, (kind, name)) <- names
   163           xname1 = (if (decode) Symbol.decode(xname) else xname)
   165           xname1 = decode(xname)
   164           if xname1 != original
   166           if xname1 != original
   165         } yield Item(range, original, name, xname1, xname1, 0, true)
   167           (full_name, descr_name) =
       
   168             if (kind == "") (name, quote(decode(name)))
       
   169             else (kind + "." + name, Library.plain_words(kind) + " " + quote(decode(name)))
       
   170           description = xname1 + "   (" + descr_name + ")"
       
   171         } yield Item(range, original, full_name, description, xname1, 0, true)
   166 
   172 
   167       if (items.isEmpty) None
   173       if (items.isEmpty) None
   168       else Some(Result(range, original, names.length == 1, items.sorted(history.ordering)))
   174       else Some(Result(range, original, names.length == 1, items.sorted(history.ordering)))
   169     }
   175     }
   170   }
   176   }
   296 
   302 
   297   /* complete */
   303   /* complete */
   298 
   304 
   299   def complete(
   305   def complete(
   300     history: Completion.History,
   306     history: Completion.History,
   301     decode: Boolean,
   307     do_decode: Boolean,
   302     explicit: Boolean,
   308     explicit: Boolean,
   303     start: Text.Offset,
   309     start: Text.Offset,
   304     text: CharSequence,
   310     text: CharSequence,
   305     caret: Int,
   311     caret: Int,
   306     extend_word: Boolean,
   312     extend_word: Boolean,
   307     language_context: Completion.Language_Context): Option[Completion.Result] =
   313     language_context: Completion.Language_Context): Option[Completion.Result] =
   308   {
   314   {
       
   315     def decode(s: String): String = if (do_decode) Symbol.decode(s) else s
   309     val length = text.length
   316     val length = text.length
   310 
   317 
   311     val abbrevs_result =
   318     val abbrevs_result =
   312     {
   319     {
   313       val reverse_in = new Library.Reverse(text.subSequence(0, caret))
   320       val reverse_in = new Library.Reverse(text.subSequence(0, caret))
   354       }
   361       }
   355 
   362 
   356     words_result match {
   363     words_result match {
   357       case Some(((word, cs), end)) =>
   364       case Some(((word, cs), end)) =>
   358         val range = Text.Range(- word.length, 0) + end + start
   365         val range = Text.Range(- word.length, 0) + end + start
   359         val ds = (if (decode) cs.map(Symbol.decode(_)) else cs).filter(_ != word)
   366         val ds = cs.map(decode(_)).filter(_ != word)
   360         if (ds.isEmpty) None
   367         if (ds.isEmpty) None
   361         else {
   368         else {
   362           val immediate =
   369           val immediate =
   363             !Completion.Word_Parsers.is_word(word) &&
   370             !Completion.Word_Parsers.is_word(word) &&
   364             Character.codePointCount(word, 0, word.length) > 1
   371             Character.codePointCount(word, 0, word.length) > 1
   365           val items =
   372           val items =
   366             ds.map(s => {
   373             for { (name, name1) <- cs zip ds }
       
   374             yield {
   367               val (s1, s2) =
   375               val (s1, s2) =
   368                 space_explode(Completion.caret_indicator, s) match {
   376                 space_explode(Completion.caret_indicator, name1) match {
   369                   case List(s1, s2) => (s1, s2)
   377                   case List(s1, s2) => (s1, s2)
   370                   case _ => (s, "")
   378                   case _ => (name1, "")
   371                 }
   379                 }
   372               Completion.Item(range, word, s, s, s1 + s2, - s2.length, explicit || immediate)
   380               val description =
   373             })
   381                 if (keywords(name)) name1 + "   (keyword)"
       
   382                 else if (Symbol.names.isDefinedAt(name) && name != name1)
       
   383                   name1 + "   (symbol " + quote(name) + ")"
       
   384                 else name1
       
   385               Completion.Item(
       
   386                 range, word, name1, description, s1 + s2, - s2.length, explicit || immediate)
       
   387             }
   374           Some(Completion.Result(range, word, cs.length == 1, items.sorted(history.ordering)))
   388           Some(Completion.Result(range, word, cs.length == 1, items.sorted(history.ordering)))
   375         }
   389         }
   376       case None => None
   390       case None => None
   377     }
   391     }
   378   }
   392   }