342 private def default_frequency(name: String): Option[Int] = |
342 private def default_frequency(name: String): Option[Int] = |
343 default_abbrevs.iterator.map(_._2).zipWithIndex.find(_._1 == name).map(_._2) |
343 default_abbrevs.iterator.map(_._2).zipWithIndex.find(_._1 == name).map(_._2) |
344 } |
344 } |
345 |
345 |
346 final class Completion private( |
346 final class Completion private( |
347 protected val keywords: Map[String, Boolean] = Map.empty, |
347 protected val keywords: Set[String] = Set.empty, |
348 protected val words_lex: Scan.Lexicon = Scan.Lexicon.empty, |
348 protected val words_lex: Scan.Lexicon = Scan.Lexicon.empty, |
349 protected val words_map: Multi_Map[String, String] = Multi_Map.empty, |
349 protected val words_map: Multi_Map[String, String] = Multi_Map.empty, |
350 protected val abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty, |
350 protected val abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty, |
351 protected val abbrevs_map: Multi_Map[String, (String, String)] = Multi_Map.empty) |
351 protected val abbrevs_map: Multi_Map[String, (String, String)] = Multi_Map.empty) |
352 { |
352 { |
361 |
361 |
362 def ++ (other: Completion): Completion = |
362 def ++ (other: Completion): Completion = |
363 if (this eq other) this |
363 if (this eq other) this |
364 else if (is_empty) other |
364 else if (is_empty) other |
365 else { |
365 else { |
366 val keywords1 = |
366 val keywords1 = (keywords /: other.keywords) { case (ks, k) => if (ks(k)) ks else ks + k } |
367 (keywords /: other.keywords) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e } |
|
368 val words_lex1 = words_lex ++ other.words_lex |
367 val words_lex1 = words_lex ++ other.words_lex |
369 val words_map1 = words_map ++ other.words_map |
368 val words_map1 = words_map ++ other.words_map |
370 val abbrevs_lex1 = abbrevs_lex ++ other.abbrevs_lex |
369 val abbrevs_lex1 = abbrevs_lex ++ other.abbrevs_lex |
371 val abbrevs_map1 = abbrevs_map ++ other.abbrevs_map |
370 val abbrevs_map1 = abbrevs_map ++ other.abbrevs_map |
372 new Completion(keywords1, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1) |
371 new Completion(keywords1, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1) |
374 |
373 |
375 |
374 |
376 /* keywords */ |
375 /* keywords */ |
377 |
376 |
378 private def is_symbol(name: String): Boolean = Symbol.names.isDefinedAt(name) |
377 private def is_symbol(name: String): Boolean = Symbol.names.isDefinedAt(name) |
379 private def is_keyword(name: String): Boolean = !is_symbol(name) && keywords.isDefinedAt(name) |
378 private def is_keyword(name: String): Boolean = !is_symbol(name) && keywords(name) |
380 private def is_keyword_template(name: String, template: Boolean): Boolean = |
379 private def is_keyword_template(name: String, template: Boolean): Boolean = |
381 is_keyword(name) && keywords(name) == template |
380 is_keyword(name) && (words_map.getOrElse(name, name) != name) == template |
382 |
381 |
383 def + (keyword: String, template: String): Completion = |
382 def add_keyword(keyword: String): Completion = |
384 new Completion( |
383 new Completion(keywords + keyword, words_lex, words_map, abbrevs_lex, abbrevs_map) |
385 keywords + (keyword -> (keyword != template)), |
|
386 words_lex + keyword, |
|
387 words_map + (keyword -> template), |
|
388 abbrevs_lex, |
|
389 abbrevs_map) |
|
390 |
|
391 def + (keyword: String): Completion = this + (keyword, keyword) |
|
392 |
384 |
393 |
385 |
394 /* symbols and abbrevs */ |
386 /* symbols and abbrevs */ |
395 |
387 |
396 def add_symbols(): Completion = |
388 def add_symbols(): Completion = |
406 abbrevs_lex, |
398 abbrevs_lex, |
407 abbrevs_map) |
399 abbrevs_map) |
408 } |
400 } |
409 |
401 |
410 def add_abbrevs(abbrevs: List[(String, String)]): Completion = |
402 def add_abbrevs(abbrevs: List[(String, String)]): Completion = |
411 { |
403 if (abbrevs.isEmpty) this |
412 val words = |
404 else { |
413 for ((abbr, text) <- abbrevs if Completion.Word_Parsers.is_word(abbr)) |
405 val words = |
414 yield (abbr, text) |
406 for ((abbr, text) <- abbrevs if text != "" && Completion.Word_Parsers.is_word(abbr)) |
415 val abbrs = |
407 yield (abbr, text) |
416 for ((abbr, text) <- abbrevs if !Completion.Word_Parsers.is_word(abbr)) |
408 val abbrs = |
417 yield (abbr.reverse, (abbr, text)) |
409 for ((abbr, text) <- abbrevs if text != "" && !Completion.Word_Parsers.is_word(abbr)) |
418 |
410 yield (abbr.reverse, (abbr, text)) |
419 new Completion( |
411 val remove = (for ((abbr, "") <- abbrevs.iterator) yield abbr).toSet |
420 keywords, |
412 |
421 words_lex ++ words.map(_._1), |
413 new Completion( |
422 words_map ++ words, |
414 keywords, |
423 abbrevs_lex ++ abbrs.map(_._1), |
415 words_lex ++ words.map(_._1) -- remove, |
424 abbrevs_map ++ abbrs) |
416 words_map ++ words -- remove, |
425 } |
417 abbrevs_lex ++ abbrs.map(_._1) -- remove, |
|
418 abbrevs_map ++ abbrs -- remove) |
|
419 } |
426 |
420 |
427 private def load(): Completion = |
421 private def load(): Completion = |
428 add_symbols().add_abbrevs(Completion.load_abbrevs() ::: Completion.default_abbrevs) |
422 add_symbols().add_abbrevs(Completion.load_abbrevs() ::: Completion.default_abbrevs) |
429 |
423 |
430 |
424 |