src/Pure/General/completion.scala
author wenzelm
Mon Dec 01 15:21:49 2014 +0100 (2014-12-01)
changeset 59073 dcecfcc56dce
parent 57602 0f708666eb7c
child 59319 677615cba30d
permissions -rw-r--r--
more merge operations;
wenzelm@55673
     1
/*  Title:      Pure/General/completion.scala
wenzelm@31763
     2
    Author:     Makarius
wenzelm@31763
     3
wenzelm@55687
     4
Semantic completion within the formal context (reported names).
wenzelm@55674
     5
Syntactic completion of keywords and symbols, with abbreviations
wenzelm@55992
     6
(based on language context).
wenzelm@55992
     7
*/
wenzelm@31763
     8
wenzelm@31763
     9
package isabelle
wenzelm@31763
    10
wenzelm@55618
    11
wenzelm@53337
    12
import scala.collection.immutable.SortedMap
wenzelm@31763
    13
import scala.util.parsing.combinator.RegexParsers
wenzelm@57589
    14
import scala.util.matching.Regex
wenzelm@53337
    15
import scala.math.Ordering
wenzelm@31763
    16
wenzelm@31763
    17
wenzelm@46624
    18
object Completion
wenzelm@31763
    19
{
wenzelm@55694
    20
  /** completion result **/
wenzelm@53275
    21
wenzelm@53296
    22
  sealed case class Item(
wenzelm@55692
    23
    range: Text.Range,
wenzelm@53296
    24
    original: String,
wenzelm@55666
    25
    name: String,
wenzelm@55978
    26
    description: List[String],
wenzelm@53296
    27
    replacement: String,
wenzelm@55666
    28
    move: Int,
wenzelm@53296
    29
    immediate: Boolean)
wenzelm@53275
    30
wenzelm@55914
    31
  object Result
wenzelm@55914
    32
  {
wenzelm@55914
    33
    def empty(range: Text.Range): Result = Result(range, "", false, Nil)
wenzelm@56175
    34
    def merge(history: History, result1: Option[Result], result2: Option[Result]): Option[Result] =
wenzelm@56175
    35
      (result1, result2) match {
wenzelm@56175
    36
        case (_, None) => result1
wenzelm@56175
    37
        case (None, _) => result2
wenzelm@56175
    38
        case (Some(res1), Some(res2)) =>
wenzelm@56175
    39
          if (res1.range != res2.range || res1.original != res2.original) result1
wenzelm@56175
    40
          else {
wenzelm@56175
    41
            val items = (res1.items ::: res2.items).sorted(history.ordering)
wenzelm@56175
    42
            Some(Result(res1.range, res1.original, false, items))
wenzelm@56175
    43
          }
wenzelm@56175
    44
      }
wenzelm@55914
    45
  }
wenzelm@55914
    46
wenzelm@55693
    47
  sealed case class Result(
wenzelm@55693
    48
    range: Text.Range,
wenzelm@55693
    49
    original: String,
wenzelm@55693
    50
    unique: Boolean,
wenzelm@55693
    51
    items: List[Item])
wenzelm@53325
    52
wenzelm@53275
    53
wenzelm@46624
    54
wenzelm@53337
    55
  /** persistent history **/
wenzelm@53337
    56
wenzelm@53337
    57
  private val COMPLETION_HISTORY = Path.explode("$ISABELLE_HOME_USER/etc/completion_history")
wenzelm@53337
    58
wenzelm@53337
    59
  object History
wenzelm@53337
    60
  {
wenzelm@53337
    61
    val empty: History = new History()
wenzelm@53337
    62
wenzelm@53337
    63
    def load(): History =
wenzelm@53337
    64
    {
wenzelm@53337
    65
      def ignore_error(msg: String): Unit =
wenzelm@56782
    66
        Output.warning("Ignoring bad content of file " + COMPLETION_HISTORY +
wenzelm@53337
    67
          (if (msg == "") "" else "\n" + msg))
wenzelm@53337
    68
wenzelm@53337
    69
      val content =
wenzelm@53337
    70
        if (COMPLETION_HISTORY.is_file) {
wenzelm@53337
    71
          try {
wenzelm@53337
    72
            import XML.Decode._
wenzelm@53337
    73
            list(pair(Symbol.decode_string, int))(
wenzelm@53337
    74
              YXML.parse_body(File.read(COMPLETION_HISTORY)))
wenzelm@53337
    75
          }
wenzelm@53337
    76
          catch {
wenzelm@53337
    77
            case ERROR(msg) => ignore_error(msg); Nil
wenzelm@53337
    78
            case _: XML.Error => ignore_error(""); Nil
wenzelm@53337
    79
          }
wenzelm@53337
    80
        }
wenzelm@53337
    81
        else Nil
wenzelm@53337
    82
      (empty /: content)(_ + _)
wenzelm@53337
    83
    }
wenzelm@53337
    84
  }
wenzelm@53337
    85
wenzelm@53337
    86
  final class History private(rep: SortedMap[String, Int] = SortedMap.empty)
wenzelm@53337
    87
  {
wenzelm@53337
    88
    override def toString: String = rep.mkString("Completion.History(", ",", ")")
wenzelm@53337
    89
wenzelm@56878
    90
    def frequency(name: String): Int =
wenzelm@56878
    91
      default_frequency(Symbol.encode(name)) getOrElse
wenzelm@56878
    92
      rep.getOrElse(name, 0)
wenzelm@53337
    93
wenzelm@53337
    94
    def + (entry: (String, Int)): History =
wenzelm@53337
    95
    {
wenzelm@53337
    96
      val (name, freq) = entry
wenzelm@56564
    97
      if (name == "") this
wenzelm@56564
    98
      else new History(rep + (name -> (frequency(name) + freq)))
wenzelm@53337
    99
    }
wenzelm@53337
   100
wenzelm@53337
   101
    def ordering: Ordering[Item] =
wenzelm@53337
   102
      new Ordering[Item] {
wenzelm@53337
   103
        def compare(item1: Item, item2: Item): Int =
wenzelm@56162
   104
          frequency(item2.name) compare frequency(item1.name)
wenzelm@56162
   105
      }
wenzelm@56162
   106
wenzelm@53337
   107
    def save()
wenzelm@53337
   108
    {
wenzelm@53337
   109
      Isabelle_System.mkdirs(COMPLETION_HISTORY.dir)
wenzelm@53337
   110
      File.write_backup(COMPLETION_HISTORY,
wenzelm@53337
   111
        {
wenzelm@53337
   112
          import XML.Encode._
wenzelm@53337
   113
          YXML.string_of_body(list(pair(Symbol.encode_string, int))(rep.toList))
wenzelm@53337
   114
        })
wenzelm@53337
   115
    }
wenzelm@53337
   116
  }
wenzelm@53337
   117
wenzelm@53337
   118
  class History_Variable
wenzelm@53337
   119
  {
wenzelm@53337
   120
    private var history = History.empty
wenzelm@53337
   121
    def value: History = synchronized { history }
wenzelm@53337
   122
wenzelm@53337
   123
    def load()
wenzelm@53337
   124
    {
wenzelm@53337
   125
      val h = History.load()
wenzelm@53337
   126
      synchronized { history = h }
wenzelm@53337
   127
    }
wenzelm@53337
   128
wenzelm@53337
   129
    def update(item: Item, freq: Int = 1): Unit = synchronized {
wenzelm@55666
   130
      history = history + (item.name -> freq)
wenzelm@53337
   131
    }
wenzelm@53337
   132
  }
wenzelm@53337
   133
wenzelm@53337
   134
wenzelm@55694
   135
wenzelm@55694
   136
  /** semantic completion **/
wenzelm@55694
   137
wenzelm@56173
   138
  object Semantic
wenzelm@55694
   139
  {
wenzelm@55694
   140
    object Info
wenzelm@55694
   141
    {
wenzelm@56173
   142
      def unapply(info: Text.Markup): Option[Text.Info[Semantic]] =
wenzelm@55694
   143
        info.info match {
wenzelm@55694
   144
          case XML.Elem(Markup(Markup.COMPLETION, _), body) =>
wenzelm@55694
   145
            try {
wenzelm@55694
   146
              val (total, names) =
wenzelm@55694
   147
              {
wenzelm@55694
   148
                import XML.Decode._
wenzelm@55977
   149
                pair(int, list(pair(string, pair(string, string))))(body)
wenzelm@55694
   150
              }
wenzelm@56173
   151
              Some(Text.Info(info.range, Names(total, names)))
wenzelm@55694
   152
            }
wenzelm@55694
   153
            catch { case _: XML.Error => None }
wenzelm@55914
   154
          case XML.Elem(Markup(Markup.NO_COMPLETION, _), _) =>
wenzelm@56173
   155
            Some(Text.Info(info.range, No_Completion))
wenzelm@55694
   156
          case _ => None
wenzelm@55694
   157
        }
wenzelm@55694
   158
    }
wenzelm@55694
   159
  }
wenzelm@55694
   160
wenzelm@56173
   161
  sealed abstract class Semantic
wenzelm@56175
   162
  case object No_Completion extends Semantic
wenzelm@56175
   163
  case class Names(total: Int, names: List[(String, (String, String))]) extends Semantic
wenzelm@55694
   164
  {
wenzelm@55694
   165
    def complete(
wenzelm@56173
   166
      range: Text.Range,
wenzelm@56173
   167
      history: Completion.History,
wenzelm@56173
   168
      do_decode: Boolean,
wenzelm@55694
   169
      original: String): Option[Completion.Result] =
wenzelm@55694
   170
    {
wenzelm@55977
   171
      def decode(s: String): String = if (do_decode) Symbol.decode(s) else s
wenzelm@55694
   172
      val items =
wenzelm@55694
   173
        for {
wenzelm@55977
   174
          (xname, (kind, name)) <- names
wenzelm@55977
   175
          xname1 = decode(xname)
wenzelm@55694
   176
          if xname1 != original
wenzelm@55977
   177
          (full_name, descr_name) =
wenzelm@55977
   178
            if (kind == "") (name, quote(decode(name)))
wenzelm@56600
   179
            else
wenzelm@56800
   180
             (Long_Name.qualify(kind, name),
wenzelm@56600
   181
              Word.implode(Word.explode('_', kind)) + " " + quote(decode(name)))
wenzelm@55978
   182
          description = List(xname1, "(" + descr_name + ")")
wenzelm@55977
   183
        } yield Item(range, original, full_name, description, xname1, 0, true)
wenzelm@55694
   184
wenzelm@55694
   185
      if (items.isEmpty) None
wenzelm@55694
   186
      else Some(Result(range, original, names.length == 1, items.sorted(history.ordering)))
wenzelm@55694
   187
    }
wenzelm@55694
   188
  }
wenzelm@55694
   189
wenzelm@55694
   190
wenzelm@55694
   191
wenzelm@55694
   192
  /** syntactic completion **/
wenzelm@55694
   193
wenzelm@55694
   194
  /* language context */
wenzelm@55694
   195
wenzelm@55749
   196
  object Language_Context
wenzelm@55694
   197
  {
wenzelm@55749
   198
    val outer = Language_Context("", true, false)
wenzelm@55749
   199
    val inner = Language_Context(Markup.Language.UNKNOWN, true, false)
wenzelm@55749
   200
    val ML_outer = Language_Context(Markup.Language.ML, false, true)
wenzelm@55749
   201
    val ML_inner = Language_Context(Markup.Language.ML, true, false)
wenzelm@56278
   202
    val SML_outer = Language_Context(Markup.Language.SML, false, false)
wenzelm@55694
   203
  }
wenzelm@55694
   204
wenzelm@55749
   205
  sealed case class Language_Context(language: String, symbols: Boolean, antiquotes: Boolean)
wenzelm@55694
   206
  {
wenzelm@55694
   207
    def is_outer: Boolean = language == ""
wenzelm@55694
   208
  }
wenzelm@55694
   209
wenzelm@55694
   210
wenzelm@55694
   211
  /* init */
wenzelm@55694
   212
wenzelm@55694
   213
  val empty: Completion = new Completion()
wenzelm@55694
   214
  def init(): Completion = empty.add_symbols()
wenzelm@55694
   215
wenzelm@55694
   216
wenzelm@55694
   217
  /* word parsers */
wenzelm@31763
   218
wenzelm@55615
   219
  private object Word_Parsers extends RegexParsers
wenzelm@31763
   220
  {
wenzelm@31763
   221
    override val whiteSpace = "".r
wenzelm@31763
   222
wenzelm@57589
   223
    private val symbol_regex: Regex = """\\<\^?[A-Za-z0-9_']+>""".r
wenzelm@57589
   224
    def is_symbol(s: CharSequence): Boolean = symbol_regex.pattern.matcher(s).matches
wenzelm@57589
   225
wenzelm@55615
   226
    private def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r
wenzelm@55615
   227
    private def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r
wenzelm@55615
   228
    private def escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r
wenzelm@55615
   229
wenzelm@56039
   230
    private val word_regex = "[a-zA-Z0-9_'.]+".r
wenzelm@55615
   231
    private def word: Parser[String] = word_regex
wenzelm@56039
   232
    private def word3: Parser[String] = "[a-zA-Z0-9_'.]{3,}".r
wenzelm@55996
   233
    private def underscores: Parser[String] = "_*".r
wenzelm@55615
   234
wenzelm@55813
   235
    def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
wenzelm@56042
   236
    def is_word_char(c: Char): Boolean = Symbol.is_ascii_letdig(c) || c == '.'
wenzelm@31763
   237
wenzelm@55813
   238
    def read_symbol(in: CharSequence): Option[String] =
wenzelm@55813
   239
    {
wenzelm@55813
   240
      val reverse_in = new Library.Reverse(in)
wenzelm@55813
   241
      parse(reverse_symbol ^^ (_.reverse), reverse_in) match {
wenzelm@55813
   242
        case Success(result, _) => Some(result)
wenzelm@55813
   243
        case _ => None
wenzelm@55813
   244
      }
wenzelm@55813
   245
    }
wenzelm@55813
   246
wenzelm@55996
   247
    def read_word(explicit: Boolean, in: CharSequence): Option[(String, String)] =
wenzelm@31763
   248
    {
wenzelm@53322
   249
      val parse_word = if (explicit) word else word3
wenzelm@37072
   250
      val reverse_in = new Library.Reverse(in)
wenzelm@55996
   251
      val parser =
wenzelm@55996
   252
        (reverse_symbol | reverse_symb | escape) ^^ (x => (x.reverse, "")) |
wenzelm@56221
   253
        underscores ~ parse_word ~ opt("?") ^^
wenzelm@56221
   254
        { case x ~ y ~ z => (z.getOrElse("") + y.reverse, x) }
wenzelm@55996
   255
      parse(parser, reverse_in) match {
wenzelm@31763
   256
        case Success(result, _) => Some(result)
wenzelm@31763
   257
        case _ => None
wenzelm@31763
   258
      }
wenzelm@31763
   259
    }
wenzelm@31763
   260
  }
wenzelm@55666
   261
wenzelm@55666
   262
wenzelm@55666
   263
  /* abbreviations */
wenzelm@55666
   264
wenzelm@56661
   265
  private val caret_indicator = '\u0007'
wenzelm@55666
   266
  private val antiquote = "@{"
wenzelm@56878
   267
wenzelm@55666
   268
  private val default_abbrs =
wenzelm@56878
   269
    List("@{" -> "@{\u0007}",
wenzelm@56878
   270
      "`" -> "\\<close>",
wenzelm@56878
   271
      "`" -> "\\<open>",
wenzelm@56878
   272
      "`" -> "\\<open>\u0007\\<close>")
wenzelm@56878
   273
wenzelm@56878
   274
  private def default_frequency(name: String): Option[Int] =
wenzelm@56878
   275
    default_abbrs.iterator.map(_._2).zipWithIndex.find(_._1 == name).map(_._2)
wenzelm@31763
   276
}
wenzelm@31763
   277
wenzelm@46712
   278
final class Completion private(
wenzelm@59073
   279
  protected val keywords: Map[String, Boolean] = Map.empty,
wenzelm@59073
   280
  protected val words_lex: Scan.Lexicon = Scan.Lexicon.empty,
wenzelm@59073
   281
  protected val words_map: Multi_Map[String, String] = Multi_Map.empty,
wenzelm@59073
   282
  protected val abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty,
wenzelm@59073
   283
  protected val abbrevs_map: Multi_Map[String, (String, String)] = Multi_Map.empty)
wenzelm@31763
   284
{
wenzelm@59073
   285
  /* merge */
wenzelm@59073
   286
wenzelm@59073
   287
  def is_empty: Boolean =
wenzelm@59073
   288
    keywords.isEmpty &&
wenzelm@59073
   289
    words_lex.is_empty &&
wenzelm@59073
   290
    words_map.isEmpty &&
wenzelm@59073
   291
    abbrevs_lex.is_empty &&
wenzelm@59073
   292
    abbrevs_map.isEmpty
wenzelm@59073
   293
wenzelm@59073
   294
  def ++ (other: Completion): Completion =
wenzelm@59073
   295
    if (this eq other) this
wenzelm@59073
   296
    else if (is_empty) other
wenzelm@59073
   297
    else {
wenzelm@59073
   298
      val keywords1 =
wenzelm@59073
   299
        (keywords /: other.keywords) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
wenzelm@59073
   300
      val words_lex1 = words_lex ++ other.words_lex
wenzelm@59073
   301
      val words_map1 = words_map ++ other.words_map
wenzelm@59073
   302
      val abbrevs_lex1 = abbrevs_lex ++ other.abbrevs_lex
wenzelm@59073
   303
      val abbrevs_map1 = abbrevs_map ++ other.abbrevs_map
wenzelm@59073
   304
      new Completion(keywords1, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1)
wenzelm@59073
   305
    }
wenzelm@59073
   306
wenzelm@59073
   307
wenzelm@55983
   308
  /* keywords */
wenzelm@31763
   309
wenzelm@55986
   310
  private def is_symbol(name: String): Boolean = Symbol.names.isDefinedAt(name)
wenzelm@55986
   311
  private def is_keyword(name: String): Boolean = !is_symbol(name) && keywords.isDefinedAt(name)
wenzelm@56001
   312
  private def is_keyword_template(name: String, template: Boolean): Boolean =
wenzelm@56001
   313
    is_keyword(name) && keywords(name) == template
wenzelm@55984
   314
wenzelm@55984
   315
  def + (keyword: String, template: String): Completion =
wenzelm@46624
   316
    new Completion(
wenzelm@55984
   317
      keywords + (keyword -> (keyword != template)),
wenzelm@46624
   318
      words_lex + keyword,
wenzelm@55984
   319
      words_map + (keyword -> template),
wenzelm@46624
   320
      abbrevs_lex,
wenzelm@46624
   321
      abbrevs_map)
wenzelm@31763
   322
wenzelm@40533
   323
  def + (keyword: String): Completion = this + (keyword, keyword)
wenzelm@40533
   324
wenzelm@55983
   325
wenzelm@55983
   326
  /* symbols with abbreviations */
wenzelm@55983
   327
wenzelm@46624
   328
  private def add_symbols(): Completion =
wenzelm@31763
   329
  {
wenzelm@31763
   330
    val words =
wenzelm@55615
   331
      (for ((x, _) <- Symbol.names.toList) yield (x, x)) :::
wenzelm@55615
   332
      (for ((x, y) <- Symbol.names.toList) yield ("\\" + y, x)) :::
wenzelm@55615
   333
      (for ((x, y) <- Symbol.abbrevs.toList if Completion.Word_Parsers.is_word(y)) yield (y, x))
wenzelm@31763
   334
wenzelm@55666
   335
    val symbol_abbrs =
wenzelm@55615
   336
      (for ((x, y) <- Symbol.abbrevs.iterator if !Completion.Word_Parsers.is_word(y))
wenzelm@55666
   337
        yield (y, x)).toList
wenzelm@55666
   338
wenzelm@55666
   339
    val abbrs =
wenzelm@56591
   340
      for ((a, b) <- symbol_abbrs ::: Completion.default_abbrs)
wenzelm@55666
   341
        yield (a.reverse, (a, b))
wenzelm@31763
   342
wenzelm@46624
   343
    new Completion(
wenzelm@55615
   344
      keywords,
wenzelm@46624
   345
      words_lex ++ words.map(_._1),
wenzelm@46624
   346
      words_map ++ words,
wenzelm@46624
   347
      abbrevs_lex ++ abbrs.map(_._1),
wenzelm@46624
   348
      abbrevs_map ++ abbrs)
wenzelm@31763
   349
  }
wenzelm@31763
   350
wenzelm@31763
   351
wenzelm@31763
   352
  /* complete */
wenzelm@31763
   353
wenzelm@53337
   354
  def complete(
wenzelm@53337
   355
    history: Completion.History,
wenzelm@55977
   356
    do_decode: Boolean,
wenzelm@53337
   357
    explicit: Boolean,
wenzelm@55813
   358
    start: Text.Offset,
wenzelm@55615
   359
    text: CharSequence,
wenzelm@55813
   360
    caret: Int,
wenzelm@55749
   361
    language_context: Completion.Language_Context): Option[Completion.Result] =
wenzelm@31763
   362
  {
wenzelm@55977
   363
    def decode(s: String): String = if (do_decode) Symbol.decode(s) else s
wenzelm@55813
   364
    val length = text.length
wenzelm@55813
   365
wenzelm@55615
   366
    val abbrevs_result =
wenzelm@55813
   367
    {
wenzelm@55813
   368
      val reverse_in = new Library.Reverse(text.subSequence(0, caret))
wenzelm@55813
   369
      Scan.Parsers.parse(Scan.Parsers.literal(abbrevs_lex), reverse_in) match {
wenzelm@55666
   370
        case Scan.Parsers.Success(reverse_a, _) =>
wenzelm@55666
   371
          val abbrevs = abbrevs_map.get_list(reverse_a)
wenzelm@55666
   372
          abbrevs match {
wenzelm@55666
   373
            case Nil => None
wenzelm@55666
   374
            case (a, _) :: _ =>
wenzelm@55666
   375
              val ok =
wenzelm@55749
   376
                if (a == Completion.antiquote) language_context.antiquotes
wenzelm@57589
   377
                else
wenzelm@57589
   378
                  language_context.symbols ||
wenzelm@57589
   379
                  Completion.default_abbrs.exists(_._1 == a) ||
wenzelm@57589
   380
                  Completion.Word_Parsers.is_symbol(a)
wenzelm@57588
   381
              if (ok) Some((a, abbrevs))
wenzelm@55813
   382
              else None
wenzelm@55666
   383
          }
wenzelm@55666
   384
        case _ => None
wenzelm@55666
   385
      }
wenzelm@55813
   386
    }
wenzelm@55615
   387
wenzelm@55615
   388
    val words_result =
wenzelm@55982
   389
      if (abbrevs_result.isDefined) None
wenzelm@55982
   390
      else {
wenzelm@57602
   391
        val word_context =
wenzelm@57602
   392
          caret < length && Completion.Word_Parsers.is_word_char(text.charAt(caret))
wenzelm@55996
   393
        val result =
wenzelm@57588
   394
          Completion.Word_Parsers.read_symbol(text.subSequence(0, caret)) match {
wenzelm@55996
   395
            case Some(symbol) => Some((symbol, ""))
wenzelm@57588
   396
            case None => Completion.Word_Parsers.read_word(explicit, text.subSequence(0, caret))
wenzelm@55992
   397
          }
wenzelm@55996
   398
        result.map(
wenzelm@55992
   399
          {
wenzelm@55996
   400
            case (word, underscores) =>
wenzelm@55996
   401
              val complete_words = words_lex.completions(word)
wenzelm@55996
   402
              val full_word = word + underscores
wenzelm@55996
   403
              val completions =
wenzelm@56001
   404
                if (complete_words.contains(full_word) && is_keyword_template(full_word, false)) Nil
wenzelm@55996
   405
                else
wenzelm@55996
   406
                  for {
wenzelm@55996
   407
                    complete_word <- complete_words
wenzelm@55996
   408
                    ok =
wenzelm@57602
   409
                      if (is_keyword(complete_word)) !word_context && language_context.is_outer
wenzelm@55996
   410
                      else language_context.symbols
wenzelm@55996
   411
                    if ok
wenzelm@55996
   412
                    completion <- words_map.get_list(complete_word)
wenzelm@55996
   413
                  } yield (complete_word, completion)
wenzelm@57588
   414
              ((full_word, completions))
wenzelm@55992
   415
          })
wenzelm@53275
   416
      }
wenzelm@55615
   417
wenzelm@55982
   418
    (abbrevs_result orElse words_result) match {
wenzelm@57588
   419
      case Some((original, completions)) if !completions.isEmpty =>
wenzelm@57588
   420
        val range = Text.Range(- original.length, 0) + caret + start
wenzelm@55985
   421
        val immediate =
wenzelm@55985
   422
          explicit ||
wenzelm@55985
   423
            (!Completion.Word_Parsers.is_word(original) &&
wenzelm@55985
   424
              Character.codePointCount(original, 0, original.length) > 1)
wenzelm@55993
   425
        val unique = completions.length == 1
wenzelm@55985
   426
wenzelm@55985
   427
        val items =
wenzelm@55985
   428
          for {
wenzelm@55993
   429
            (complete_word, name0) <- completions
wenzelm@55993
   430
            name1 = decode(name0)
wenzelm@55985
   431
            if name1 != original
wenzelm@55985
   432
            (s1, s2) =
wenzelm@55985
   433
              space_explode(Completion.caret_indicator, name1) match {
wenzelm@55985
   434
                case List(s1, s2) => (s1, s2)
wenzelm@55985
   435
                case _ => (name1, "")
wenzelm@55985
   436
              }
wenzelm@55985
   437
            move = - s2.length
wenzelm@55985
   438
            description =
wenzelm@55985
   439
              if (is_symbol(name0)) {
wenzelm@55985
   440
                if (name0 == name1) List(name0)
wenzelm@55985
   441
                else List(name1, "(symbol " + quote(name0) + ")")
wenzelm@55985
   442
              }
wenzelm@56001
   443
              else if (is_keyword_template(complete_word, true))
wenzelm@55993
   444
                List(name1, "(template " + quote(complete_word) + ")")
wenzelm@55993
   445
              else if (move != 0) List(name1, "(template)")
wenzelm@55993
   446
              else if (is_keyword(complete_word)) List(name1, "(keyword)")
wenzelm@55985
   447
              else List(name1)
wenzelm@55985
   448
          }
wenzelm@55985
   449
          yield Completion.Item(range, original, name1, description, s1 + s2, move, immediate)
wenzelm@55985
   450
wenzelm@55985
   451
        if (items.isEmpty) None
wenzelm@56174
   452
        else
wenzelm@56174
   453
          Some(Completion.Result(range, original, unique,
wenzelm@56174
   454
            items.sortBy(_.name).sorted(history.ordering)))
wenzelm@55985
   455
wenzelm@55992
   456
      case _ => None
wenzelm@31765
   457
    }
wenzelm@31763
   458
  }
wenzelm@31763
   459
}