src/Pure/General/completion.scala
author wenzelm
Wed Nov 01 21:21:09 2017 +0100 (20 months ago)
changeset 66985 7382ff5b46b9
parent 66984 a1d3e5df0c95
child 67004 af72fa58f71b
permissions -rw-r--r--
tuned;
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@66157
    34
    def merge(history: History, results: Option[Result]*): Option[Result] =
wenzelm@66157
    35
      ((None: Option[Result]) /: results)({
wenzelm@66157
    36
        case (result1, None) => result1
wenzelm@66157
    37
        case (None, result2) => result2
wenzelm@66157
    38
        case (result1 @ 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@66157
    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@65344
    73
            list(pair(string, int))(Symbol.decode_yxml(File.read(COMPLETION_HISTORY)))
wenzelm@53337
    74
          }
wenzelm@53337
    75
          catch {
wenzelm@53337
    76
            case ERROR(msg) => ignore_error(msg); Nil
wenzelm@53337
    77
            case _: XML.Error => ignore_error(""); Nil
wenzelm@53337
    78
          }
wenzelm@53337
    79
        }
wenzelm@53337
    80
        else Nil
wenzelm@53337
    81
      (empty /: content)(_ + _)
wenzelm@53337
    82
    }
wenzelm@53337
    83
  }
wenzelm@53337
    84
wenzelm@53337
    85
  final class History private(rep: SortedMap[String, Int] = SortedMap.empty)
wenzelm@53337
    86
  {
wenzelm@53337
    87
    override def toString: String = rep.mkString("Completion.History(", ",", ")")
wenzelm@53337
    88
wenzelm@56878
    89
    def frequency(name: String): Int =
wenzelm@56878
    90
      default_frequency(Symbol.encode(name)) getOrElse
wenzelm@56878
    91
      rep.getOrElse(name, 0)
wenzelm@53337
    92
wenzelm@53337
    93
    def + (entry: (String, Int)): History =
wenzelm@53337
    94
    {
wenzelm@53337
    95
      val (name, freq) = entry
wenzelm@56564
    96
      if (name == "") this
wenzelm@56564
    97
      else new History(rep + (name -> (frequency(name) + freq)))
wenzelm@53337
    98
    }
wenzelm@53337
    99
wenzelm@53337
   100
    def ordering: Ordering[Item] =
wenzelm@53337
   101
      new Ordering[Item] {
wenzelm@53337
   102
        def compare(item1: Item, item2: Item): Int =
wenzelm@56162
   103
          frequency(item2.name) compare frequency(item1.name)
wenzelm@56162
   104
      }
wenzelm@56162
   105
wenzelm@53337
   106
    def save()
wenzelm@53337
   107
    {
wenzelm@53337
   108
      Isabelle_System.mkdirs(COMPLETION_HISTORY.dir)
wenzelm@53337
   109
      File.write_backup(COMPLETION_HISTORY,
wenzelm@53337
   110
        {
wenzelm@53337
   111
          import XML.Encode._
wenzelm@65344
   112
          Symbol.encode_yxml(list(pair(string, int))(rep.toList))
wenzelm@53337
   113
        })
wenzelm@53337
   114
    }
wenzelm@53337
   115
  }
wenzelm@53337
   116
wenzelm@53337
   117
  class History_Variable
wenzelm@53337
   118
  {
wenzelm@53337
   119
    private var history = History.empty
wenzelm@53337
   120
    def value: History = synchronized { history }
wenzelm@53337
   121
wenzelm@53337
   122
    def load()
wenzelm@53337
   123
    {
wenzelm@53337
   124
      val h = History.load()
wenzelm@53337
   125
      synchronized { history = h }
wenzelm@53337
   126
    }
wenzelm@53337
   127
wenzelm@53337
   128
    def update(item: Item, freq: Int = 1): Unit = synchronized {
wenzelm@55666
   129
      history = history + (item.name -> freq)
wenzelm@53337
   130
    }
wenzelm@53337
   131
  }
wenzelm@53337
   132
wenzelm@53337
   133
wenzelm@55694
   134
wenzelm@55694
   135
  /** semantic completion **/
wenzelm@55694
   136
wenzelm@61100
   137
  def clean_name(s: String): Option[String] =
wenzelm@61100
   138
    if (s == "" || s == "_") None
wenzelm@61100
   139
    else Some(s.reverseIterator.dropWhile(_ == '_').toList.reverse.mkString)
wenzelm@61100
   140
wenzelm@66768
   141
  def completed(input: String): String => Boolean =
wenzelm@66768
   142
    clean_name(input) match {
wenzelm@66768
   143
      case None => (name: String) => false
wenzelm@66768
   144
      case Some(prefix) => (name: String) => name.startsWith(prefix)
wenzelm@66768
   145
    }
wenzelm@66768
   146
wenzelm@59717
   147
  def report_no_completion(pos: Position.T): String =
wenzelm@59717
   148
    YXML.string_of_tree(Semantic.Info(pos, No_Completion))
wenzelm@59717
   149
wenzelm@66766
   150
  def report_names(pos: Position.T, names: List[(String, (String, String))], total: Int = 0): String =
wenzelm@66768
   151
    if (names.isEmpty) ""
wenzelm@66768
   152
    else
wenzelm@66768
   153
      YXML.string_of_tree(Semantic.Info(pos, Names(if (total > 0) total else names.length, names)))
wenzelm@66766
   154
wenzelm@66766
   155
  def report_theories(pos: Position.T, thys: List[String], total: Int = 0): String =
wenzelm@66766
   156
    report_names(pos, thys.map(name => (name, ("theory", name))), total)
wenzelm@59717
   157
wenzelm@56173
   158
  object Semantic
wenzelm@55694
   159
  {
wenzelm@55694
   160
    object Info
wenzelm@55694
   161
    {
wenzelm@59717
   162
      def apply(pos: Position.T, semantic: Semantic): XML.Elem =
wenzelm@59717
   163
      {
wenzelm@59717
   164
        val elem =
wenzelm@59717
   165
          semantic match {
wenzelm@59717
   166
            case No_Completion => XML.Elem(Markup(Markup.NO_COMPLETION, pos), Nil)
wenzelm@59717
   167
            case Names(total, names) =>
wenzelm@59717
   168
              XML.Elem(Markup(Markup.COMPLETION, pos),
wenzelm@59717
   169
                {
wenzelm@59717
   170
                  import XML.Encode._
wenzelm@59717
   171
                  pair(int, list(pair(string, pair(string, string))))(total, names)
wenzelm@59717
   172
                })
wenzelm@59717
   173
          }
wenzelm@59717
   174
        XML.Elem(Markup(Markup.REPORT, pos), List(elem))
wenzelm@59717
   175
      }
wenzelm@59717
   176
wenzelm@56173
   177
      def unapply(info: Text.Markup): Option[Text.Info[Semantic]] =
wenzelm@55694
   178
        info.info match {
wenzelm@55694
   179
          case XML.Elem(Markup(Markup.COMPLETION, _), body) =>
wenzelm@55694
   180
            try {
wenzelm@55694
   181
              val (total, names) =
wenzelm@55694
   182
              {
wenzelm@55694
   183
                import XML.Decode._
wenzelm@55977
   184
                pair(int, list(pair(string, pair(string, string))))(body)
wenzelm@55694
   185
              }
wenzelm@56173
   186
              Some(Text.Info(info.range, Names(total, names)))
wenzelm@55694
   187
            }
wenzelm@55694
   188
            catch { case _: XML.Error => None }
wenzelm@55914
   189
          case XML.Elem(Markup(Markup.NO_COMPLETION, _), _) =>
wenzelm@56173
   190
            Some(Text.Info(info.range, No_Completion))
wenzelm@55694
   191
          case _ => None
wenzelm@55694
   192
        }
wenzelm@55694
   193
    }
wenzelm@55694
   194
  }
wenzelm@55694
   195
wenzelm@56173
   196
  sealed abstract class Semantic
wenzelm@56175
   197
  case object No_Completion extends Semantic
wenzelm@56175
   198
  case class Names(total: Int, names: List[(String, (String, String))]) extends Semantic
wenzelm@55694
   199
  {
wenzelm@55694
   200
    def complete(
wenzelm@56173
   201
      range: Text.Range,
wenzelm@56173
   202
      history: Completion.History,
wenzelm@66055
   203
      unicode: Boolean,
wenzelm@55694
   204
      original: String): Option[Completion.Result] =
wenzelm@55694
   205
    {
wenzelm@66055
   206
      def decode(s: String): String = if (unicode) Symbol.decode(s) else s
wenzelm@55694
   207
      val items =
wenzelm@55694
   208
        for {
wenzelm@55977
   209
          (xname, (kind, name)) <- names
wenzelm@55977
   210
          xname1 = decode(xname)
wenzelm@55694
   211
          if xname1 != original
wenzelm@55977
   212
          (full_name, descr_name) =
wenzelm@55977
   213
            if (kind == "") (name, quote(decode(name)))
wenzelm@56600
   214
            else
wenzelm@56800
   215
             (Long_Name.qualify(kind, name),
wenzelm@60732
   216
              Word.implode(Word.explode('_', kind)) +
wenzelm@60732
   217
              (if (xname == name) "" else " " + quote(decode(name))))
wenzelm@61622
   218
        } yield {
wenzelm@61622
   219
          val description = List(xname1, "(" + descr_name + ")")
wenzelm@61622
   220
          val replacement =
wenzelm@63761
   221
            List(original, xname1).map(Token.explode(Keyword.Keywords.empty, _)) match {
wenzelm@63761
   222
              case List(List(tok), _) if tok.kind == Token.Kind.CARTOUCHE =>
wenzelm@63761
   223
                Symbol.open_decoded + xname1 + Symbol.close_decoded
wenzelm@63761
   224
              case List(_, List(tok)) if tok.is_name => xname1
wenzelm@61622
   225
              case _ => quote(xname1)
wenzelm@61622
   226
            }
wenzelm@61622
   227
          Item(range, original, full_name, description, replacement, 0, true)
wenzelm@61622
   228
        }
wenzelm@55694
   229
wenzelm@55694
   230
      if (items.isEmpty) None
wenzelm@55694
   231
      else Some(Result(range, original, names.length == 1, items.sorted(history.ordering)))
wenzelm@55694
   232
    }
wenzelm@55694
   233
  }
wenzelm@55694
   234
wenzelm@55694
   235
wenzelm@55694
   236
wenzelm@55694
   237
  /** syntactic completion **/
wenzelm@55694
   238
wenzelm@55694
   239
  /* language context */
wenzelm@55694
   240
wenzelm@55749
   241
  object Language_Context
wenzelm@55694
   242
  {
wenzelm@55749
   243
    val outer = Language_Context("", true, false)
wenzelm@55749
   244
    val inner = Language_Context(Markup.Language.UNKNOWN, true, false)
wenzelm@55749
   245
    val ML_outer = Language_Context(Markup.Language.ML, false, true)
wenzelm@55749
   246
    val ML_inner = Language_Context(Markup.Language.ML, true, false)
wenzelm@56278
   247
    val SML_outer = Language_Context(Markup.Language.SML, false, false)
wenzelm@55694
   248
  }
wenzelm@55694
   249
wenzelm@55749
   250
  sealed case class Language_Context(language: String, symbols: Boolean, antiquotes: Boolean)
wenzelm@55694
   251
  {
wenzelm@55694
   252
    def is_outer: Boolean = language == ""
wenzelm@55694
   253
  }
wenzelm@55694
   254
wenzelm@55694
   255
wenzelm@55694
   256
  /* init */
wenzelm@55694
   257
wenzelm@55694
   258
  val empty: Completion = new Completion()
wenzelm@66984
   259
wenzelm@66984
   260
  lazy val init: Completion =
wenzelm@63871
   261
    empty.add_symbols.add_abbrevs(Completion.symbol_abbrevs ::: Completion.default_abbrevs)
wenzelm@55694
   262
wenzelm@55694
   263
wenzelm@55694
   264
  /* word parsers */
wenzelm@31763
   265
wenzelm@63587
   266
  object Word_Parsers extends RegexParsers
wenzelm@31763
   267
  {
wenzelm@31763
   268
    override val whiteSpace = "".r
wenzelm@31763
   269
wenzelm@61613
   270
    private val symboloid_regex: Regex = """\\([A-Za-z0-9_']+|<\^?[A-Za-z0-9_']+>?)""".r
wenzelm@61600
   271
    def is_symboloid(s: CharSequence): Boolean = symboloid_regex.pattern.matcher(s).matches
wenzelm@57589
   272
wenzelm@55615
   273
    private def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r
wenzelm@55615
   274
    private def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r
wenzelm@61599
   275
    private def reverse_escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r
wenzelm@55615
   276
wenzelm@56039
   277
    private val word_regex = "[a-zA-Z0-9_'.]+".r
wenzelm@63887
   278
    private def word2: Parser[String] = "[a-zA-Z0-9_'.]{2,}".r
wenzelm@55996
   279
    private def underscores: Parser[String] = "_*".r
wenzelm@55615
   280
wenzelm@55813
   281
    def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
wenzelm@56042
   282
    def is_word_char(c: Char): Boolean = Symbol.is_ascii_letdig(c) || c == '.'
wenzelm@31763
   283
wenzelm@55813
   284
    def read_symbol(in: CharSequence): Option[String] =
wenzelm@55813
   285
    {
wenzelm@55813
   286
      val reverse_in = new Library.Reverse(in)
wenzelm@55813
   287
      parse(reverse_symbol ^^ (_.reverse), reverse_in) match {
wenzelm@55813
   288
        case Success(result, _) => Some(result)
wenzelm@55813
   289
        case _ => None
wenzelm@55813
   290
      }
wenzelm@55813
   291
    }
wenzelm@55813
   292
wenzelm@63887
   293
    def read_word(in: CharSequence): Option[(String, String)] =
wenzelm@31763
   294
    {
wenzelm@37072
   295
      val reverse_in = new Library.Reverse(in)
wenzelm@55996
   296
      val parser =
wenzelm@61599
   297
        (reverse_symbol | reverse_symb | reverse_escape) ^^ (x => (x.reverse, "")) |
wenzelm@63887
   298
        underscores ~ word2 ~ opt("?") ^^
wenzelm@56221
   299
        { case x ~ y ~ z => (z.getOrElse("") + y.reverse, x) }
wenzelm@55996
   300
      parse(parser, reverse_in) match {
wenzelm@31763
   301
        case Success(result, _) => Some(result)
wenzelm@31763
   302
        case _ => None
wenzelm@31763
   303
      }
wenzelm@31763
   304
    }
wenzelm@31763
   305
  }
wenzelm@55666
   306
wenzelm@55666
   307
wenzelm@63871
   308
  /* templates */
wenzelm@61960
   309
wenzelm@63869
   310
  val caret_indicator = '\u0007'
wenzelm@63871
   311
wenzelm@63869
   312
  def split_template(s: String): (String, String) =
wenzelm@63869
   313
    space_explode(caret_indicator, s) match {
wenzelm@63869
   314
      case List(s1, s2) => (s1, s2)
wenzelm@63869
   315
      case _ => (s, "")
wenzelm@63869
   316
    }
wenzelm@63869
   317
wenzelm@63871
   318
wenzelm@63871
   319
  /* abbreviations */
wenzelm@63871
   320
wenzelm@63871
   321
  private def symbol_abbrevs: Thy_Header.Abbrevs =
wenzelm@63871
   322
    for ((sym, abbr) <- Symbol.abbrevs.toList) yield (abbr, sym)
wenzelm@63871
   323
wenzelm@55666
   324
  private val antiquote = "@{"
wenzelm@56878
   325
wenzelm@63578
   326
  private val default_abbrevs =
wenzelm@56878
   327
    List("@{" -> "@{\u0007}",
wenzelm@56878
   328
      "`" -> "\\<close>",
wenzelm@56878
   329
      "`" -> "\\<open>",
wenzelm@63135
   330
      "`" -> "\\<open>\u0007\\<close>",
wenzelm@63135
   331
      "\"" -> "\\<close>",
wenzelm@63135
   332
      "\"" -> "\\<open>",
wenzelm@63135
   333
      "\"" -> "\\<open>\u0007\\<close>")
wenzelm@56878
   334
wenzelm@56878
   335
  private def default_frequency(name: String): Option[Int] =
wenzelm@63578
   336
    default_abbrevs.iterator.map(_._2).zipWithIndex.find(_._1 == name).map(_._2)
wenzelm@31763
   337
}
wenzelm@31763
   338
wenzelm@46712
   339
final class Completion private(
wenzelm@63579
   340
  protected val keywords: Set[String] = Set.empty,
wenzelm@59073
   341
  protected val words_lex: Scan.Lexicon = Scan.Lexicon.empty,
wenzelm@59073
   342
  protected val words_map: Multi_Map[String, String] = Multi_Map.empty,
wenzelm@59073
   343
  protected val abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty,
wenzelm@59073
   344
  protected val abbrevs_map: Multi_Map[String, (String, String)] = Multi_Map.empty)
wenzelm@31763
   345
{
wenzelm@59073
   346
  /* merge */
wenzelm@59073
   347
wenzelm@59073
   348
  def is_empty: Boolean =
wenzelm@59073
   349
    keywords.isEmpty &&
wenzelm@59073
   350
    words_lex.is_empty &&
wenzelm@59073
   351
    words_map.isEmpty &&
wenzelm@59073
   352
    abbrevs_lex.is_empty &&
wenzelm@59073
   353
    abbrevs_map.isEmpty
wenzelm@59073
   354
wenzelm@59073
   355
  def ++ (other: Completion): Completion =
wenzelm@59073
   356
    if (this eq other) this
wenzelm@59073
   357
    else if (is_empty) other
wenzelm@59073
   358
    else {
wenzelm@66985
   359
      val keywords1 =
wenzelm@66985
   360
        if (keywords eq other.keywords) keywords
wenzelm@66985
   361
        else if (keywords.isEmpty) other.keywords
wenzelm@66985
   362
        else (keywords /: other.keywords) { case (ks, k) => if (ks(k)) ks else ks + k }
wenzelm@59073
   363
      val words_lex1 = words_lex ++ other.words_lex
wenzelm@59073
   364
      val words_map1 = words_map ++ other.words_map
wenzelm@59073
   365
      val abbrevs_lex1 = abbrevs_lex ++ other.abbrevs_lex
wenzelm@59073
   366
      val abbrevs_map1 = abbrevs_map ++ other.abbrevs_map
wenzelm@66985
   367
      if ((keywords eq keywords1) && (words_lex eq words_lex1) && (words_map eq words_map1) &&
wenzelm@66985
   368
        (abbrevs_lex eq abbrevs_lex1) && (abbrevs_map eq abbrevs_map1)) this
wenzelm@66985
   369
      else new Completion(keywords1, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1)
wenzelm@59073
   370
    }
wenzelm@59073
   371
wenzelm@59073
   372
wenzelm@55983
   373
  /* keywords */
wenzelm@31763
   374
wenzelm@55986
   375
  private def is_symbol(name: String): Boolean = Symbol.names.isDefinedAt(name)
wenzelm@63579
   376
  private def is_keyword(name: String): Boolean = !is_symbol(name) && keywords(name)
wenzelm@56001
   377
  private def is_keyword_template(name: String, template: Boolean): Boolean =
wenzelm@63579
   378
    is_keyword(name) && (words_map.getOrElse(name, name) != name) == template
wenzelm@55984
   379
wenzelm@63579
   380
  def add_keyword(keyword: String): Completion =
wenzelm@63579
   381
    new Completion(keywords + keyword, words_lex, words_map, abbrevs_lex, abbrevs_map)
wenzelm@40533
   382
wenzelm@55983
   383
wenzelm@63578
   384
  /* symbols and abbrevs */
wenzelm@55983
   385
wenzelm@63871
   386
  def add_symbols: Completion =
wenzelm@31763
   387
  {
wenzelm@31763
   388
    val words =
wenzelm@61599
   389
      (for ((sym, _) <- Symbol.names.toList) yield (sym, sym)) :::
wenzelm@63578
   390
      (for ((sym, name) <- Symbol.names.toList) yield ("\\" + name, sym))
wenzelm@31763
   391
wenzelm@63578
   392
    new Completion(
wenzelm@63578
   393
      keywords,
wenzelm@63578
   394
      words_lex ++ words.map(_._1),
wenzelm@63578
   395
      words_map ++ words,
wenzelm@63578
   396
      abbrevs_lex,
wenzelm@63578
   397
      abbrevs_map)
wenzelm@63578
   398
  }
wenzelm@55666
   399
wenzelm@63578
   400
  def add_abbrevs(abbrevs: List[(String, String)]): Completion =
wenzelm@63808
   401
    (this /: abbrevs)(_.add_abbrev(_))
wenzelm@63808
   402
wenzelm@63808
   403
  private def add_abbrev(abbrev: (String, String)): Completion =
wenzelm@63873
   404
    abbrev match {
wenzelm@63873
   405
      case ("", _) => this
wenzelm@63873
   406
      case (abbr, text) =>
wenzelm@63873
   407
        val rev_abbr = abbr.reverse
wenzelm@63873
   408
        val is_word = Completion.Word_Parsers.is_word(abbr)
wenzelm@31763
   409
wenzelm@63873
   410
        val (words_lex1, words_map1) =
wenzelm@63873
   411
          if (!is_word) (words_lex, words_map)
wenzelm@63873
   412
          else if (text != "") (words_lex + abbr, words_map + abbrev)
wenzelm@63873
   413
          else (words_lex -- List(abbr), words_map - abbr)
wenzelm@63808
   414
wenzelm@63873
   415
        val (abbrevs_lex1, abbrevs_map1) =
wenzelm@63873
   416
          if (is_word) (abbrevs_lex, abbrevs_map)
wenzelm@63873
   417
          else if (text != "") (abbrevs_lex + rev_abbr, abbrevs_map + (rev_abbr -> abbrev))
wenzelm@63873
   418
          else (abbrevs_lex -- List(rev_abbr), abbrevs_map - rev_abbr)
wenzelm@63808
   419
wenzelm@63873
   420
        new Completion(keywords, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1)
wenzelm@63873
   421
    }
wenzelm@31763
   422
wenzelm@31763
   423
wenzelm@31763
   424
  /* complete */
wenzelm@31763
   425
wenzelm@53337
   426
  def complete(
wenzelm@53337
   427
    history: Completion.History,
wenzelm@66055
   428
    unicode: Boolean,
wenzelm@53337
   429
    explicit: Boolean,
wenzelm@55813
   430
    start: Text.Offset,
wenzelm@55615
   431
    text: CharSequence,
wenzelm@55813
   432
    caret: Int,
wenzelm@55749
   433
    language_context: Completion.Language_Context): Option[Completion.Result] =
wenzelm@31763
   434
  {
wenzelm@55813
   435
    val length = text.length
wenzelm@55813
   436
wenzelm@55615
   437
    val abbrevs_result =
wenzelm@55813
   438
    {
wenzelm@55813
   439
      val reverse_in = new Library.Reverse(text.subSequence(0, caret))
wenzelm@55813
   440
      Scan.Parsers.parse(Scan.Parsers.literal(abbrevs_lex), reverse_in) match {
wenzelm@61599
   441
        case Scan.Parsers.Success(reverse_abbr, _) =>
wenzelm@61599
   442
          val abbrevs = abbrevs_map.get_list(reverse_abbr)
wenzelm@55666
   443
          abbrevs match {
wenzelm@55666
   444
            case Nil => None
wenzelm@61599
   445
            case (abbr, _) :: _ =>
wenzelm@55666
   446
              val ok =
wenzelm@61599
   447
                if (abbr == Completion.antiquote) language_context.antiquotes
wenzelm@63578
   448
                else language_context.symbols || Completion.default_abbrevs.exists(_._1 == abbr)
wenzelm@61599
   449
              if (ok) Some((abbr, abbrevs))
wenzelm@55813
   450
              else None
wenzelm@55666
   451
          }
wenzelm@55666
   452
        case _ => None
wenzelm@55666
   453
      }
wenzelm@55813
   454
    }
wenzelm@55615
   455
wenzelm@55615
   456
    val words_result =
wenzelm@55982
   457
      if (abbrevs_result.isDefined) None
wenzelm@55982
   458
      else {
wenzelm@57602
   459
        val word_context =
wenzelm@57602
   460
          caret < length && Completion.Word_Parsers.is_word_char(text.charAt(caret))
wenzelm@55996
   461
        val result =
wenzelm@57588
   462
          Completion.Word_Parsers.read_symbol(text.subSequence(0, caret)) match {
wenzelm@55996
   463
            case Some(symbol) => Some((symbol, ""))
wenzelm@63887
   464
            case None => Completion.Word_Parsers.read_word(text.subSequence(0, caret))
wenzelm@55992
   465
          }
wenzelm@55996
   466
        result.map(
wenzelm@55992
   467
          {
wenzelm@55996
   468
            case (word, underscores) =>
wenzelm@55996
   469
              val complete_words = words_lex.completions(word)
wenzelm@55996
   470
              val full_word = word + underscores
wenzelm@55996
   471
              val completions =
wenzelm@56001
   472
                if (complete_words.contains(full_word) && is_keyword_template(full_word, false)) Nil
wenzelm@55996
   473
                else
wenzelm@55996
   474
                  for {
wenzelm@55996
   475
                    complete_word <- complete_words
wenzelm@55996
   476
                    ok =
wenzelm@57602
   477
                      if (is_keyword(complete_word)) !word_context && language_context.is_outer
wenzelm@61600
   478
                      else language_context.symbols || Completion.Word_Parsers.is_symboloid(word)
wenzelm@55996
   479
                    if ok
wenzelm@55996
   480
                    completion <- words_map.get_list(complete_word)
wenzelm@55996
   481
                  } yield (complete_word, completion)
wenzelm@60215
   482
              (full_word, completions)
wenzelm@55992
   483
          })
wenzelm@53275
   484
      }
wenzelm@55615
   485
wenzelm@55982
   486
    (abbrevs_result orElse words_result) match {
wenzelm@59319
   487
      case Some((original, completions)) if completions.nonEmpty =>
wenzelm@57588
   488
        val range = Text.Range(- original.length, 0) + caret + start
wenzelm@55985
   489
        val immediate =
wenzelm@55985
   490
          explicit ||
wenzelm@55985
   491
            (!Completion.Word_Parsers.is_word(original) &&
wenzelm@61600
   492
             !Completion.Word_Parsers.is_symboloid(original) &&
wenzelm@55985
   493
              Character.codePointCount(original, 0, original.length) > 1)
wenzelm@55993
   494
        val unique = completions.length == 1
wenzelm@55985
   495
wenzelm@66056
   496
        def decode1(s: String): String = if (unicode) Symbol.decode(s) else s
wenzelm@66056
   497
        def decode2(s: String): String = if (unicode) s else Symbol.decode(s)
wenzelm@66056
   498
wenzelm@55985
   499
        val items =
wenzelm@55985
   500
          for {
wenzelm@55993
   501
            (complete_word, name0) <- completions
wenzelm@66056
   502
            name1 = decode1(name0)
wenzelm@66056
   503
            name2 = decode2(name0)
wenzelm@55985
   504
            if name1 != original
wenzelm@63869
   505
            (s1, s2) = Completion.split_template(name1)
wenzelm@55985
   506
            move = - s2.length
wenzelm@55985
   507
            description =
wenzelm@55985
   508
              if (is_symbol(name0)) {
wenzelm@66056
   509
                if (name1 == name2) List(name1)
wenzelm@66056
   510
                else List(name1, "(symbol " + quote(name2) + ")")
wenzelm@55985
   511
              }
wenzelm@56001
   512
              else if (is_keyword_template(complete_word, true))
wenzelm@55993
   513
                List(name1, "(template " + quote(complete_word) + ")")
wenzelm@55993
   514
              else if (move != 0) List(name1, "(template)")
wenzelm@55993
   515
              else if (is_keyword(complete_word)) List(name1, "(keyword)")
wenzelm@55985
   516
              else List(name1)
wenzelm@55985
   517
          }
wenzelm@55985
   518
          yield Completion.Item(range, original, name1, description, s1 + s2, move, immediate)
wenzelm@55985
   519
wenzelm@55985
   520
        if (items.isEmpty) None
wenzelm@56174
   521
        else
wenzelm@56174
   522
          Some(Completion.Result(range, original, unique,
wenzelm@56174
   523
            items.sortBy(_.name).sorted(history.ordering)))
wenzelm@55985
   524
wenzelm@55992
   525
      case _ => None
wenzelm@31765
   526
    }
wenzelm@31763
   527
  }
wenzelm@31763
   528
}