src/Tools/jEdit/src/spell_checker.scala
changeset 56584 9ccbac38bcad
parent 56583 c49607db182a
child 56585 a0e844c6e1ed
equal deleted inserted replaced
56583:c49607db182a 56584:9ccbac38bcad
   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