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.io.*;
013: import java.net.URL;
014: import java.util.*;
015:
016: import de.uka.ilkd.key.gui.DecisionProcedureSettings;
017: import de.uka.ilkd.key.gui.GUIEvent;
018: import de.uka.ilkd.key.gui.ModelSourceSettings;
019: import de.uka.ilkd.key.proof.init.JavaProfile;
020: import de.uka.ilkd.key.proof.init.Profile;
021: import de.uka.ilkd.key.util.Debug;
022: import de.uka.ilkd.key.util.KeYResourceManager;
023:
024: /** This class is used to load and save settings for proofs such as
025: * which data type models are used to represent the java types. Which
026: * heuristics have to be loaded and so on.
027: * The class loads the file proofsettings.config from the place where
028: * you started key. If the file is not available standard settings are
029: * used.
030: * The loaded file has the following structure:
031: * <code>
032: * // KeY-Configuration file
033: * ActiveHeuristics=simplify_prog , simplify
034: * MaximumNumberOfHeuristcsApplications=400
035: * number = IntegerLDT.class
036: * boolean = BooleanLDT.class
037: * </code>
038: */
039: public class ProofSettings {
040:
041: public static final File PROVER_CONFIG_FILE;
042: public static final URL PROVER_CONFIG_FILE_TEMPLATE;
043: public static final ProofSettings DEFAULT_SETTINGS;
044:
045: static {
046: PROVER_CONFIG_FILE = new File(PathConfig.KEY_CONFIG_DIR
047: + File.separator + "proof-settings.props");
048: PROVER_CONFIG_FILE_TEMPLATE = KeYResourceManager.getManager()
049: .getResourceFile(ProofSettings.class,
050: "default-proof-settings.props");
051: DEFAULT_SETTINGS = new ProofSettings();
052: }
053:
054: private boolean initialized = false;
055:
056: /** all setting objects in the following order: heuristicSettings */
057: private Settings[] settings;
058:
059: /** the default listener to settings */
060: private ProofSettingsListener listener = new ProofSettingsListener();
061:
062: /** profile */
063: private Profile profile;
064:
065: /** create a proof settings object */
066: public ProofSettings() {
067: settings = new Settings[] { new StrategySettings(),
068: new ModelSourceSettings(),
069: new SimultaneousUpdateSimplifierSettings(),
070: new GeneralSettings(), new ChoiceSettings(),
071: new DecisionProcedureSettings(), new ViewSettings(),
072: new LibrariesSettings() };
073: for (int i = 0; i < settings.length; i++) {
074: settings[i].addSettingsListener(listener);
075: }
076: }
077:
078: /* copy constructor - substitutes .clone() in classes implementing Settings */
079: public ProofSettings(ProofSettings toCopy) {
080: this ();
081:
082: Properties result = new Properties();
083: Settings[] s = toCopy.settings;
084:
085: for (int i = 0; i < s.length; i++) {
086: s[i].writeSettings(result);
087: }
088:
089: for (int i = settings.length - 1; i >= 0; i--) {
090: settings[i].readSettings(result);
091: }
092: initialized = true;
093: setProfile(toCopy.getProfile());
094: }
095:
096: public void ensureInitialized() {
097: if (!initialized) {
098: loadSettings();
099: initialized = true;
100: }
101: }
102:
103: public void setProfile(Profile profile) {
104: ensureInitialized();
105: this .profile = profile;
106: }
107:
108: public Profile getProfile() {
109: if (profile == null) {
110: //the following line should be removed
111: profile = new JavaProfile();
112: }
113: return profile;
114: }
115:
116: /**
117: * Used by saveSettings() and settingsToString()
118: */
119: public void settingsToStream(Settings[] s, OutputStream out) {
120: try {
121: Properties result = new Properties();
122: for (int i = 0; i < s.length; i++) {
123: s[i].writeSettings(result);
124: }
125: result.store(out, "Proof-Settings-Config-File");
126: } catch (IOException e) {
127: System.err
128: .println("Warning: could not save proof-settings.");
129: System.err.println(e);
130: Debug.out(e);
131: }
132: }
133:
134: /**
135: * Saves the current settings in this dialog into a configuration file.
136: */
137: public void saveSettings() {
138: try {
139: if (!PROVER_CONFIG_FILE.exists()) {
140: new File(PathConfig.KEY_CONFIG_DIR + File.separator)
141: .mkdirs();
142: PROVER_CONFIG_FILE.createNewFile();
143: }
144: FileOutputStream out = new FileOutputStream(
145: PROVER_CONFIG_FILE);
146: settingsToStream(settings, out);
147: } catch (IOException e) {
148: System.err
149: .println("Warning: could not save proof-settings.");
150: System.err.println(e);
151: Debug.out(e);
152: }
153: }
154:
155: public String settingsToString() {
156: ByteArrayOutputStream out = new ByteArrayOutputStream();
157: settingsToStream(settings, out);
158: return new String(out.toByteArray());
159: }
160:
161: /** Used by loadSettings() and loadSettingsFromString(...) */
162: public void loadSettingsFromStream(InputStream in) {
163: Properties defaultProps = new Properties();
164:
165: if (PROVER_CONFIG_FILE_TEMPLATE == null)
166: System.err
167: .println("Warning: default proof-settings file could not be found.");
168: else {
169: try {
170: defaultProps.load(PROVER_CONFIG_FILE_TEMPLATE
171: .openStream());
172: } catch (IOException e) {
173: System.err
174: .println("Warning: default proof-settings could not be loaded.");
175: Debug.out(e);
176: }
177: }
178:
179: Properties props = new Properties(defaultProps);
180: try {
181: props.load(in);
182: } catch (IOException e) {
183: System.err
184: .println("Warning: no proof-settings could be loaded, using defaults");
185: Debug.out(e);
186: }
187:
188: for (int i = settings.length - 1; i >= 0; i--) {
189: settings[i].readSettings(props);
190: }
191:
192: initialized = true;
193: }
194:
195: /**
196: * Loads the the former settings from configuration file.
197: */
198: public void loadSettings() {
199: try {
200: FileInputStream in = new FileInputStream(PROVER_CONFIG_FILE);
201: loadSettingsFromStream(in);
202: } catch (IOException e) {
203: System.err
204: .println("Warning: no proof-settings could be loaded, using defaults");
205: Debug.out(e);
206: }
207: }
208:
209: /** Used to load Settings from a .key file*/
210: public void loadSettingsFromString(String s) {
211: if (s == null)
212: return;
213: StringBufferInputStream in = new StringBufferInputStream(s);
214: loadSettingsFromStream(in);
215: }
216:
217: /** returns the StrategySettings object
218: * @return the StrategySettings object
219: */
220: public StrategySettings getStrategySettings() {
221: ensureInitialized();
222: return (StrategySettings) settings[0];
223: }
224:
225: /** returns the ChoiceSettings object
226: * @return the ChoiceSettings object
227: */
228: public ChoiceSettings getChoiceSettings() {
229: ensureInitialized();
230: return (ChoiceSettings) settings[4];
231: }
232:
233: public ProofSettings setChoiceSettings(ChoiceSettings cs) {
234: settings[4] = cs;
235: return this ;
236: }
237:
238: /** returns the DecisionProcedureSettings object
239: * @return the DecisionProcedureSettings object
240: */
241: public DecisionProcedureSettings getDecisionProcedureSettings() {
242: ensureInitialized();
243: return (DecisionProcedureSettings) settings[5];
244: }
245:
246: public ModelSourceSettings getModelSourceSettings() {
247: ensureInitialized();
248: return (ModelSourceSettings) settings[1];
249: }
250:
251: public SimultaneousUpdateSimplifierSettings getSimultaneousUpdateSimplifierSettings() {
252: ensureInitialized();
253: return (SimultaneousUpdateSimplifierSettings) settings[2];
254: }
255:
256: public LibrariesSettings getLibrariesSettings() {
257: ensureInitialized();
258: return (LibrariesSettings) settings[7];
259: }
260:
261: public GeneralSettings getGeneralSettings() {
262: ensureInitialized();
263: return (GeneralSettings) settings[3];
264: }
265:
266: public ViewSettings getViewSettings() {
267: ensureInitialized();
268: return (ViewSettings) settings[6];
269: }
270:
271: private class ProofSettingsListener implements SettingsListener {
272:
273: ProofSettingsListener() {
274: }
275:
276: /** called by the Settings object to inform the listener that its
277: * state has changed
278: * @param e the Event sent to the listener
279: */
280: public void settingsChanged(GUIEvent e) {
281: saveSettings();
282: }
283:
284: }
285:
286: }
|