src/Pure/General/completion.scala
changeset 66055 07175635f78c
parent 65344 b99283eed13c
child 66056 cf35abfb9ebc
equal deleted inserted replaced
66054:fb0eea226a4d 66055:07175635f78c
   187   case class Names(total: Int, names: List[(String, (String, String))]) extends Semantic
   187   case class Names(total: Int, names: List[(String, (String, String))]) extends Semantic
   188   {
   188   {
   189     def complete(
   189     def complete(
   190       range: Text.Range,
   190       range: Text.Range,
   191       history: Completion.History,
   191       history: Completion.History,
   192       do_decode: Boolean,
   192       unicode: Boolean,
   193       original: String): Option[Completion.Result] =
   193       original: String): Option[Completion.Result] =
   194     {
   194     {
   195       def decode(s: String): String = if (do_decode) Symbol.decode(s) else s
   195       def decode(s: String): String = if (unicode) Symbol.decode(s) else s
   196       val items =
   196       val items =
   197         for {
   197         for {
   198           (xname, (kind, name)) <- names
   198           (xname, (kind, name)) <- names
   199           xname1 = decode(xname)
   199           xname1 = decode(xname)
   200           if xname1 != original
   200           if xname1 != original
   406 
   406 
   407   /* complete */
   407   /* complete */
   408 
   408 
   409   def complete(
   409   def complete(
   410     history: Completion.History,
   410     history: Completion.History,
   411     do_decode: Boolean,
   411     unicode: Boolean,
   412     explicit: Boolean,
   412     explicit: Boolean,
   413     start: Text.Offset,
   413     start: Text.Offset,
   414     text: CharSequence,
   414     text: CharSequence,
   415     caret: Int,
   415     caret: Int,
   416     language_context: Completion.Language_Context): Option[Completion.Result] =
   416     language_context: Completion.Language_Context): Option[Completion.Result] =
   417   {
   417   {
   418     def decode(s: String): String = if (do_decode) Symbol.decode(s) else s
   418     def decode(s: String): String = if (unicode) Symbol.decode(s) else s
   419     val length = text.length
   419     val length = text.length
   420 
   420 
   421     val abbrevs_result =
   421     val abbrevs_result =
   422     {
   422     {
   423       val reverse_in = new Library.Reverse(text.subSequence(0, caret))
   423       val reverse_in = new Library.Reverse(text.subSequence(0, caret))