|
1 |
| |
|
2 |
| |
|
3 |
| |
|
4 |
| |
|
5 |
| |
|
6 |
| |
|
7 |
| |
|
8 |
| |
|
9 |
| |
|
10 |
| |
|
11 |
| |
|
12 |
| |
|
13 |
| |
|
14 |
| |
|
15 |
| |
|
16 |
| |
|
17 |
| |
|
18 |
| |
|
19 |
| |
|
20 |
| |
|
21 |
| |
|
22 |
| |
|
23 |
| |
|
24 |
| |
|
25 |
| |
|
26 |
| |
|
27 |
| |
|
28 |
| |
|
29 |
| |
|
30 |
| |
|
31 |
| |
|
32 |
| |
|
33 |
| |
|
34 |
| |
|
35 |
| |
|
36 |
| |
|
37 |
| package edu.rice.cs.drjava.ui.config; |
|
38 |
| |
|
39 |
| import javax.swing.*; |
|
40 |
| import edu.rice.cs.drjava.config.*; |
|
41 |
| import edu.rice.cs.drjava.*; |
|
42 |
| import edu.rice.cs.util.swing.FontChooser; |
|
43 |
| import edu.rice.cs.util.swing.SwingFrame; |
|
44 |
| |
|
45 |
| import java.awt.*; |
|
46 |
| import java.awt.event.*; |
|
47 |
| |
|
48 |
| |
|
49 |
| |
|
50 |
| |
|
51 |
| public class FontOptionComponent extends OptionComponent<Font,JPanel> { |
|
52 |
| |
|
53 |
| private final JButton _button; |
|
54 |
| private final JTextField _fontField; |
|
55 |
| private final JPanel _panel; |
|
56 |
| private volatile Font _font; |
|
57 |
| |
|
58 |
155
| public FontOptionComponent(FontOption opt, String text, SwingFrame parent) {
|
|
59 |
155
| super(opt, text, parent);
|
|
60 |
155
| _button = new JButton();
|
|
61 |
155
| _button.addActionListener(new ActionListener() {
|
|
62 |
0
| public void actionPerformed(ActionEvent e) { chooseFont(); }
|
|
63 |
| }); |
|
64 |
155
| _button.setText("...");
|
|
65 |
155
| _button.setMaximumSize(new Dimension(10,10));
|
|
66 |
155
| _button.setMinimumSize(new Dimension(10,10));
|
|
67 |
| |
|
68 |
155
| _fontField = new JTextField();
|
|
69 |
155
| _fontField.setEditable(false);
|
|
70 |
155
| _fontField.setBackground(Color.white);
|
|
71 |
155
| _fontField.setHorizontalAlignment(JTextField.CENTER);
|
|
72 |
155
| _panel = new JPanel(new BorderLayout());
|
|
73 |
155
| _panel.add(_fontField, BorderLayout.CENTER);
|
|
74 |
155
| _panel.add(_button, BorderLayout.EAST);
|
|
75 |
| |
|
76 |
155
| _font = DrJava.getConfig().getSetting(_option);
|
|
77 |
155
| _updateField(_font);
|
|
78 |
155
| setComponent(_panel);
|
|
79 |
| } |
|
80 |
| |
|
81 |
| |
|
82 |
152
| public FontOptionComponent(FontOption opt, String text, SwingFrame parent, String description) {
|
|
83 |
152
| this(opt, text, parent);
|
|
84 |
152
| setDescription(description);
|
|
85 |
| } |
|
86 |
| |
|
87 |
| |
|
88 |
| |
|
89 |
| |
|
90 |
152
| public void setDescription(String description) {
|
|
91 |
152
| _panel.setToolTipText(description);
|
|
92 |
152
| _fontField.setToolTipText(description);
|
|
93 |
152
| _label.setToolTipText(description);
|
|
94 |
| } |
|
95 |
| |
|
96 |
| |
|
97 |
163
| private void _updateField(Font f) {
|
|
98 |
163
| _fontField.setFont(f);
|
|
99 |
163
| _fontField.setText(_option.format(f));
|
|
100 |
| } |
|
101 |
| |
|
102 |
| |
|
103 |
0
| public void chooseFont() {
|
|
104 |
0
| String oldText = _fontField.getText();
|
|
105 |
0
| Font f = FontChooser.showDialog(_parent, "Choose '" + getLabelText() + "'", _font);
|
|
106 |
0
| if (f != null) {
|
|
107 |
0
| _font = f;
|
|
108 |
0
| _updateField(_font);
|
|
109 |
0
| if (!oldText.equals(_fontField.getText())) { notifyChangeListeners(); }
|
|
110 |
| } |
|
111 |
| } |
|
112 |
| |
|
113 |
| |
|
114 |
| |
|
115 |
| |
|
116 |
4
| public boolean updateConfig() {
|
|
117 |
3
| if (! _font.equals(DrJava.getConfig().getSetting(_option))) DrJava.getConfig().setSetting(_option, _font);
|
|
118 |
4
| return true;
|
|
119 |
| } |
|
120 |
| |
|
121 |
| |
|
122 |
8
| public void setValue(Font value) {
|
|
123 |
8
| _font = value;
|
|
124 |
8
| _updateField(value);
|
|
125 |
| } |
|
126 |
| } |