equal
deleted
inserted
replaced
204 (word, upd) <- updates.iterator |
204 (word, upd) <- updates.iterator |
205 if upd.permanent |
205 if upd.permanent |
206 } yield Spell_Checker.Decl(word, upd.include)).toList |
206 } yield Spell_Checker.Decl(word, upd.include)).toList |
207 |
207 |
208 if (!permanent_decls.isEmpty || dictionary.user_path.is_file) { |
208 if (!permanent_decls.isEmpty || dictionary.user_path.is_file) { |
209 val header = |
209 val header = """# User updates for spell-checker dictionary |
210 "# Permanent updates for spell-checker dictionary " + quote(dictionary.lang) + |
|
211 """ |
|
212 # |
210 # |
213 # * each line contains at most one word |
211 # * each line contains at most one word |
214 # * extra blanks are ignored |
212 # * extra blanks are ignored |
215 # * lines starting with "#" are stripped |
213 # * lines starting with "#" are stripped |
216 # * lines starting with "-" indicate excluded words |
214 # * lines starting with "-" indicate excluded words |