From 33f5c536685d018fa256919f8860a206988ca15d Mon Sep 17 00:00:00 2001 From: Cristian Maglie Date: Fri, 25 May 2012 19:03:00 +0200 Subject: [PATCH] Implemented OS specific preferences --- .../app/helpers/PreferencesMap.java | 22 +++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/app/src/processing/app/helpers/PreferencesMap.java b/app/src/processing/app/helpers/PreferencesMap.java index 301f5a701..22e3523f2 100644 --- a/app/src/processing/app/helpers/PreferencesMap.java +++ b/app/src/processing/app/helpers/PreferencesMap.java @@ -29,9 +29,12 @@ import java.io.FileNotFoundException; import java.io.IOException; import java.io.InputStream; import java.util.HashMap; +import java.util.HashSet; import java.util.Hashtable; import java.util.Map; +import java.util.Set; +import processing.app.Base; import processing.core.PApplet; public class PreferencesMap extends HashMap { @@ -78,6 +81,25 @@ public class PreferencesMap extends HashMap { put(key.trim(), value.trim()); } } + + // This is needed to avoid ConcurrentAccessExceptions + Set keys = new HashSet(keySet()); + + // Override keys that have OS specific versions + for (String k : keys) { + boolean replace = false; + if (Base.isLinux() && k.endsWith(".linux")) + replace = true; + if (Base.isWindows() && k.endsWith(".windows")) + replace = true; + if (Base.isMacOS() && k.endsWith(".macos")) + replace = true; + if (replace) { + int dot = k.lastIndexOf('.'); + String overridenKey = k.substring(0, dot); + put(overridenKey, get(k)); + } + } } /**