1 | // License: GPL. For details, see LICENSE file.
|
---|
2 | package org.openstreetmap.josm.gui.widgets;
|
---|
3 |
|
---|
4 | import java.awt.Component;
|
---|
5 | import java.awt.Dimension;
|
---|
6 | import java.awt.GridBagLayout;
|
---|
7 | import java.text.DateFormat;
|
---|
8 | import java.text.SimpleDateFormat;
|
---|
9 | import java.util.ArrayList;
|
---|
10 | import java.util.Date;
|
---|
11 | import java.util.List;
|
---|
12 |
|
---|
13 | import javax.swing.JLabel;
|
---|
14 | import javax.swing.JPanel;
|
---|
15 | import javax.swing.JSlider;
|
---|
16 | import javax.swing.JSpinner;
|
---|
17 | import javax.swing.SpinnerDateModel;
|
---|
18 | import javax.swing.event.ChangeEvent;
|
---|
19 | import javax.swing.event.ChangeListener;
|
---|
20 |
|
---|
21 | import org.openstreetmap.josm.tools.GBC;
|
---|
22 | import org.openstreetmap.josm.tools.date.DateUtils;
|
---|
23 |
|
---|
24 | /**
|
---|
25 | * Widget originally created for date filtering of GPX tracks.
|
---|
26 | * Allows to enter the date or choose it by using slider
|
---|
27 | * @since 5815
|
---|
28 | */
|
---|
29 | public class DateEditorWithSlider extends JPanel {
|
---|
30 | private final JSpinner spinner;
|
---|
31 | private final JSlider slider;
|
---|
32 | private Date dateMin;
|
---|
33 | private Date dateMax;
|
---|
34 | private static final int MAX_SLIDER = 300;
|
---|
35 | private boolean watchSlider = true;
|
---|
36 |
|
---|
37 | private final transient List<ChangeListener> listeners = new ArrayList<>();
|
---|
38 |
|
---|
39 | /**
|
---|
40 | * Constructs a new {@code DateEditorWithSlider} with a given label
|
---|
41 | * @param labelText The label to display
|
---|
42 | */
|
---|
43 | public DateEditorWithSlider(String labelText) {
|
---|
44 | super(new GridBagLayout());
|
---|
45 | spinner = new JSpinner(new SpinnerDateModel());
|
---|
46 | String pattern = ((SimpleDateFormat) DateUtils.getDateFormat(DateFormat.DEFAULT)).toPattern();
|
---|
47 | JSpinner.DateEditor timeEditor = new JSpinner.DateEditor(spinner, pattern);
|
---|
48 | spinner.setEditor(timeEditor);
|
---|
49 |
|
---|
50 | spinner.setPreferredSize(new Dimension(spinner.getPreferredSize().width+5,
|
---|
51 | spinner.getPreferredSize().height));
|
---|
52 |
|
---|
53 | slider = new JSlider(0, MAX_SLIDER);
|
---|
54 | spinner.addChangeListener(new ChangeListener() {
|
---|
55 | @Override
|
---|
56 | public void stateChanged(ChangeEvent e) {
|
---|
57 | int i = slider.getValue();
|
---|
58 | Date d = (Date) spinner.getValue();
|
---|
59 | int j = intFromDate(d);
|
---|
60 | if (i != j) {
|
---|
61 | watchSlider = false;
|
---|
62 | slider.setValue(j);
|
---|
63 | watchSlider = true;
|
---|
64 | }
|
---|
65 | for (ChangeListener l : listeners) {
|
---|
66 | l.stateChanged(e);
|
---|
67 | }
|
---|
68 | }
|
---|
69 | });
|
---|
70 | slider.addChangeListener(new ChangeListener() {
|
---|
71 | @Override
|
---|
72 | public void stateChanged(ChangeEvent e) {
|
---|
73 | if (!watchSlider) return;
|
---|
74 | Date d = (Date) spinner.getValue();
|
---|
75 | Date d1 = dateFromInt(slider.getValue());
|
---|
76 | if (!d.equals(d1)) {
|
---|
77 | spinner.setValue(d1);
|
---|
78 | }
|
---|
79 | }
|
---|
80 | });
|
---|
81 | add(new JLabel(labelText), GBC.std());
|
---|
82 | add(spinner, GBC.std().insets(10, 0, 0, 0));
|
---|
83 | add(slider, GBC.eol().insets(10, 0, 0, 0).fill(GBC.HORIZONTAL));
|
---|
84 |
|
---|
85 | dateMin = new Date(0);
|
---|
86 | dateMax = new Date();
|
---|
87 | }
|
---|
88 |
|
---|
89 | protected Date dateFromInt(int value) {
|
---|
90 | double k = 1.0*value/MAX_SLIDER;
|
---|
91 | return new Date((long) (dateMax.getTime()*k+ dateMin.getTime()*(1-k)));
|
---|
92 | }
|
---|
93 |
|
---|
94 | protected int intFromDate(Date date) {
|
---|
95 | return (int) (300.0*(date.getTime()-dateMin.getTime()) /
|
---|
96 | (dateMax.getTime()-dateMin.getTime()));
|
---|
97 | }
|
---|
98 |
|
---|
99 | public void setRange(Date dateMin, Date dateMax) {
|
---|
100 | this.dateMin = dateMin;
|
---|
101 | this.dateMax = dateMax;
|
---|
102 | }
|
---|
103 |
|
---|
104 | public void setDate(Date date) {
|
---|
105 | spinner.setValue(date);
|
---|
106 | }
|
---|
107 |
|
---|
108 | public Date getDate() {
|
---|
109 | return (Date) spinner.getValue();
|
---|
110 | }
|
---|
111 |
|
---|
112 | public void addDateListener(ChangeListener l) {
|
---|
113 | listeners.add(l);
|
---|
114 | }
|
---|
115 |
|
---|
116 | public void removeDateListener(ChangeListener l) {
|
---|
117 | listeners.remove(l);
|
---|
118 | }
|
---|
119 |
|
---|
120 | @Override
|
---|
121 | public void setEnabled(boolean enabled) {
|
---|
122 | super.setEnabled(enabled);
|
---|
123 | for (Component c: getComponents()) {
|
---|
124 | c.setEnabled(enabled);
|
---|
125 | }
|
---|
126 | }
|
---|
127 | }
|
---|