equal
deleted
inserted
replaced
38 } |
38 } |
39 } |
39 } |
40 } |
40 } |
41 } |
41 } |
42 |
42 |
43 class Completion private( |
43 final class Completion private( |
44 words_lex: Scan.Lexicon = Scan.Lexicon.empty, |
44 words_lex: Scan.Lexicon = Scan.Lexicon.empty, |
45 words_map: Map[String, String] = Map.empty, |
45 words_map: Map[String, String] = Map.empty, |
46 abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty, |
46 abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty, |
47 abbrevs_map: Map[String, (String, String)] = Map.empty) |
47 abbrevs_map: Map[String, (String, String)] = Map.empty) |
48 { |
48 { |