385 |
385 |
386 def add_abbrevs(abbrevs: List[(String, String)]): Completion = |
386 def add_abbrevs(abbrevs: List[(String, String)]): Completion = |
387 (this /: abbrevs)(_.add_abbrev(_)) |
387 (this /: abbrevs)(_.add_abbrev(_)) |
388 |
388 |
389 private def add_abbrev(abbrev: (String, String)): Completion = |
389 private def add_abbrev(abbrev: (String, String)): Completion = |
390 { |
390 abbrev match { |
391 val (abbr, text) = abbrev |
391 case ("", _) => this |
392 val rev_abbr = abbr.reverse |
392 case (abbr, text) => |
393 val is_word = Completion.Word_Parsers.is_word(abbr) |
393 val rev_abbr = abbr.reverse |
394 |
394 val is_word = Completion.Word_Parsers.is_word(abbr) |
395 val (words_lex1, words_map1) = |
395 |
396 if (!is_word) (words_lex, words_map) |
396 val (words_lex1, words_map1) = |
397 else if (text != "") (words_lex + abbr, words_map + abbrev) |
397 if (!is_word) (words_lex, words_map) |
398 else (words_lex -- List(abbr), words_map - abbr) |
398 else if (text != "") (words_lex + abbr, words_map + abbrev) |
399 |
399 else (words_lex -- List(abbr), words_map - abbr) |
400 val (abbrevs_lex1, abbrevs_map1) = |
400 |
401 if (is_word) (abbrevs_lex, abbrevs_map) |
401 val (abbrevs_lex1, abbrevs_map1) = |
402 else if (text != "") (abbrevs_lex + rev_abbr, abbrevs_map + (rev_abbr -> abbrev)) |
402 if (is_word) (abbrevs_lex, abbrevs_map) |
403 else (abbrevs_lex -- List(rev_abbr), abbrevs_map - rev_abbr) |
403 else if (text != "") (abbrevs_lex + rev_abbr, abbrevs_map + (rev_abbr -> abbrev)) |
404 |
404 else (abbrevs_lex -- List(rev_abbr), abbrevs_map - rev_abbr) |
405 new Completion(keywords, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1) |
405 |
406 } |
406 new Completion(keywords, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1) |
|
407 } |
407 |
408 |
408 |
409 |
409 /* complete */ |
410 /* complete */ |
410 |
411 |
411 def complete( |
412 def complete( |