001: /*
002: * Preferences.java
003: *
004: * Copyright (C) 1998-2003 Peter Graves
005: * $Id: Preferences.java,v 1.5 2003/07/03 01:56:40 piso Exp $
006: *
007: * This program is free software; you can redistribute it and/or
008: * modify it under the terms of the GNU General Public License
009: * as published by the Free Software Foundation; either version 2
010: * of the License, or (at your option) any later version.
011: *
012: * This program is distributed in the hope that it will be useful,
013: * but WITHOUT ANY WARRANTY; without even the implied warranty of
014: * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
015: * GNU General Public License for more details.
016: *
017: * You should have received a copy of the GNU General Public License
018: * along with this program; if not, write to the Free Software
019: * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
020: */
021:
022: package org.armedbear.j;
023:
024: import java.awt.Color;
025: import java.io.IOException;
026: import java.io.InputStream;
027: import java.util.ArrayList;
028: import java.util.Enumeration;
029: import java.util.Iterator;
030: import java.util.Properties;
031:
032: public final class Preferences {
033: private Properties properties = new Properties();
034: private ArrayList listeners;
035:
036: public static final File getPreferencesFile() {
037: return File.getInstance(Directories.getEditorDirectory(),
038: "prefs");
039: }
040:
041: public synchronized void reload() {
042: reloadInternal();
043: firePreferencesChanged();
044: }
045:
046: private void reloadInternal() {
047: File file = getPreferencesFile();
048: if (file == null || !file.isFile()) {
049: // No preferences file.
050: properties = new Properties();
051: return;
052: }
053:
054: // Load preferences file into a temporary Properties object so we can
055: // see if the user has specified a theme.
056: Properties temp = new Properties();
057: try {
058: InputStream in = file.getInputStream();
059: temp.load(in);
060: in.close();
061: } catch (IOException e) {
062: Log.error(e);
063: }
064: // Convert keys to lower case.
065: temp = canonicalize(temp);
066:
067: String themeName = temp.getProperty(Property.THEME.key());
068: if (themeName == null || themeName.length() == 0) {
069: // No theme specified.
070: properties = temp;
071: return;
072: }
073:
074: String themePath = temp.getProperty(Property.THEME_PATH.key());
075:
076: // User has specified a theme. Load theme into a new Properties object.
077: properties = loadTheme(themeName, themePath);
078:
079: // User preferences from temporary Properties object override theme.
080: properties.putAll(temp);
081: }
082:
083: // Returns new Properties with keys converted to lower case.
084: private static Properties canonicalize(Properties properties) {
085: Properties newProperties = new Properties();
086: for (Enumeration e = properties.keys(); e.hasMoreElements();) {
087: String key = (String) e.nextElement();
088: newProperties.put(key.toLowerCase(), properties.get(key));
089: }
090: return newProperties;
091: }
092:
093: // FIXME This is far from ideal (but it does work).
094: public synchronized void killTheme() {
095: Iterator it = properties.keySet().iterator();
096: while (it.hasNext()) {
097: String key = (String) it.next();
098: if (key.startsWith("color."))
099: it.remove();
100: else if (key.indexOf(".color.") >= 0)
101: it.remove();
102: else if (key.startsWith("style."))
103: it.remove();
104: else if (key.indexOf(".style.") >= 0)
105: it.remove();
106: }
107: }
108:
109: private static Properties loadTheme(String themeName,
110: String themePath) {
111: Properties properties = new Properties();
112: File file = getThemeFile(themeName, themePath);
113: if (file != null && file.isFile()) {
114: try {
115: InputStream in = file.getInputStream();
116: properties.load(in);
117: in.close();
118: } catch (IOException e) {
119: Log.error(e);
120: }
121: }
122: return canonicalize(properties);
123: }
124:
125: private static File getThemeFile(String themeName, String themePath) {
126: if (themeName == null)
127: return null;
128: themeName = stripQuotes(themeName);
129:
130: // The string passed in is either the name of a theme ("Anokha") or
131: // the full pathname of the file ("/home/peter/Anokha").
132: if (Utilities.isFilenameAbsolute(themeName))
133: return File.getInstance(themeName);
134:
135: // It's not an absolute filename. Check theme path.
136: if (themePath != null) {
137: Path path = new Path(stripQuotes(themePath));
138: String[] array = path.list();
139: if (array != null) {
140: for (int i = 0; i < array.length; i++) {
141: File dir = File.getInstance(array[i]);
142: if (dir != null && dir.isDirectory()) {
143: File themeFile = File.getInstance(dir,
144: themeName);
145: if (themeFile != null && themeFile.isFile())
146: return themeFile;
147: }
148: }
149: }
150: }
151:
152: // We haven't found it yet. Look in default locations.
153: String classPath = System.getProperty("java.class.path");
154: if (classPath != null) {
155: Path path = new Path(classPath);
156: String[] array = path.list();
157: if (array == null)
158: return null;
159: final File userDir = File.getInstance(System
160: .getProperty("user.dir"));
161: for (int i = 0; i < array.length; i++) {
162: String pathComponent = array[i];
163: if (pathComponent.endsWith("src")) {
164: // "~/j/src"
165: File srcDir = File.getInstance(pathComponent);
166: if (srcDir != null && srcDir.isDirectory()) {
167: File parentDir = srcDir.getParentFile(); // "~/j"
168: if (parentDir != null
169: && parentDir.isDirectory()) {
170: File themeDir = File.getInstance(parentDir,
171: "themes"); // "~/j/themes"
172: if (themeDir != null
173: && themeDir.isDirectory()) {
174: File themeFile = File.getInstance(
175: themeDir, themeName);
176: if (themeFile != null
177: && themeFile.isFile())
178: return themeFile;
179: }
180: }
181: }
182: } else {
183: String suffix = "j.jar";
184: if (pathComponent.endsWith(suffix)) {
185: // "/usr/local/share/j/j.jar"
186: String prefix = pathComponent.substring(0,
187: pathComponent.length()
188: - suffix.length());
189: // "/usr/local/share/j/"
190: File prefixDir;
191: if (prefix.length() == 0) {
192: // j.jar is in working directory ("java -jar j.jar").
193: prefixDir = userDir;
194: } else {
195: // Prefix might be relative to working directory ("java -jar ../j.jar").
196: prefixDir = File.getInstance(userDir,
197: prefix);
198: }
199: if (prefixDir != null
200: && prefixDir.isDirectory()) {
201: // Look for a "themes" subdirectory under prefix directory.
202: File themeDir = File.getInstance(prefixDir,
203: "themes");
204: // "/usr/local/share/j/themes"
205: if (themeDir != null
206: && themeDir.isDirectory()) {
207: File themeFile = File.getInstance(
208: themeDir, themeName);
209: if (themeFile != null
210: && themeFile.isFile())
211: return themeFile;
212: }
213: }
214: }
215: }
216: }
217: }
218: return null;
219: }
220:
221: public synchronized void setProperty(Property property, String value) {
222: properties.setProperty(property.key(), value);
223: }
224:
225: public synchronized void setProperty(String key, String value) {
226: properties.setProperty(key.toLowerCase(), value);
227: }
228:
229: public synchronized void removeProperty(String key) {
230: properties.remove(key.toLowerCase());
231: }
232:
233: // Strips quotes if present.
234: public synchronized String getStringProperty(Property property) {
235: String value = getProperty(property.key());
236: if (value != null)
237: return stripQuotes(value);
238: else
239: return (String) property.getDefaultValue(); // May be null.
240: }
241:
242: // Strips quotes if present.
243: public synchronized String getStringProperty(String key) {
244: String value = getProperty(key);
245: if (value != null)
246: return stripQuotes(value);
247: else
248: return null;
249: }
250:
251: public synchronized boolean getBooleanProperty(Property property) {
252: String value = getProperty(property.key());
253: if (value != null) {
254: value = value.trim();
255: if (value.equals("true") || value.equals("1"))
256: return true;
257: if (value.equals("false") || value.equals("0"))
258: return false;
259: }
260: return ((Boolean) property.getDefaultValue()).booleanValue();
261: }
262:
263: public synchronized boolean getBooleanProperty(Property property,
264: boolean defaultValue) {
265: return getBooleanProperty(property.key(), defaultValue);
266: }
267:
268: public synchronized boolean getBooleanProperty(String key,
269: boolean defaultValue) {
270: String value = getProperty(key);
271: if (value != null) {
272: value = value.trim();
273: if (value.equals("true") || value.equals("1"))
274: return true;
275: if (value.equals("false") || value.equals("0"))
276: return false;
277: }
278: return defaultValue;
279: }
280:
281: public synchronized int getIntegerProperty(Property property) {
282: String value = getProperty(property.key());
283: if (value != null) {
284: value = value.trim();
285: if (value.length() > 0) {
286: // Integer.parseInt() doesn't understand a plus sign.
287: if (value.charAt(0) == '+')
288: value = value.substring(1).trim();
289: try {
290: return Integer.parseInt(value);
291: } catch (NumberFormatException e) {
292: }
293: }
294: }
295: return ((Integer) property.getDefaultValue()).intValue();
296: }
297:
298: public synchronized Color getColorProperty(String key) {
299: String value = getStringProperty(key);
300: if (value != null)
301: return Utilities.getColor(value);
302: return null;
303: }
304:
305: private String getProperty(String key) {
306: return properties.getProperty(key.toLowerCase());
307: }
308:
309: private static String stripQuotes(String s) {
310: final int length = s.length();
311: if (length >= 2) {
312: if (s.charAt(0) == '"' && s.charAt(length - 1) == '"')
313: return s.substring(1, length - 1);
314: else if (s.charAt(0) == '\''
315: && s.charAt(length - 1) == '\'')
316: return s.substring(1, length - 1);
317: }
318: // Not quoted.
319: return s.trim();
320: }
321:
322: public synchronized void addPreferencesChangeListener(
323: PreferencesChangeListener listener) {
324: if (listeners == null)
325: listeners = new ArrayList();
326: listeners.add(listener);
327: }
328:
329: public synchronized void firePreferencesChanged() {
330: if (listeners != null)
331: for (int i = 0; i < listeners.size(); i++)
332: ((PreferencesChangeListener) listeners.get(i))
333: .preferencesChanged();
334: }
335: }
|