001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010: package de.uka.ilkd.key.gui.configuration;
011:
012: import java.util.*;
013: import java.util.Map.Entry;
014:
015: import de.uka.ilkd.key.gui.GUIEvent;
016: import de.uka.ilkd.key.logic.*;
017:
018: public class ChoiceSettings implements Settings {
019:
020: private static final String DEFAULTCHOICES_KEY = "[Choice]DefaultChoices";
021: private static final String CHOICES_KEY = "[Choice]Choices";
022: private LinkedList listenerList = new LinkedList();
023: private HashMap category2Default;
024: /** maps categories to a set of Strings(representing the choices
025: * which are options for this category).*/
026: private HashMap category2Choices = new HashMap();
027:
028: public ChoiceSettings() {
029: category2Default = new HashMap();
030: }
031:
032: public ChoiceSettings(HashMap category2Default) {
033: this .category2Default = category2Default;
034: }
035:
036: public void setDefaultChoices(HashMap category2Default) {
037: HashMap category2Defaultold = this .category2Default;
038: this .category2Default = category2Default;
039: if (category2Defaultold != null
040: && !category2Defaultold.equals(category2Default)) {
041: fireSettingsChanged();
042: }
043: }
044:
045: /** returns a copy of the HashMap that maps categories to
046: * their choices. */
047: public HashMap getChoices() {
048: return (HashMap) category2Choices.clone();
049: }
050:
051: /** returns a copy of the HashMap that maps categories to
052: * their default choices. */
053: public HashMap getDefaultChoices() {
054: return (HashMap) category2Default.clone();
055: }
056:
057: /**
058: * returns the current selected choices as set
059: */
060: public SetOfChoice getDefaultChoicesAsSet() {
061: return choiceMap2choiceSet(category2Default);
062: }
063:
064: private SetOfChoice choiceMap2choiceSet(HashMap ccc) {
065: final Iterator choiceIter = ccc.entrySet().iterator();
066: SetOfChoice choices = SetAsListOfChoice.EMPTY_SET;
067: while (choiceIter.hasNext()) {
068: final Map.Entry entry = (Entry) choiceIter.next();
069: choices = choices.add(new Choice(new Name(entry.getValue()
070: .toString()), entry.getKey().toString()));
071: }
072: return choices;
073: }
074:
075: /** updates <code>category2Choices</code> if new entries are found
076: * in <code>choiceNS</code> or if entries of <code>category2Choices</code>
077: * are no longer present in <code>choiceNS</code>
078: * @param remove remove entries not present in <code>choiceNS</code> */
079: public void updateChoices(Namespace choiceNS, boolean remove) {
080: IteratorOfNamed it = choiceNS.allElements().iterator();
081: HashMap c2C = new HashMap();
082: Choice c;
083: Set soc;
084: while (it.hasNext()) {
085: c = (Choice) it.next();
086: if (c2C.containsKey(c.category())) {
087: soc = (Set) c2C.get(c.category().toString());
088: soc.add(c.name().toString());
089: c2C.put(c.category(), soc);
090: } else {
091: soc = new HashSet();
092: soc.add(c.name().toString());
093: c2C.put(c.category(), soc);
094: }
095: }
096: if (!c2C.equals(category2Choices)) {
097: if (remove) {
098: category2Choices = c2C;
099: fireSettingsChanged();
100: } else {
101: category2Choices.putAll(c2C);
102: ProofSettings.DEFAULT_SETTINGS.saveSettings();
103: }
104: }
105: Iterator catIt = getDefaultChoices().keySet().iterator();
106: while (catIt.hasNext()) {
107: String s = (String) catIt.next();
108: if (category2Choices.containsKey(s)) {
109: if (!((Set) category2Choices.get(s))
110: .contains(category2Default.get(s))) {
111: category2Default.put(s, ((Set) category2Choices
112: .get(s)).iterator().next());
113: fireSettingsChanged();
114: }
115: } else {
116: category2Default.remove(s);
117: fireSettingsChanged();
118: }
119: }
120: }
121:
122: /** sends the message that the state of this setting has been
123: * changed to its registered listeners (not thread-safe)
124: */
125: protected void fireSettingsChanged() {
126: Iterator it = listenerList.iterator();
127: ProofSettings.DEFAULT_SETTINGS.saveSettings();
128: while (it.hasNext()) {
129: ((SettingsListener) it.next())
130: .settingsChanged(new GUIEvent(this ));
131: }
132: }
133:
134: /** gets a Properties object and has to perform the necessary
135: * steps in order to change this object in a way that it
136: * represents the stored settings
137: */
138: public void readSettings(Properties props) {
139: String choiceSequence = props.getProperty(DEFAULTCHOICES_KEY);
140: // set choices
141: if (choiceSequence != null) {
142: StringTokenizer st = new StringTokenizer(choiceSequence,
143: ",");
144: while (st.hasMoreTokens()) {
145: StringTokenizer st2 = new StringTokenizer(st
146: .nextToken().trim(), "-");
147: String category = st2.nextToken().trim();
148: String def = st2.nextToken().trim();
149: category2Default.put(category, def);
150:
151: }
152: }
153: choiceSequence = props.getProperty(CHOICES_KEY);
154: if (choiceSequence != null) {
155: StringTokenizer st = new StringTokenizer(choiceSequence,
156: ",");
157: while (st.hasMoreTokens()) {
158: StringTokenizer st2 = new StringTokenizer(st
159: .nextToken().trim(), "-");
160: String category = st2.nextToken().trim();
161: Set soc = new HashSet();
162: while (st2.hasMoreTokens()) {
163: soc.add(st2.nextToken().trim());
164: }
165: category2Choices.put(category, soc);
166: }
167: }
168: }
169:
170: /** implements the method required by the Settings interface. The
171: * settings are written to the given Properties object. Only entries of
172: * the form < key > = < value > (,< value >)* are allowed.
173: * @param props the Properties object where to write the
174: * settings as (key, value) pair
175: */
176: public void writeSettings(Properties props) {
177: Map.Entry entry;
178: String choiceSequence = "";
179: Iterator it = category2Default.entrySet().iterator();
180: while (it.hasNext()) {
181: entry = (Map.Entry) it.next();
182: choiceSequence += entry.getKey().toString() + "-"
183: + entry.getValue().toString();
184: if (it.hasNext()) {
185: choiceSequence += " , ";
186: }
187: }
188: props.setProperty(DEFAULTCHOICES_KEY, choiceSequence);
189: choiceSequence = "";
190: it = category2Choices.keySet().iterator();
191: while (it.hasNext()) {
192: String cat = (String) it.next();
193: Set soc = (Set) category2Choices.get(cat);
194: choiceSequence += cat;
195: Iterator it2 = soc.iterator();
196: while (it2.hasNext()) {
197: choiceSequence += "-" + it2.next().toString();
198: }
199: if (it.hasNext()) {
200: choiceSequence += " , ";
201: }
202: }
203: props.setProperty(CHOICES_KEY, choiceSequence);
204: }
205:
206: public ChoiceSettings updateWith(SetOfChoice sc) {
207: IteratorOfChoice it = sc.iterator();
208: while (it.hasNext()) {
209: Choice c = it.next();
210: if (category2Default.containsKey(c.category())) {
211: category2Default.remove(c.category());
212: }
213: category2Default.put(c.category(), c.name().toString());
214: }
215: return this ;
216: }
217:
218: /** adds a listener to the settings object
219: * @param l the listener
220: */
221: public void addSettingsListener(SettingsListener l) {
222: listenerList.add(l);
223: }
224: }
|