1 33 34 package edu.rice.cs.drjava.ui.config; 35 36 import javax.swing.*; 37 import edu.rice.cs.drjava.config.*; 38 import edu.rice.cs.drjava.*; 39 import edu.rice.cs.util.swing.FontChooser; 40 41 import java.awt.*; 42 import java.awt.event.*; 43 44 48 public class FontOptionComponent extends OptionComponent<Font> { 49 50 private JButton _button; 51 private JTextField _fontField; 52 private JPanel _panel; 53 private Font _font; 54 55 public FontOptionComponent(FontOption opt, String text, Frame parent) { 56 super(opt, text, parent); 57 _button = new JButton(); 58 _button.addActionListener(new ActionListener() { 59 public void actionPerformed(ActionEvent e) { 60 chooseFont(); 61 } 62 }); 63 _button.setText("..."); 64 _button.setMaximumSize(new Dimension(10,10)); 65 _button.setMinimumSize(new Dimension(10,10)); 66 67 _fontField = new JTextField(); 68 _fontField.setEditable(false); 69 _fontField.setBackground(Color.white); 70 _fontField.setHorizontalAlignment(JTextField.CENTER); 71 _panel = new JPanel(new BorderLayout()); 72 _panel.add(_fontField, BorderLayout.CENTER); 73 _panel.add(_button, BorderLayout.EAST); 74 75 _font = DrJava.getConfig().getSetting(_option); 76 _updateField(_font); 77 } 78 79 82 public FontOptionComponent(FontOption opt, String text, 83 Frame parent, String description) { 84 this(opt, text, parent); 85 setDescription(description); 86 } 87 88 92 public void setDescription(String description) { 93 _panel.setToolTipText(description); 94 _fontField.setToolTipText(description); 95 _label.setToolTipText(description); 96 } 97 98 101 private void _updateField(Font f) { 102 _fontField.setFont(f); 103 _fontField.setText(_option.format(f)); 104 } 105 106 109 public JComponent getComponent() { 110 return _panel; 111 } 112 113 116 public void chooseFont() { 117 String oldText = _fontField.getText(); 118 Font f = FontChooser.showDialog(_parent, 119 "Choose '" + getLabelText() + "'", 120 _font); 121 if (f != null) { 122 _font = f; 123 _updateField(_font); 124 if (!oldText.equals(_fontField.getText())) { 125 notifyChangeListeners(); 126 } 127 } 128 } 129 130 134 public boolean updateConfig() { 135 if (!_font.equals(DrJava.getConfig().getSetting(_option))) { 136 DrJava.getConfig().setSetting(_option, _font); 137 } 138 return true; 139 } 140 141 144 public void setValue(Font value) { 145 _font = value; 146 _updateField(value); 147 } 148 } | Popular Tags |