# HG changeset patch
# User wenzelm
# Date 1397510645 -7200
# Node ID 58d7960058f5d98048bd2bb16dc97038934374a3
# Parent  86148ca3c4fd0710c265d6844d2f9b8b0bfebc94
tuned;

diff -r 86148ca3c4fd -r 58d7960058f5 src/Tools/jEdit/src/spell_checker.scala
--- a/src/Tools/jEdit/src/spell_checker.scala	Mon Apr 14 23:13:10 2014 +0200
+++ b/src/Tools/jEdit/src/spell_checker.scala	Mon Apr 14 23:24:05 2014 +0200
@@ -99,8 +99,6 @@
     }
   }
 
-  private sealed case class Declaration(include: Boolean, permanent: Boolean)
-
 
   /* known dictionaries */
 
@@ -141,6 +139,8 @@
   /* create spell checker */
 
   def apply(dictionary: Dictionary): Spell_Checker = new Spell_Checker(dictionary)
+
+  private sealed case class Update(include: Boolean, permanent: Boolean)
 }
 
 
@@ -149,17 +149,17 @@
   override def toString: String = dictionary.toString
 
   private var dict = new Object
-  private var declarations = SortedMap.empty[String, Spell_Checker.Declaration]
+  private var updates = SortedMap.empty[String, Spell_Checker.Update]
 
   private def included_iterator(): Iterator[String] =
     for {
-      (word, d) <- declarations.iterator
-      if d.include
+      (word, upd) <- updates.iterator
+      if upd.include
     } yield word
 
   private def excluded(word: String): Boolean =
-    declarations.get(word) match {
-      case Some(d) => !d.include
+    updates.get(word) match {
+      case Some(upd) => !upd.include
       case None => false
     }
 
@@ -167,16 +167,16 @@
   {
     val main_dictionary = split_lines(File.read_gzip(dictionary.path))
 
-    val user_declarations =
+    val permanent_updates =
       if (dictionary.user_path.is_file)
         for {
           Spell_Checker.Decl(word, include) <- split_lines(File.read(dictionary.user_path))
-        } yield (word, Spell_Checker.Declaration(include, true))
+        } yield (word, Spell_Checker.Update(include, true))
       else Nil
 
-    declarations =
-      declarations -- (for ((name, d) <- declarations.iterator; if d.permanent) yield name) ++
-        user_declarations
+    updates =
+      updates -- (for ((name, upd) <- updates.iterator; if upd.permanent) yield name) ++
+        permanent_updates
 
     val factory_class = Class.forName("com.inet.jortho.DictionaryFactory")
     val factory_cons = factory_class.getConstructor()
@@ -201,13 +201,13 @@
   {
     val permanent_decls =
       (for {
-        (word, d) <- declarations.iterator
-        if d.permanent
-      } yield Spell_Checker.Decl(word, d.include)).toList
+        (word, upd) <- updates.iterator
+        if upd.permanent
+      } yield Spell_Checker.Decl(word, upd.include)).toList
 
     if (!permanent_decls.isEmpty || dictionary.user_path.is_file) {
       val header =
-        "# User declarations for spell-checker dictionary " + quote(dictionary.lang) +
+        "# Permanent updates for spell-checker dictionary " + quote(dictionary.lang) +
 """
 #
 #   * each line contains at most one word
@@ -225,7 +225,7 @@
 
   def update(word: String, include: Boolean, permanent: Boolean)
   {
-    declarations += (word -> Spell_Checker.Declaration(include, permanent))
+    updates += (word -> Spell_Checker.Update(include, permanent))
 
     if (include) {
       if (permanent) save()
@@ -239,8 +239,7 @@
 
   def reset()
   {
-    declarations =
-      declarations -- (for ((name, d) <- declarations.iterator; if !d.permanent) yield name)
+    updates = SortedMap.empty
     load()
   }