1 | // Jomic - a viewer for comic book archives. |
2 | // Copyright (C) 2004-2011 Thomas Aglassinger |
3 | // |
4 | // This program is free software: you can redistribute it and/or modify |
5 | // it under the terms of the GNU General Public License as published by |
6 | // the Free Software Foundation, either version 3 of the License, or |
7 | // (at your option) any later version. |
8 | // |
9 | // This program is distributed in the hope that it will be useful, |
10 | // but WITHOUT ANY WARRANTY; without even the implied warranty of |
11 | // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
12 | // GNU General Public License for more details. |
13 | // |
14 | // You should have received a copy of the GNU General Public License |
15 | // along with this program. If not, see <http://www.gnu.org/licenses/>. |
16 | package net.sf.jomic.tools; |
17 | |
18 | import java.awt.Color; |
19 | import java.awt.Component; |
20 | import java.awt.Dimension; |
21 | import java.awt.Point; |
22 | import java.awt.Toolkit; |
23 | import java.beans.PropertyChangeListener; |
24 | import java.beans.PropertyChangeSupport; |
25 | import java.io.File; |
26 | import java.text.ParseException; |
27 | import java.util.Properties; |
28 | |
29 | import org.apache.commons.logging.Log; |
30 | import org.apache.commons.logging.LogFactory; |
31 | |
32 | /** |
33 | * Extended <code>Properties</code> with additional features. |
34 | * <ul> |
35 | * <li> Type-safe getters and setters, for example <code>getIntProperty()</code> |
36 | * <li> Possibility to listen for changes |
37 | * <li> Overridable by end user by setting corresponding system properties at application launch |
38 | * (typically using the <code>java -D</code> option) |
39 | * <li> Optional default values using <code>setDefault()</code>. This simplifies writing |
40 | * specialized getters and setters conforming to the Java Beans naming conventions with |
41 | * predictable default value behavior. (The original <code>Properties</code> allow to specify |
42 | * default properties to the constructor, but it is not documented if the can be changed at run |
43 | * time.) |
44 | * </ul> |
45 | * |
46 | * |
47 | * @author Thomas Aglassinger |
48 | * @see java.util.Properties |
49 | * @see java.beans.PropertyChangeSupport |
50 | */ |
51 | public class BasicSettings extends Properties |
52 | { |
53 | static final String DEFAULT_COLOR = "#000000"; |
54 | |
55 | /** |
56 | * Slack in percent of screen size which part of a window is allowed to be of screen before its |
57 | * location and size are adjusted automatically to ensure that it is visible. |
58 | */ |
59 | static final double SLACK = 0.10; |
60 | |
61 | /** |
62 | * Minimum number of pixels that must be visible of a window vertically and horizontally before |
63 | * its location and size are adjusted automatically to ensure that it is visible. |
64 | */ |
65 | static final int SNAP = 3; |
66 | private static final int COMPONENT_AREA_HEIGHT_INDEX = 3; |
67 | private static final int COMPONENT_AREA_WIDTH_INDEX = 2; |
68 | private static final int COMPONENT_AREA_X_INDEX = 0; |
69 | private static final int COMPONENT_AREA_Y_INDEX = 1; |
70 | |
71 | /** |
72 | * Values needed to specify what area a AWT component covers. |
73 | */ |
74 | private static final int EXPECTED_COMPONENT_AREA_VALUE_COUNT = 4; |
75 | private PropertyChangeSupport changes; |
76 | private Log logger; |
77 | private /*@ spec_public @*/ StringTools stringTools; |
78 | private /*@ spec_public nullable @*/ String systemPropertyPrefix; |
79 | |
80 | protected BasicSettings() { |
81 | super(new Properties()); |
82 | logger = LogFactory.getLog(BasicSettings.class); |
83 | stringTools = StringTools.instance(); |
84 | changes = new PropertyChangeSupport(this); |
85 | } |
86 | |
87 | //@ requires isValidPropertyName(key); |
88 | public void setBooleanProperty(String key, boolean value) { |
89 | String textValue = Boolean.toString(value); |
90 | |
91 | setProperty(key, textValue); |
92 | } |
93 | |
94 | /** |
95 | * Set property <code>key</code> to <code>newValue</code>, and notify |
96 | * all listeners about the change. |
97 | * |
98 | * @exception IllegalArgumentException |
99 | * if <code>newValue</code> is not within <code>possibleChoices</code>. |
100 | */ |
101 | //@ requires isValidPropertyName(key); |
102 | //@ requires stringTools.isSorted(possibleChoices); |
103 | public void setChoiceProperty(String key, String newValue, String[] possibleChoices) { |
104 | if (stringTools.equalsAnyOf(possibleChoices, newValue)) { |
105 | setProperty(key, newValue); |
106 | } else { |
107 | throw new IllegalArgumentException(key + ": " + stringTools.sourced(newValue) |
108 | + " not in " + stringTools.arrayToString(possibleChoices)); |
109 | } |
110 | } |
111 | |
112 | /** |
113 | * Sets property <code>key</code> to a string representation of <code>newColor</code>, and |
114 | * notifies all listeners about the change. |
115 | */ |
116 | //@ requires isValidPropertyName(key); |
117 | public void setColorProperty(String key, Color newColor) { |
118 | setProperty(key, stringTools.colorString(newColor)); |
119 | } |
120 | |
121 | /** |
122 | * Set property <code>propertyName</code> to store the location and dimension of <code>component</code> |
123 | * . |
124 | */ |
125 | //@ requires isValidPropertyName(propertyName); |
126 | public void setComponentAreaProperty(String propertyName, Component component) { |
127 | Point location = component.getLocation(); |
128 | Dimension dimension = component.getSize(); |
129 | int[] values = new int[]{ |
130 | location.x, location.y, dimension.width, dimension.height |
131 | }; |
132 | String value = stringTools.arrayToString(values); |
133 | |
134 | setProperty(propertyName, value); |
135 | } |
136 | |
137 | //@ requires isValidPropertyName(propertyName); |
138 | public void setFileProperty(String propertyName, /*@ nullable @*/ File newValue) { |
139 | String filePath; |
140 | |
141 | if (newValue == null) { |
142 | filePath = null; |
143 | } else { |
144 | filePath = newValue.getAbsolutePath(); |
145 | } |
146 | setProperty(propertyName, filePath); |
147 | } |
148 | |
149 | //@ requires isValidPropertyName(key); |
150 | public void setIntProperty(String key, int value) { |
151 | setProperty(key, Integer.toString(value)); |
152 | } |
153 | |
154 | //@ requires isValidPropertyName(key); |
155 | //@ requires minValue <= maxValue; |
156 | public void setLimitedIntProperty(String key, int value, int minValue, int maxValue) { |
157 | if (value < minValue) { |
158 | throw new IllegalArgumentException(key + ": " + value + " < " + minValue); |
159 | } else if (value > maxValue) { |
160 | throw new IllegalArgumentException(key + ": " + value + " > " + maxValue); |
161 | } |
162 | setProperty(key, Integer.toString(value)); |
163 | } |
164 | |
165 | /** |
166 | * Set property with name <code>key</code> to <code>value</code>. |
167 | */ |
168 | //@ also |
169 | //@ requires isValidPropertyName(key); |
170 | public /*@ nullable @*/ Object setProperty(String key, /*@ nullable @*/ String value) { |
171 | if (logger.isDebugEnabled()) { |
172 | logger.debug("set property " + key + " to: " + stringTools.sourced(value)); |
173 | } |
174 | Object oldValue = getProperty(key); |
175 | |
176 | super.setProperty(key, value); |
177 | firePropertyChangeEvent(key, oldValue, value); |
178 | return oldValue; |
179 | } |
180 | |
181 | //@ requires newSystemPropertyPrefix.length() > 0; |
182 | //@ requires newSystemPropertyPrefix.endsWith("."); |
183 | public void setSystemPropertyPrefix(String newSystemPropertyPrefix) { |
184 | systemPropertyPrefix = newSystemPropertyPrefix; |
185 | } |
186 | |
187 | /** |
188 | * Set the default value for property <code>key</code> to <code>value</code>. |
189 | */ |
190 | //@ requires isValidPropertyName(key); |
191 | protected void setDefault(String key, /*@ nullable @*/ String value) { |
192 | defaults.setProperty(key, value); |
193 | } |
194 | |
195 | /** |
196 | * Set the default value for integer property <code>key</code> to <code>value</code>. |
197 | */ |
198 | //@ requires isValidPropertyName(key); |
199 | protected void setDefault(String key, int value) { |
200 | setDefault(key, Integer.toString(value)); |
201 | } |
202 | |
203 | /** |
204 | * Set the default value for boolean property <code>key</code> to <code>value</code>. |
205 | */ |
206 | //@ requires isValidPropertyName(key); |
207 | protected void setDefault(String key, boolean value) { |
208 | setDefault(key, Boolean.toString(value)); |
209 | } |
210 | |
211 | //@ requires isValidPropertyName(key); |
212 | public /*@ pure @*/ boolean getBooleanProperty(String key) { |
213 | boolean result; |
214 | String value = getProperty(key); |
215 | |
216 | if (value != null) { |
217 | result = Boolean.valueOf(value).booleanValue(); |
218 | } else { |
219 | result = false; |
220 | } |
221 | return result; |
222 | } |
223 | |
224 | //@ requires isValidPropertyName(propertyName); |
225 | //@ requires stringTools.isSorted(possibleChoices); |
226 | public String getChoiceProperty(String propertyName, String[] possibleChoices) { |
227 | String result = getProperty(propertyName); |
228 | |
229 | if (!stringTools.equalsAnyOf(possibleChoices, result)) { |
230 | String fixedResult = defaults.getProperty(propertyName, possibleChoices[0]); |
231 | |
232 | logger.warn("resetting " + propertyName + " from " + result + " to " + fixedResult |
233 | + " because it is not one of " + stringTools.arrayToString(possibleChoices)); |
234 | super.setProperty(propertyName, fixedResult); |
235 | result = fixedResult; |
236 | } |
237 | |
238 | return result; |
239 | } |
240 | //@ requires isValidPropertyName(propertyName); |
241 | public /*@ nullable pure @*/ Color getColorProperty(String propertyName) { |
242 | Color result = null; |
243 | String value = getProperty(propertyName); |
244 | boolean useDefaultColor = (value == null); |
245 | |
246 | if (!useDefaultColor) { |
247 | try { |
248 | result = Color.decode(value); |
249 | } catch (NumberFormatException error) { |
250 | useDefaultColor = true; |
251 | } |
252 | } |
253 | |
254 | if (useDefaultColor) { |
255 | String defaultValue = defaults.getProperty(propertyName, DEFAULT_COLOR); |
256 | |
257 | logger.warn( |
258 | "property " |
259 | + propertyName |
260 | + ": using default \"" |
261 | + defaultValue |
262 | + "\" because value \"" |
263 | + value |
264 | + "\" is not a color of the form \"#rrggbb\""); |
265 | result = Color.decode(defaultValue); |
266 | } |
267 | |
268 | return result; |
269 | } |
270 | |
271 | //@ requires isValidPropertyName(propertyName); |
272 | public /*@ nullable pure @*/ File getFileProperty(String propertyName) { |
273 | File result; |
274 | String value = getProperty(propertyName); |
275 | |
276 | if (value == null) { |
277 | result = null; |
278 | } else { |
279 | result = new File(value); |
280 | } |
281 | return result; |
282 | } |
283 | |
284 | //@ requires isValidPropertyName(propertyName); |
285 | public /*@ pure @*/ int getIntProperty(String propertyName) { |
286 | int result; |
287 | String value = getProperty(propertyName); |
288 | |
289 | try { |
290 | result = Integer.parseInt(value); |
291 | } catch (NumberFormatException error) { |
292 | String defaultValue = defaults.getProperty(propertyName, Integer.toString(0)); |
293 | |
294 | logger.warn( |
295 | "property " |
296 | + propertyName |
297 | + ": using default " |
298 | + defaultValue |
299 | + " because value \"" |
300 | + value |
301 | + "\" is not an integer"); |
302 | result = Integer.parseInt(defaultValue); |
303 | } |
304 | return result; |
305 | } |
306 | |
307 | /** |
308 | * Get property <code>propertyName</code> and make sure that it is within |
309 | * <code>minValue</code> and <code>maxValue</code>. If it is not, fix |
310 | * it by resetting it to its default. If there is no default for this |
311 | * property, reset it to the average of <code>minValue</code> and |
312 | * <code>maxValue</code>. |
313 | */ |
314 | //@ requires isValidPropertyName(propertyName); |
315 | //@ requires minValue <= maxValue; |
316 | //@ ensures \result >= minValue; |
317 | //@ ensures \result <= maxValue; |
318 | public int getLimitedIntProperty(String propertyName, int minValue, int maxValue) { |
319 | int result = getIntProperty(propertyName); |
320 | if ((result < minValue) || (result > maxValue)) { |
321 | int averageValue = (minValue + maxValue) / 2; |
322 | String defaultValue = defaults.getProperty(propertyName, Integer.toString(averageValue)); |
323 | int fixedResult = Integer.parseInt(defaultValue); |
324 | |
325 | logger.warn("resetting " + propertyName + " from " + result + " to " + fixedResult |
326 | + " because it is not within a range of " + minValue + "..." + maxValue); |
327 | result = fixedResult; |
328 | setLimitedIntProperty(propertyName, result, minValue, maxValue); |
329 | } |
330 | return result; |
331 | } |
332 | |
333 | /** |
334 | * @deprecated use setDefault() to specify a default value |
335 | * @see #setDefault(String, String) |
336 | */ |
337 | public /*@ nullable pure @*/ String getProperty(String name, String defaultValue) { |
338 | throw new IllegalStateException("defaultValue must be stored using setDefault()"); |
339 | } |
340 | |
341 | //@ also |
342 | //@ requires isValidPropertyName(name); |
343 | public /*@ nullable pure @*/ String getProperty(String name) { |
344 | String result; |
345 | |
346 | if (systemPropertyPrefix != null) { |
347 | String systemPropertyName = getSystemPropertyName(name); |
348 | |
349 | result = System.getProperty(systemPropertyName); |
350 | } else { |
351 | result = null; |
352 | } |
353 | |
354 | if (result == null) { |
355 | result = super.getProperty(name); |
356 | } |
357 | return result; |
358 | } |
359 | |
360 | /** |
361 | * Get name of system property corresponding to application property <code>name</code>. |
362 | */ |
363 | //@ requires isValidPropertyName(name); |
364 | //@ requires systemPropertyPrefix != null; |
365 | public /*@ pure @*/ String getSystemPropertyName(String name) { |
366 | return systemPropertyPrefix + name; |
367 | } |
368 | |
369 | public void addPropertyChangeListener(PropertyChangeListener listener) { |
370 | changes.addPropertyChangeListener(listener); |
371 | } |
372 | |
373 | public void addPropertyChangeListener(String propertyName, PropertyChangeListener listener) { |
374 | changes.addPropertyChangeListener(propertyName, listener); |
375 | } |
376 | |
377 | /** |
378 | * Yields <code>true</code> if the specified window coordinates and size are outside of the |
379 | * screen (given some slack). |
380 | */ |
381 | private boolean isOutsideOfScreen(String propertyName, int x, int y, int width, int height) { |
382 | boolean result = false; |
383 | Dimension screenSize = Toolkit.getDefaultToolkit().getScreenSize(); |
384 | int screenWidth = screenSize.width; |
385 | int screenHeight = screenSize.height; |
386 | double slackX = screenWidth * SLACK; |
387 | int minX = 0 - (int) slackX; |
388 | int maxX = screenWidth - SNAP; |
389 | int minY = 0; |
390 | int maxY = screenHeight - SNAP; |
391 | int maxWidth = screenWidth + SNAP; |
392 | int maxHeight = screenHeight + SNAP; |
393 | |
394 | if (x < minX) { |
395 | logger.warn(propertyName + ".x is too small, resetting (" + x + " < " + minX + ")"); |
396 | result = true; |
397 | } else if (x > maxX) { |
398 | logger.warn(propertyName + ".x is too large, resetting (" + x + " > " + maxX + ")"); |
399 | result = true; |
400 | } else if (y < minY) { |
401 | logger.warn(propertyName + ".y is too small, resetting (" + y + " < " + minY + ")"); |
402 | result = true; |
403 | } else if (y > maxY) { |
404 | logger.warn(propertyName + ".y is too large, resetting (" + y + " > " + maxY + ")"); |
405 | result = true; |
406 | } else if (width > maxWidth) { |
407 | logger.warn(propertyName + ".width is too large, resetting (" |
408 | + width + " > " + maxWidth + ")"); |
409 | result = true; |
410 | } else if (height > maxHeight) { |
411 | logger.warn(propertyName + ".height is too large, resetting (" |
412 | + height + " > " + maxHeight + ")"); |
413 | result = true; |
414 | } |
415 | return result; |
416 | } |
417 | |
418 | /** |
419 | * Apply the component location and dimension stored in <code>propertyName</code> on <code>component</code> |
420 | * . |
421 | */ |
422 | //@ requires isValidPropertyName(propertyName); |
423 | public void applyComponentAreaProperty(String propertyName, Component component) { |
424 | String value = getProperty(propertyName); |
425 | |
426 | if (value != null) { |
427 | try { |
428 | int[] intValues = stringTools.stringToIntArray(value); |
429 | int actualComponentAreaValueCount = intValues.length; |
430 | |
431 | if (actualComponentAreaValueCount == EXPECTED_COMPONENT_AREA_VALUE_COUNT) { |
432 | int x = intValues[COMPONENT_AREA_X_INDEX]; |
433 | int y = intValues[COMPONENT_AREA_Y_INDEX]; |
434 | int width = intValues[COMPONENT_AREA_WIDTH_INDEX]; |
435 | int height = intValues[COMPONENT_AREA_HEIGHT_INDEX]; |
436 | |
437 | // If area is outside of screen (given some slack), reset area |
438 | Dimension screenSize = Toolkit.getDefaultToolkit().getScreenSize(); |
439 | int screenWidth = screenSize.width; |
440 | int screenHeight = screenSize.height; |
441 | boolean reset = isOutsideOfScreen(propertyName, x, y, width, height); |
442 | |
443 | if (reset) { |
444 | // Attempt to reset to default value |
445 | remove(propertyName); |
446 | |
447 | String defaultValue = getProperty(propertyName); |
448 | |
449 | if (defaultValue == null) { |
450 | // No default, figure out some area that is guaranteed to be visible |
451 | // (Component does not have pack()) |
452 | width = screenWidth / 2; |
453 | height = screenHeight / 2; |
454 | x = (screenWidth - width) / 2; |
455 | y = (screenHeight - height) / 2; |
456 | } else { |
457 | // Use the default value |
458 | int[] intDefaultValues = stringTools.stringToIntArray(defaultValue); |
459 | |
460 | assert intDefaultValues.length == EXPECTED_COMPONENT_AREA_VALUE_COUNT |
461 | : "default value for property " + propertyName + " must be fixed: " |
462 | + stringTools.sourced(defaultValue); |
463 | x = intDefaultValues[COMPONENT_AREA_X_INDEX]; |
464 | y = intDefaultValues[COMPONENT_AREA_Y_INDEX]; |
465 | width = intDefaultValues[COMPONENT_AREA_WIDTH_INDEX]; |
466 | height = intDefaultValues[COMPONENT_AREA_HEIGHT_INDEX]; |
467 | } |
468 | } |
469 | |
470 | component.setLocation(x, y); |
471 | component.setSize(width, height); |
472 | } else { |
473 | // No need to localize because this message only shows up in the log (see "catch" below). |
474 | throw new ParseException( |
475 | "component area must be specified using " + EXPECTED_COMPONENT_AREA_VALUE_COUNT |
476 | + " instead of " + actualComponentAreaValueCount + " items", 0); |
477 | } |
478 | } catch (Exception error) { |
479 | logger.warn("cannot use value of property " + stringTools.sourced(propertyName) |
480 | + " to apply on component location and dimension: " |
481 | + stringTools.sourced(getProperty(propertyName)), error); |
482 | } |
483 | } |
484 | } |
485 | |
486 | /** |
487 | * Reset all settings to their default value. |
488 | */ |
489 | public void clear() { |
490 | if (logger.isInfoEnabled()) { |
491 | logger.info("reset settings to default values"); |
492 | } |
493 | super.clear(); |
494 | } |
495 | |
496 | /** |
497 | * Remove the property <code>key</code>. This either resets it to the internal default, or the |
498 | * value optionally specified in the corresponding system property. |
499 | */ |
500 | //@ requires isValidPropertyName(key); |
501 | public void remove(String key) { |
502 | if (logger.isDebugEnabled()) { |
503 | logger.debug("remove property " + key); |
504 | } |
505 | super.remove(key); |
506 | } |
507 | |
508 | public void removePropertyChangeListener(PropertyChangeListener listener) { |
509 | changes.removePropertyChangeListener(listener); |
510 | } |
511 | |
512 | //@ requires isValidPropertyName(propertyName); |
513 | public void removePropertyChangeListener(String propertyName, PropertyChangeListener listener) { |
514 | changes.removePropertyChangeListener(propertyName, listener); |
515 | } |
516 | |
517 | /** |
518 | * <code>True</code> if <code>propertyName</code> is valid. Invalid names cause an error |
519 | * message to be logged that explains why the name was rejected. |
520 | */ |
521 | protected /*@ spec_public pure @*/ boolean isValidPropertyName(/*@ nullable @*/ String propertyName) { |
522 | boolean result = true; |
523 | |
524 | if (propertyName == null) { |
525 | logger.error("propertyName is null"); |
526 | result = false; |
527 | } else if (propertyName.length() == 0) { |
528 | logger.error("propertyName is empty"); |
529 | result = false; |
530 | } else if (!propertyName.trim().equals(propertyName)) { |
531 | logger.error("propertyName contains leading or trailing white space: \"" + propertyName + "\""); |
532 | result = false; |
533 | } |
534 | return result; |
535 | } |
536 | /** |
537 | * Notify all listeners that have registered interest for notification on this event type. The |
538 | * event instance is lazily created using the parameters passed into the fire method. |
539 | */ |
540 | //@ requires isValidPropertyName(propertyName); |
541 | protected void firePropertyChangeEvent(String propertyName, /*@ nullable @*/ Object oldValue, |
542 | /*@ nullable @*/ Object newValue) { |
543 | changes.firePropertyChange(propertyName, oldValue, newValue); |
544 | } |
545 | } |