001: /*
002: * PropertyManager.java - Manages property files
003: * :tabSize=8:indentSize=8:noTabs=false:
004: * :folding=explicit:collapseFolds=1:
005: *
006: * Copyright (C) 2004 Slava Pestov
007: *
008: * This program is free software; you can redistribute it and/or
009: * modify it under the terms of the GNU General Public License
010: * as published by the Free Software Foundation; either version 2
011: * of the License, or any later version.
012: *
013: * This program is distributed in the hope that it will be useful,
014: * but WITHOUT ANY WARRANTY; without even the implied warranty of
015: * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
016: * GNU General Public License for more details.
017: *
018: * You should have received a copy of the GNU General Public License
019: * along with this program; if not, write to the Free Software
020: * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
021: */
022:
023: package org.gjt.sp.jedit;
024:
025: import java.io.*;
026: import java.util.*;
027:
028: class PropertyManager {
029: //{{{ getProperties() method
030: Properties getProperties() {
031: Properties total = new Properties();
032: total.putAll(system);
033: Iterator iter = plugins.iterator();
034: while (iter.hasNext())
035: total.putAll((Properties) iter.next());
036: total.putAll(site);
037: total.putAll(user);
038: return total;
039: } //}}}
040:
041: //{{{ loadSystemProps() method
042: void loadSystemProps(InputStream in) throws IOException {
043: loadProps(system, in);
044: } //}}}
045:
046: //{{{ loadSiteProps() method
047: void loadSiteProps(InputStream in) throws IOException {
048: loadProps(site, in);
049: } //}}}
050:
051: //{{{ loadUserProps() method
052: void loadUserProps(InputStream in) throws IOException {
053: loadProps(user, in);
054: } //}}}
055:
056: //{{{ saveUserProps() method
057: void saveUserProps(OutputStream out) throws IOException {
058: user.store(out, "jEdit properties");
059: out.close();
060: } //}}}
061:
062: //{{{ loadPluginProps() method
063: Properties loadPluginProps(InputStream in) throws IOException {
064: Properties plugin = new Properties();
065: loadProps(plugin, in);
066: plugins.add(plugin);
067: return plugin;
068: } //}}}
069:
070: //{{{ addPluginProps() method
071: void addPluginProps(Properties props) {
072: plugins.add(props);
073: } //}}}
074:
075: //{{{ removePluginProps() method
076: void removePluginProps(Properties props) {
077: plugins.remove(props);
078: } //}}}
079:
080: //{{{ getProperty() method
081: String getProperty(String name) {
082: String value = user.getProperty(name);
083: if (value != null)
084: return value;
085: else
086: return getDefaultProperty(name);
087: } //}}}
088:
089: //{{{ setProperty() method
090: void setProperty(String name, String value) {
091: String prop = getDefaultProperty(name);
092:
093: /* if value is null:
094: * - if default is null, unset user prop
095: * - else set user prop to ""
096: * else
097: * - if default equals value, ignore
098: * - if default doesn't equal value, set user
099: */
100: if (value == null) {
101: if (prop == null || prop.length() == 0)
102: user.remove(name);
103: else
104: user.put(name, "");
105: } else {
106: if (value.equals(prop))
107: user.remove(name);
108: else
109: user.put(name, value);
110: }
111: } //}}}
112:
113: //{{{ setTemporaryProperty() method
114: public void setTemporaryProperty(String name, String value) {
115: user.remove(name);
116: system.put(name, value);
117: } //}}}
118:
119: //{{{ unsetProperty() method
120: void unsetProperty(String name) {
121: if (getDefaultProperty(name) != null)
122: user.put(name, "");
123: else
124: user.remove(name);
125: } //}}}
126:
127: //{{{ resetProperty() method
128: public void resetProperty(String name) {
129: user.remove(name);
130: } //}}}
131:
132: //{{{ Private members
133: private Properties system = new Properties();
134: private List plugins = new LinkedList();
135: private Properties site = new Properties();
136: private Properties user = new Properties();
137:
138: //{{{ getDefaultProperty() method
139: private String getDefaultProperty(String name) {
140: String value = site.getProperty(name);
141: if (value != null)
142: return value;
143:
144: Iterator iter = plugins.iterator();
145: while (iter.hasNext()) {
146: value = ((Properties) iter.next()).getProperty(name);
147: if (value != null)
148: return value;
149: }
150:
151: return system.getProperty(name);
152: } //}}}
153:
154: //{{{ loadProps() method
155: private void loadProps(Properties into, InputStream in)
156: throws IOException {
157: try {
158: into.load(in);
159: } finally {
160: in.close();
161: }
162: } //}}}
163:
164: //}}}
165: }
|