equal
deleted
inserted
replaced
60 } |
60 } |
61 } |
61 } |
62 |
62 |
63 def + (keyword: String): Completion = this + (keyword, keyword) |
63 def + (keyword: String): Completion = this + (keyword, keyword) |
64 |
64 |
65 def + (symbols: Symbol.Interpretation): Completion = |
65 def add_symbols: Completion = |
66 { |
66 { |
67 val words = |
67 val words = |
68 (for ((x, _) <- symbols.names) yield (x, x)).toList ::: |
68 (for ((x, _) <- Symbol.names) yield (x, x)).toList ::: |
69 (for ((x, y) <- symbols.names) yield (y, x)).toList ::: |
69 (for ((x, y) <- Symbol.names) yield (y, x)).toList ::: |
70 (for ((x, y) <- symbols.abbrevs if Completion.is_word(y)) yield (y, x)).toList |
70 (for ((x, y) <- Symbol.abbrevs if Completion.is_word(y)) yield (y, x)).toList |
71 |
71 |
72 val abbrs = |
72 val abbrs = |
73 (for ((x, y) <- symbols.abbrevs if !Completion.is_word(y)) |
73 (for ((x, y) <- Symbol.abbrevs if !Completion.is_word(y)) |
74 yield (y.reverse.toString, (y, x))).toList |
74 yield (y.reverse.toString, (y, x))).toList |
75 |
75 |
76 val old = this |
76 val old = this |
77 new Completion { |
77 new Completion { |
78 override val words_lex = old.words_lex ++ words.map(_._1) |
78 override val words_lex = old.words_lex ++ words.map(_._1) |