34
|
1 /*******************************************************************************
|
|
2 * Copyright (c) 2003, 2006 IBM Corporation and others.
|
|
3 * All rights reserved. This program and the accompanying materials
|
|
4 * are made available under the terms of the Eclipse Public License v1.0
|
|
5 * which accompanies this distribution, and is available at
|
|
6 * http://www.eclipse.org/legal/epl-v10.html
|
|
7 *
|
|
8 * Contributors:
|
|
9 * IBM Corporation - initial API and implementation
|
|
10 * Port to the D programming language:
|
|
11 * Frank Benoit <benoit@tionex.de>
|
|
12 *******************************************************************************/
|
|
13 module dwtx.jface.preference.ScaleFieldEditor;
|
|
14
|
|
15 import dwtx.jface.preference.FieldEditor;
|
|
16
|
|
17 import dwt.DWT;
|
|
18 import dwt.events.DisposeEvent;
|
|
19 import dwt.events.DisposeListener;
|
|
20 import dwt.events.SelectionAdapter;
|
|
21 import dwt.events.SelectionEvent;
|
|
22 import dwt.layout.GridData;
|
|
23 import dwt.widgets.Composite;
|
|
24 import dwt.widgets.Control;
|
|
25 import dwt.widgets.Scale;
|
|
26
|
|
27 import dwt.dwthelper.utils;
|
|
28
|
|
29 /**
|
|
30 * A field editor for an integer type preference. This class may be used as is,
|
|
31 * or subclassed as required.
|
|
32 *
|
|
33 * @since 3.0
|
|
34 */
|
|
35 public class ScaleFieldEditor : FieldEditor {
|
|
36
|
|
37 /**
|
|
38 * Value that will feed Scale.setIncrement(int).
|
|
39 */
|
|
40 private int incrementValue;
|
|
41
|
|
42 /**
|
|
43 * Value that will feed Scale.setMaximum(int).
|
|
44 */
|
|
45 private int maxValue;
|
|
46
|
|
47 /**
|
|
48 * Value that will feed Scale.setMinimum(int).
|
|
49 */
|
|
50 private int minValue;
|
|
51
|
|
52 /**
|
|
53 * Old integer value.
|
|
54 */
|
|
55 private int oldValue;
|
|
56
|
|
57 /**
|
|
58 * Value that will feed Scale.setPageIncrement(int).
|
|
59 */
|
|
60 private int pageIncrementValue;
|
|
61
|
|
62 /**
|
|
63 * The scale, or <code>null</code> if none.
|
|
64 */
|
|
65 protected Scale scale;
|
|
66
|
|
67 /**
|
|
68 * Creates a scale field editor.
|
|
69 *
|
|
70 * @param name
|
|
71 * the name of the preference this field editor works on
|
|
72 * @param labelText
|
|
73 * the label text of the field editor
|
|
74 * @param parent
|
|
75 * the parent of the field editor's control
|
|
76 */
|
|
77 public this(String name, String labelText, Composite parent) {
|
|
78 super(name, labelText, parent);
|
|
79 setDefaultValues();
|
|
80 }
|
|
81
|
|
82 /**
|
|
83 * Creates a scale field editor with particular scale values.
|
|
84 *
|
|
85 * @param name
|
|
86 * the name of the preference this field editor works on
|
|
87 * @param labelText
|
|
88 * the label text of the field editor
|
|
89 * @param parent
|
|
90 * the parent of the field editor's control
|
|
91 * @param min
|
|
92 * the value used for Scale.setMinimum(int).
|
|
93 * @param max
|
|
94 * the value used for Scale.setMaximum(int).
|
|
95 * @param increment
|
|
96 * the value used for Scale.setIncrement(int).
|
|
97 * @param pageIncrement
|
|
98 * the value used for Scale.setPageIncrement(int).
|
|
99 */
|
|
100 public this(String name, String labelText, Composite parent,
|
|
101 int min, int max, int increment, int pageIncrement) {
|
|
102 super(name, labelText, parent);
|
|
103 setValues(min, max, increment, pageIncrement);
|
|
104 }
|
|
105
|
|
106 /*
|
|
107 * (non-Javadoc)
|
|
108 *
|
|
109 * @see dwtx.jface.preference.FieldEditor#adjustForNumColumns(int)
|
|
110 */
|
|
111 protected void adjustForNumColumns(int numColumns) {
|
|
112 (cast(GridData) scale.getLayoutData()).horizontalSpan = numColumns - 1;
|
|
113 }
|
|
114
|
|
115 /*
|
|
116 * (non-Javadoc)
|
|
117 *
|
|
118 * @see dwtx.jface.preference.FieldEditor#doFillIntoGrid(dwt.widgets.Composite,
|
|
119 * int)
|
|
120 */
|
|
121 protected void doFillIntoGrid(Composite parent, int numColumns) {
|
|
122 Control control = getLabelControl(parent);
|
|
123 GridData gd = new GridData();
|
|
124 control.setLayoutData(gd);
|
|
125
|
|
126 scale = getScaleControl(parent);
|
|
127 gd = new GridData(GridData.FILL_HORIZONTAL);
|
|
128 gd.verticalAlignment = GridData.FILL;
|
|
129 gd.horizontalSpan = numColumns - 1;
|
|
130 gd.grabExcessHorizontalSpace = true;
|
|
131 scale.setLayoutData(gd);
|
|
132 updateScale();
|
|
133 }
|
|
134
|
|
135 /*
|
|
136 * (non-Javadoc)
|
|
137 *
|
|
138 * @see dwtx.jface.preference.FieldEditor#doLoad()
|
|
139 */
|
|
140 protected void doLoad() {
|
|
141 if (scale !is null) {
|
|
142 int value = getPreferenceStore().getInt(getPreferenceName());
|
|
143 scale.setSelection(value);
|
|
144 oldValue = value;
|
|
145 }
|
|
146 }
|
|
147
|
|
148 /*
|
|
149 * (non-Javadoc)
|
|
150 *
|
|
151 * @see dwtx.jface.preference.FieldEditor#doLoadDefault()
|
|
152 */
|
|
153 protected void doLoadDefault() {
|
|
154 if (scale !is null) {
|
|
155 int value = getPreferenceStore().getDefaultInt(getPreferenceName());
|
|
156 scale.setSelection(value);
|
|
157 }
|
|
158 valueChanged();
|
|
159 }
|
|
160
|
|
161 /*
|
|
162 * (non-Javadoc)
|
|
163 *
|
|
164 * @see dwtx.jface.preference.FieldEditor#doStore()
|
|
165 */
|
|
166 protected void doStore() {
|
|
167 getPreferenceStore()
|
|
168 .setValue(getPreferenceName(), scale.getSelection());
|
|
169 }
|
|
170
|
|
171 /**
|
|
172 * Returns the value that will be used for Scale.setIncrement(int).
|
|
173 *
|
|
174 * @return the value.
|
|
175 * @see dwt.widgets.Scale#setIncrement(int)
|
|
176 */
|
|
177 public int getIncrement() {
|
|
178 return incrementValue;
|
|
179 }
|
|
180
|
|
181 /**
|
|
182 * Returns the value that will be used for Scale.setMaximum(int).
|
|
183 *
|
|
184 * @return the value.
|
|
185 * @see dwt.widgets.Scale#setMaximum(int)
|
|
186 */
|
|
187 public int getMaximum() {
|
|
188 return maxValue;
|
|
189 }
|
|
190
|
|
191 /**
|
|
192 * Returns the value that will be used for Scale.setMinimum(int).
|
|
193 *
|
|
194 * @return the value.
|
|
195 * @see dwt.widgets.Scale#setMinimum(int)
|
|
196 */
|
|
197 public int getMinimum() {
|
|
198 return minValue;
|
|
199 }
|
|
200
|
|
201 /*
|
|
202 * (non-Javadoc)
|
|
203 *
|
|
204 * @see dwtx.jface.preference.FieldEditor#getNumberOfControls()
|
|
205 */
|
|
206 public int getNumberOfControls() {
|
|
207 return 2;
|
|
208 }
|
|
209
|
|
210 /**
|
|
211 * Returns the value that will be used for Scale.setPageIncrement(int).
|
|
212 *
|
|
213 * @return the value.
|
|
214 * @see dwt.widgets.Scale#setPageIncrement(int)
|
|
215 */
|
|
216 public int getPageIncrement() {
|
|
217 return pageIncrementValue;
|
|
218 }
|
|
219
|
|
220 /**
|
|
221 * Returns this field editor's scale control.
|
|
222 *
|
|
223 * @return the scale control, or <code>null</code> if no scale field is
|
|
224 * created yet
|
|
225 */
|
|
226 public Scale getScaleControl() {
|
|
227 return scale;
|
|
228 }
|
|
229
|
|
230 /**
|
|
231 * Returns this field editor's scale control. The control is created if it
|
|
232 * does not yet exist.
|
|
233 *
|
|
234 * @param parent
|
|
235 * the parent
|
|
236 * @return the scale control
|
|
237 */
|
|
238 private Scale getScaleControl(Composite parent) {
|
|
239 if (scale is null) {
|
|
240 scale = new Scale(parent, DWT.HORIZONTAL);
|
|
241 scale.setFont(parent.getFont());
|
|
242 scale.addSelectionListener(new class SelectionAdapter {
|
|
243 public void widgetSelected(SelectionEvent event) {
|
|
244 valueChanged();
|
|
245 }
|
|
246 });
|
|
247 scale.addDisposeListener(new class DisposeListener {
|
|
248 public void widgetDisposed(DisposeEvent event) {
|
|
249 scale = null;
|
|
250 }
|
|
251 });
|
|
252 } else {
|
|
253 checkParent(scale, parent);
|
|
254 }
|
|
255 return scale;
|
|
256 }
|
|
257
|
|
258 /**
|
|
259 * Set default values for the various scale fields. These defaults are:<br>
|
|
260 * <ul>
|
|
261 * <li>Minimum = 0
|
|
262 * <li>Maximim = 10
|
|
263 * <li>Increment = 1
|
|
264 * <li>Page Increment = 1
|
|
265 * </ul>
|
|
266 */
|
|
267 private void setDefaultValues() {
|
|
268 setValues(0, 10, 1, 1);
|
|
269 }
|
|
270
|
|
271 /*
|
|
272 * (non-Javadoc)
|
|
273 *
|
|
274 * @see dwtx.jface.preference.FieldEditor#setFocus()
|
|
275 */
|
|
276 public void setFocus() {
|
|
277 if (scale !is null && !scale.isDisposed()) {
|
|
278 scale.setFocus();
|
|
279 }
|
|
280 }
|
|
281
|
|
282 /**
|
|
283 * Set the value to be used for Scale.setIncrement(int) and update the
|
|
284 * scale.
|
|
285 *
|
|
286 * @param increment
|
|
287 * a value greater than 0.
|
|
288 * @see dwt.widgets.Scale#setIncrement(int)
|
|
289 */
|
|
290 public void setIncrement(int increment) {
|
|
291 this.incrementValue = increment;
|
|
292 updateScale();
|
|
293 }
|
|
294
|
|
295 /**
|
|
296 * Set the value to be used for Scale.setMaximum(int) and update the
|
|
297 * scale.
|
|
298 *
|
|
299 * @param max
|
|
300 * a value greater than 0.
|
|
301 * @see dwt.widgets.Scale#setMaximum(int)
|
|
302 */
|
|
303 public void setMaximum(int max) {
|
|
304 this.maxValue = max;
|
|
305 updateScale();
|
|
306 }
|
|
307
|
|
308 /**
|
|
309 * Set the value to be used for Scale.setMinumum(int) and update the
|
|
310 * scale.
|
|
311 *
|
|
312 * @param min
|
|
313 * a value greater than 0.
|
|
314 * @see dwt.widgets.Scale#setMinimum(int)
|
|
315 */
|
|
316 public void setMinimum(int min) {
|
|
317 this.minValue = min;
|
|
318 updateScale();
|
|
319 }
|
|
320
|
|
321 /**
|
|
322 * Set the value to be used for Scale.setPageIncrement(int) and update the
|
|
323 * scale.
|
|
324 *
|
|
325 * @param pageIncrement
|
|
326 * a value greater than 0.
|
|
327 * @see dwt.widgets.Scale#setPageIncrement(int)
|
|
328 */
|
|
329 public void setPageIncrement(int pageIncrement) {
|
|
330 this.pageIncrementValue = pageIncrement;
|
|
331 updateScale();
|
|
332 }
|
|
333
|
|
334 /**
|
|
335 * Set all Scale values.
|
|
336 *
|
|
337 * @param min
|
|
338 * the value used for Scale.setMinimum(int).
|
|
339 * @param max
|
|
340 * the value used for Scale.setMaximum(int).
|
|
341 * @param increment
|
|
342 * the value used for Scale.setIncrement(int).
|
|
343 * @param pageIncrement
|
|
344 * the value used for Scale.setPageIncrement(int).
|
|
345 */
|
|
346 private void setValues(int min, int max, int increment, int pageIncrement) {
|
|
347 this.incrementValue = increment;
|
|
348 this.maxValue = max;
|
|
349 this.minValue = min;
|
|
350 this.pageIncrementValue = pageIncrement;
|
|
351 updateScale();
|
|
352 }
|
|
353
|
|
354 /**
|
|
355 * Update the scale particulars with set values.
|
|
356 */
|
|
357 private void updateScale() {
|
|
358 if (scale !is null && !scale.isDisposed()) {
|
|
359 scale.setMinimum(getMinimum());
|
|
360 scale.setMaximum(getMaximum());
|
|
361 scale.setIncrement(getIncrement());
|
|
362 scale.setPageIncrement(getPageIncrement());
|
|
363 }
|
|
364 }
|
|
365
|
|
366 /**
|
|
367 * Informs this field editor's listener, if it has one, about a change to
|
|
368 * the value (<code>VALUE</code> property) provided that the old and new
|
|
369 * values are different.
|
|
370 * <p>
|
|
371 * This hook is <em>not</em> called when the scale is initialized (or
|
|
372 * reset to the default value) from the preference store.
|
|
373 * </p>
|
|
374 */
|
|
375 protected void valueChanged() {
|
|
376 setPresentsDefaultValue(false);
|
|
377
|
|
378 int newValue = scale.getSelection();
|
|
379 if (newValue !is oldValue) {
|
|
380 fireStateChanged(IS_VALID, false, true);
|
|
381 fireValueChanged(VALUE, new ValueWrapperInt(oldValue),
|
|
382 new ValueWrapperInt(newValue));
|
|
383 oldValue = newValue;
|
|
384 }
|
|
385 }
|
|
386 }
|