add change listeners to utils.Preferences

set()/unset() notify registered listeners when a value actually
changes; loading stays silent. per the #1104 todo list.

Author: diyaayay

app/utils/src/main/java/processing/utils/Preferences.java

@@ -33,7 +33,10 @@
 import java.nio.charset.StandardCharsets;
 import java.util.Arrays;
 import java.util.HashMap;
+import java.util.List;
 import java.util.Map;
+import java.util.Objects;
+import java.util.concurrent.CopyOnWriteArrayList;
 
 
 /**
@@ -76,6 +79,45 @@ public class Preferences {
   static File preferencesFile;
   static private boolean initialized = false;
 
+  static private final List<ChangeListener> listeners =
+    new CopyOnWriteArrayList<>();
+
+
+  /**
+   * Callback for preference changes made through set() or unset().
+   * Loading (init or otherwise) does not fire events: listeners are for
+   * reacting to changes, not for observing startup.
+   */
+  public interface ChangeListener {
+    /**
+     * @param key the preference that changed
+     * @param value the new value, or null if the key was removed
+     */
+    void preferenceChanged(String key, String value);
+  }
+
+
+  static public void addChangeListener(ChangeListener listener) {
+    listeners.add(listener);
+  }
+
+
+  static public void removeChangeListener(ChangeListener listener) {
+    listeners.remove(listener);
+  }
+
+
+  static private void fireChange(String key, String value) {
+    for (ChangeListener listener : listeners) {
+      try {
+        listener.preferenceChanged(key, value);
+      } catch (Exception e) {
+        // one broken listener shouldn't prevent the change (or the others)
+        e.printStackTrace();
+      }
+    }
+  }
+
 
   /**
    * Load the bundled defaults followed by the user's preferences.txt from
@@ -323,12 +365,17 @@ static public String getDefault(String attribute) {
 
 
   static public void set(String attribute, String value) {
-    table.put(attribute, value);
+    String previous = table.put(attribute, value);
+    if (!Objects.equals(previous, value)) {
+      fireChange(attribute, value);
+    }
   }
 
 
   static public void unset(String attribute) {
-    table.remove(attribute);
+    if (table.remove(attribute) != null) {
+      fireChange(attribute, null);
+    }
   }