001: /*
002: * GutterOptionPane.java - Gutter options panel
003: * :tabSize=8:indentSize=8:noTabs=false:
004: * :folding=explicit:collapseFolds=1:
005: *
006: * Copyright (C) 2000 mike dillon
007: * Portions copyright (C) 2001, 2002 Slava Pestov
008: *
009: * This program is free software; you can redistribute it and/or
010: * modify it under the terms of the GNU General Public License
011: * as published by the Free Software Foundation; either version 2
012: * of the License, or any later version.
013: *
014: * This program is distributed in the hope that it will be useful,
015: * but WITHOUT ANY WARRANTY; without even the implied warranty of
016: * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
017: * GNU General Public License for more details.
018: *
019: * You should have received a copy of the GNU General Public License
020: * along with this program; if not, write to the Free Software
021: * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
022: */
023:
024: package org.gjt.sp.jedit.options;
025:
026: //{{{ Imports
027: import javax.swing.*;
028: import java.awt.*;
029: import org.gjt.sp.jedit.gui.*;
030: import org.gjt.sp.jedit.*;
031:
032: //}}}
033:
034: public class GutterOptionPane extends AbstractOptionPane {
035: //{{{ GutterOptionPane constructor
036: public GutterOptionPane() {
037: super ("gutter");
038: } //}}}
039:
040: //{{{ _init() method
041: public void _init() {
042: /* Line numbering */
043: lineNumbersEnabled = new JCheckBox(jEdit
044: .getProperty("options.gutter.lineNumbers"));
045: lineNumbersEnabled.setSelected(jEdit
046: .getBooleanProperty("view.gutter.lineNumbers"));
047: addComponent(lineNumbersEnabled);
048:
049: /* Text font */
050: gutterFont = new FontSelector(jEdit.getFontProperty(
051: "view.gutter.font", new Font("Monospaced", Font.PLAIN,
052: 10)));
053:
054: addComponent(jEdit.getProperty("options.gutter.font"),
055: gutterFont);
056:
057: /* Text color */
058: addComponent(jEdit.getProperty("options.gutter.foreground"),
059: gutterForeground = new ColorWellButton(jEdit
060: .getColorProperty("view.gutter.fgColor")),
061: GridBagConstraints.VERTICAL);
062:
063: /* Background color */
064: addComponent(jEdit.getProperty("options.gutter.background"),
065: gutterBackground = new ColorWellButton(jEdit
066: .getColorProperty("view.gutter.bgColor")),
067: GridBagConstraints.VERTICAL);
068:
069: /* Border width */
070: /* gutterBorderWidth = new JTextField(jEdit.getProperty(
071: "view.gutter.borderWidth"));
072: addComponent(jEdit.getProperty("options.gutter.borderWidth"),
073: gutterBorderWidth); */
074:
075: /* Number alignment */
076: /* String[] alignments = new String[] {
077: "Left", "Center", "Right"
078: };
079: gutterNumberAlignment = new JComboBox(alignments);
080: String alignment = jEdit.getProperty("view.gutter.numberAlignment");
081: if("right".equals(alignment))
082: gutterNumberAlignment.setSelectedIndex(2);
083: else if("center".equals(alignment))
084: gutterNumberAlignment.setSelectedIndex(1);
085: else
086: gutterNumberAlignment.setSelectedIndex(0);
087: addComponent(jEdit.getProperty("options.gutter.numberAlignment"),
088: gutterNumberAlignment); */
089:
090: /* Current line highlight */
091: gutterCurrentLineHighlightEnabled = new JCheckBox(jEdit
092: .getProperty("options.gutter.currentLineHighlight"));
093: gutterCurrentLineHighlightEnabled
094: .setSelected(jEdit
095: .getBooleanProperty("view.gutter.highlightCurrentLine"));
096: addComponent(
097: gutterCurrentLineHighlightEnabled,
098: gutterCurrentLineHighlight = new ColorWellButton(
099: jEdit
100: .getColorProperty("view.gutter.currentLineColor")),
101: GridBagConstraints.VERTICAL);
102:
103: /* Highlight interval and color */
104: gutterHighlightInterval = new JTextField(jEdit
105: .getProperty("view.gutter.highlightInterval"), 3);
106:
107: Box gutterHighlightBox = new Box(BoxLayout.X_AXIS);
108: gutterHighlightBox.add(new JLabel(jEdit
109: .getProperty("options.gutter.interval-1")));
110: gutterHighlightBox.add(Box.createHorizontalStrut(3));
111: gutterHighlightBox.add(gutterHighlightInterval);
112: gutterHighlightBox.add(Box.createHorizontalStrut(3));
113: gutterHighlightBox.add(new JLabel(jEdit
114: .getProperty("options.gutter.interval-2")));
115: gutterHighlightBox.add(Box.createHorizontalStrut(12));
116:
117: addComponent(
118: gutterHighlightBox,
119: gutterHighlightColor = new ColorWellButton(jEdit
120: .getColorProperty("view.gutter.highlightColor")),
121: GridBagConstraints.VERTICAL);
122:
123: /* Structure highlight */
124: gutterStructureHighlightEnabled = new JCheckBox(jEdit
125: .getProperty("options.gutter.structureHighlight"));
126: gutterStructureHighlightEnabled.setSelected(jEdit
127: .getBooleanProperty("view.gutter.structureHighlight"));
128: addComponent(
129: gutterStructureHighlightEnabled,
130: gutterStructureHighlight = new ColorWellButton(
131: jEdit
132: .getColorProperty("view.gutter.structureHighlightColor")),
133: GridBagConstraints.VERTICAL);
134:
135: /* Marker highlight */
136: gutterMarkerHighlightEnabled = new JCheckBox(jEdit
137: .getProperty("options.gutter.markerHighlight"));
138: gutterMarkerHighlightEnabled.setSelected(jEdit
139: .getBooleanProperty("view.gutter.markerHighlight"));
140: addComponent(gutterMarkerHighlightEnabled,
141: gutterMarkerHighlight = new ColorWellButton(jEdit
142: .getColorProperty("view.gutter.markerColor")),
143: GridBagConstraints.VERTICAL);
144:
145: /* Fold marker color */
146: addComponent(jEdit.getProperty("options.gutter.foldColor"),
147: gutterFoldMarkers = new ColorWellButton(jEdit
148: .getColorProperty("view.gutter.foldColor")),
149: GridBagConstraints.VERTICAL);
150:
151: /* Focused border color */
152: addComponent(
153: jEdit.getProperty("options.gutter.focusBorderColor"),
154: gutterFocusBorder = new ColorWellButton(
155: jEdit
156: .getColorProperty("view.gutter.focusBorderColor")),
157: GridBagConstraints.VERTICAL);
158:
159: /* unfocused border color */
160: addComponent(
161: jEdit.getProperty("options.gutter.noFocusBorderColor"),
162: gutterNoFocusBorder = new ColorWellButton(
163: jEdit
164: .getColorProperty("view.gutter.noFocusBorderColor")),
165: GridBagConstraints.VERTICAL);
166: } //}}}
167:
168: //{{{ _save() method
169: public void _save() {
170: jEdit.setBooleanProperty("view.gutter.lineNumbers",
171: lineNumbersEnabled.isSelected());
172:
173: jEdit.setFontProperty("view.gutter.font", gutterFont.getFont());
174: jEdit.setColorProperty("view.gutter.fgColor", gutterForeground
175: .getSelectedColor());
176: jEdit.setColorProperty("view.gutter.bgColor", gutterBackground
177: .getSelectedColor());
178:
179: /* jEdit.setProperty("view.gutter.borderWidth",
180: gutterBorderWidth.getText());
181:
182: String alignment = null;
183: switch(gutterNumberAlignment.getSelectedIndex())
184: {
185: case 2:
186: alignment = "right";
187: break;
188: case 1:
189: alignment = "center";
190: break;
191: case 0: default:
192: alignment = "left";
193: }
194: jEdit.setProperty("view.gutter.numberAlignment", alignment); */
195:
196: jEdit.setBooleanProperty("view.gutter.highlightCurrentLine",
197: gutterCurrentLineHighlightEnabled.isSelected());
198: jEdit.setColorProperty("view.gutter.currentLineColor",
199: gutterCurrentLineHighlight.getSelectedColor());
200: jEdit.setProperty("view.gutter.highlightInterval",
201: gutterHighlightInterval.getText());
202: jEdit.setColorProperty("view.gutter.highlightColor",
203: gutterHighlightColor.getSelectedColor());
204:
205: jEdit.setBooleanProperty("view.gutter.structureHighlight",
206: gutterStructureHighlightEnabled.isSelected());
207: jEdit.setColorProperty("view.gutter.structureHighlightColor",
208: gutterStructureHighlight.getSelectedColor());
209: jEdit.setBooleanProperty("view.gutter.markerHighlight",
210: gutterMarkerHighlightEnabled.isSelected());
211: jEdit.setColorProperty("view.gutter.markerColor",
212: gutterMarkerHighlight.getSelectedColor());
213: jEdit.setColorProperty("view.gutter.foldColor",
214: gutterFoldMarkers.getSelectedColor());
215: jEdit.setColorProperty("view.gutter.focusBorderColor",
216: gutterFocusBorder.getSelectedColor());
217: jEdit.setColorProperty("view.gutter.noFocusBorderColor",
218: gutterNoFocusBorder.getSelectedColor());
219: } //}}}
220:
221: //{{{ Private members
222: private FontSelector gutterFont;
223: private ColorWellButton gutterForeground;
224: private ColorWellButton gutterBackground;
225: private JTextField gutterHighlightInterval;
226: private ColorWellButton gutterHighlightColor;
227: private JCheckBox lineNumbersEnabled;
228: private JCheckBox gutterCurrentLineHighlightEnabled;
229: private ColorWellButton gutterCurrentLineHighlight;
230: private JCheckBox gutterStructureHighlightEnabled;
231: private ColorWellButton gutterStructureHighlight;
232: private JCheckBox gutterMarkerHighlightEnabled;
233: private ColorWellButton gutterMarkerHighlight;
234: private ColorWellButton gutterFoldMarkers;
235: private ColorWellButton gutterFocusBorder;
236: private ColorWellButton gutterNoFocusBorder;
237: //}}}
238: }
|