From: <sh...@us...> - 2009-08-08 15:23:20
|
Revision: 15880 http://jedit.svn.sourceforge.net/jedit/?rev=15880&view=rev Author: shlomy Date: 2009-08-08 15:23:13 +0000 (Sat, 08 Aug 2009) Log Message: ----------- Fixed #2833822: - Disable the "line numbers" and "selection area" options in the Gutter option pane when the "show gutter" option is not checked. - When "Toggle line numbers" menu is used, if the gutter is not shown, show it (otherwise the line numbers are not shown). - Added options to specify the width and background color of the selection area in the gutter. Modified Paths: -------------- jEdit/trunk/org/gjt/sp/jedit/EditPane.java jEdit/trunk/org/gjt/sp/jedit/actions.xml jEdit/trunk/org/gjt/sp/jedit/jedit.props jEdit/trunk/org/gjt/sp/jedit/jedit_gui.props jEdit/trunk/org/gjt/sp/jedit/options/GutterOptionPane.java jEdit/trunk/org/gjt/sp/jedit/textarea/Gutter.java Modified: jEdit/trunk/org/gjt/sp/jedit/EditPane.java =================================================================== --- jEdit/trunk/org/gjt/sp/jedit/EditPane.java 2009-08-08 06:15:47 UTC (rev 15879) +++ jEdit/trunk/org/gjt/sp/jedit/EditPane.java 2009-08-08 15:23:13 UTC (rev 15880) @@ -920,7 +920,7 @@ Gutter gutter = textArea.getGutter(); gutter.setGutterEnabled(GutterOptionPane.isGutterEnabled()); gutter.setMinLineNumberDigitCount(GutterOptionPane.getMinLineNumberDigits()); - gutter.setSelectonAreaEnabled(GutterOptionPane.isSelectionAreaEnabled()); + gutter.setSelectionAreaEnabled(GutterOptionPane.isSelectionAreaEnabled()); gutter.addExtension(markerHighlight); gutter.setSelectionPopupHandler( new GutterPopupHandler() @@ -1044,8 +1044,12 @@ gutter.setGutterEnabled(GutterOptionPane.isGutterEnabled()); gutter.setMinLineNumberDigitCount( GutterOptionPane.getMinLineNumberDigits()); - gutter.setSelectonAreaEnabled( + gutter.setSelectionAreaEnabled( GutterOptionPane.isSelectionAreaEnabled()); + gutter.setSelectionAreaBackground( + GutterOptionPane.getSelectionAreaBackground()); + gutter.setSelectionAreaWidth( + GutterOptionPane.getSelectionAreaWidth()); int width = jEdit.getIntegerProperty( "view.gutter.borderWidth",3); Modified: jEdit/trunk/org/gjt/sp/jedit/actions.xml =================================================================== --- jEdit/trunk/org/gjt/sp/jedit/actions.xml 2009-08-08 06:15:47 UTC (rev 15879) +++ jEdit/trunk/org/gjt/sp/jedit/actions.xml 2009-08-08 15:23:13 UTC (rev 15880) @@ -1407,8 +1407,11 @@ <ACTION NAME="toggle-line-numbers"> <CODE> - textArea.getGutter().toggleExpanded(); - jEdit.setBooleanProperty("view.gutter.lineNumbers", textArea.getGutter().isExpanded()); + boolean shown = jEdit.getBooleanProperty("view.gutter.lineNumbers"); + jEdit.setBooleanProperty("view.gutter.lineNumbers", !shown); + if (! shown) + jEdit.setBooleanProperty("view.gutter.enabled", !shown); + jEdit.propertiesChanged(); </CODE> <IS_SELECTED> return textArea.getGutter().isExpanded(); Modified: jEdit/trunk/org/gjt/sp/jedit/jedit.props =================================================================== --- jEdit/trunk/org/gjt/sp/jedit/jedit.props 2009-08-08 06:15:47 UTC (rev 15879) +++ jEdit/trunk/org/gjt/sp/jedit/jedit.props 2009-08-08 15:23:13 UTC (rev 15880) @@ -333,6 +333,8 @@ # Show selection area in gutter? view.gutter.selectionAreaEnabled=true +# Gutter selection area background color +view.gutter.selectionAreaBgColor=#dbdbdb #}}} # Expand abbrevs when space bar pressed Modified: jEdit/trunk/org/gjt/sp/jedit/jedit_gui.props =================================================================== --- jEdit/trunk/org/gjt/sp/jedit/jedit_gui.props 2009-08-08 06:15:47 UTC (rev 15879) +++ jEdit/trunk/org/gjt/sp/jedit/jedit_gui.props 2009-08-08 15:23:13 UTC (rev 15880) @@ -1897,6 +1897,8 @@ options.gutter.lineNumbers=Line numbers options.gutter.minLineNumberDigits=Minimal number of digits to reserve for line numbers: options.gutter.selectionAreaEnabled=Line selection area when line numbers are not shown +options.gutter.selectionAreaBgColor=Selection area background color: +options.gutter.selectionAreaWidth=Selection area width (in pixels): options.gutter.font=Gutter font: options.gutter.foreground=Line number color: options.gutter.background=Background color: Modified: jEdit/trunk/org/gjt/sp/jedit/options/GutterOptionPane.java =================================================================== --- jEdit/trunk/org/gjt/sp/jedit/options/GutterOptionPane.java 2009-08-08 06:15:47 UTC (rev 15879) +++ jEdit/trunk/org/gjt/sp/jedit/options/GutterOptionPane.java 2009-08-08 15:23:13 UTC (rev 15880) @@ -35,8 +35,6 @@ import org.gjt.sp.jedit.*; //}}} -import com.sun.java.swing.SwingUtilities3; - public class GutterOptionPane extends AbstractOptionPane { //{{{ GutterOptionPane constructor @@ -75,21 +73,24 @@ "view.gutter.lineNumbers")); gutterComponents.add(lineNumbersEnabled, cons); - minLineNumberDigits = new JTextField(String.valueOf( - getMinLineNumberDigits()),1); - minLineNumberDigits.setInputVerifier(new InputVerifier() { + InputVerifier integerInputVerifier = new InputVerifier() { @Override public boolean verify(JComponent input) { - String s = minLineNumberDigits.getText(); + if (! (input instanceof JTextField)) + return true; + JTextField tf = (JTextField) input; int i; try { - i = Integer.valueOf(s).intValue(); + i = Integer.valueOf(tf.getText()).intValue(); } catch (Exception e) { return false; } return (i >= 0); } - }); + }; + minLineNumberDigits = new JTextField(String.valueOf( + getMinLineNumberDigits()),1); + minLineNumberDigits.setInputVerifier(integerInputVerifier); JPanel minLineNumberDigitsPanel = new JPanel(); minLineNumberDigitsPanel.add(new JLabel( jEdit.getProperty("options.gutter.minLineNumberDigits"))); @@ -115,6 +116,19 @@ } }); + /* Selection area background color */ + addComponent(jEdit.getProperty("options.gutter.selectionAreaBgColor"), + selectionAreaBgColor = new ColorWellButton( + jEdit.getColorProperty("view.gutter.selectionAreaBgColor")), + GridBagConstraints.VERTICAL); + + /* Selection area width */ + selectionAreaWidth = new JTextField(String.valueOf( + getSelectionAreaWidth()),DEFAULT_SELECTION_GUTTER_WIDTH); + selectionAreaWidth.setInputVerifier(integerInputVerifier); + addComponent(jEdit.getProperty("options.gutter.selectionAreaWidth"), + selectionAreaWidth); + /* Text font */ gutterFont = new FontSelector( jEdit.getFontProperty("view.gutter.font", @@ -285,6 +299,10 @@ gutterEnabled.isSelected()); jEdit.setBooleanProperty(SELECTION_AREA_ENABLED_PROPERTY, selectionAreaEnabled.isSelected()); + jEdit.setColorProperty(SELECTION_AREA_BGCOLOR_PROPERTY, + selectionAreaBgColor.getSelectedColor()); + jEdit.setIntegerProperty("view.gutter.selectionAreaWidth", + Integer.valueOf(selectionAreaWidth.getText())); } //}}} //{{{ setGutterComponentsEnabledState @@ -326,19 +344,39 @@ if (n < 0) n = 2; return n; - } + } //}}} //{{{ isSelectionAreaEnabled() method public static boolean isSelectionAreaEnabled() { return jEdit.getBooleanProperty(SELECTION_AREA_ENABLED_PROPERTY); - } + } //}}} + //{{{ getSelectionAreaBgColor() method + public static Color getSelectionAreaBackground() + { + return jEdit.getColorProperty(SELECTION_AREA_BGCOLOR_PROPERTY); + } //}}} + + //{{{ getSelectionAreaWidth() method + public static int getSelectionAreaWidth() + { + int n = jEdit.getIntegerProperty("view.gutter.selectionAreaWidth", + DEFAULT_SELECTION_GUTTER_WIDTH); + if (n < 0) + n = DEFAULT_SELECTION_GUTTER_WIDTH; + return n; + } //}}} + //{{{ Private members private static final String GUTTER_ENABLED_PROPERTY = "view.gutter.enabled"; private static final String SELECTION_AREA_ENABLED_PROPERTY = "view.gutter.selectionAreaEnabled"; + private static final String SELECTION_AREA_BGCOLOR_PROPERTY = + "view.gutter.selectionAreaBgColor"; + private static final int DEFAULT_SELECTION_GUTTER_WIDTH = 12; + private FontSelector gutterFont; private ColorWellButton gutterForeground; private ColorWellButton gutterBackground; @@ -360,5 +398,7 @@ private JPanel gutterComponents; private JTextField minLineNumberDigits; private JCheckBox selectionAreaEnabled; + private ColorWellButton selectionAreaBgColor; + private JTextField selectionAreaWidth; //}}} } Modified: jEdit/trunk/org/gjt/sp/jedit/textarea/Gutter.java =================================================================== --- jEdit/trunk/org/gjt/sp/jedit/textarea/Gutter.java 2009-08-08 06:15:47 UTC (rev 15879) +++ jEdit/trunk/org/gjt/sp/jedit/textarea/Gutter.java 2009-08-08 15:23:13 UTC (rev 15880) @@ -102,6 +102,7 @@ this.textArea = textArea; enabled = true; selectionAreaEnabled = true; + selectionAreaWidth = SELECTION_GUTTER_WIDTH; setAutoscrolls(true); setOpaque(true); @@ -139,8 +140,17 @@ // fill the background Rectangle clip = gfx.getClipBounds(); gfx.setColor(getBackground()); - gfx.fillRect(clip.x, clip.y, clip.width, clip.height); - + int bgColorWidth = isSelectionAreaEnabled() ? FOLD_MARKER_SIZE : + clip.width; + gfx.fillRect(clip.x, clip.y, bgColorWidth, clip.height); + if (isSelectionAreaEnabled()) + { + if (selectionAreaBgColor == null) + selectionAreaBgColor = getBackground(); + gfx.setColor(selectionAreaBgColor); + gfx.fillRect(clip.x + FOLD_MARKER_SIZE, clip.y, + clip.width - FOLD_MARKER_SIZE, clip.height); + } // if buffer is loading, don't paint anything if (textArea.getBuffer().isLoading()) return; @@ -294,8 +304,8 @@ { Insets insets = border.getBorderInsets(this); collapsedSize.width = FOLD_MARKER_SIZE + insets.right; - if (selectionAreaEnabled) - collapsedSize.width += SELECTION_GUTTER_WIDTH; + if (isSelectionAreaEnabled()) + collapsedSize.width += selectionAreaWidth; collapsedSize.height = gutterSize.height = insets.top + insets.bottom; lineNumberWidth = fm.charWidth('5') * getLineNumberDigitCount(); @@ -345,7 +355,7 @@ if (buffer != null) buffer.addBufferListener(bufferListener); updateLineNumberWidth(); - } + } //}}} //{{{ updateLineNumberWidth() method private void updateLineNumberWidth() @@ -388,6 +398,8 @@ } } //}}} + //{{{ Getters and setters + //{{{ setGutterEnabled() method /* Enables showing or hiding the gutter. */ public void setGutterEnabled(boolean enabled) @@ -396,21 +408,39 @@ revalidate(); } //}}} + //{{{ isSelectionAreaEnabled() method + public boolean isSelectionAreaEnabled() + { + return selectionAreaEnabled; + } //}}} + //{{{ setSelectionAreaEnabled() method - public void setSelectonAreaEnabled(boolean enabled) + public void setSelectionAreaEnabled(boolean enabled) { - if (selectionAreaEnabled == enabled) + if (isSelectionAreaEnabled() == enabled) return; selectionAreaEnabled = enabled; if (enabled) - collapsedSize.width += SELECTION_GUTTER_WIDTH; + collapsedSize.width += selectionAreaWidth; else - collapsedSize.width -= SELECTION_GUTTER_WIDTH; + collapsedSize.width -= selectionAreaWidth; revalidate(); } //}}} - - //{{{ Getters and setters + //{{{ setSelectionAreaBackground() method + public void setSelectionAreaBackground(Color bgColor) + { + selectionAreaBgColor = bgColor; + repaint(); + } //}}} + + //{{{ setSelectionAreaWidth() method + public void setSelectionAreaWidth(int width) + { + selectionAreaWidth = width; + revalidate(); + } //}}} + //{{{ getHighlightedForeground() method /** * Get the foreground color for highlighted line numbers @@ -647,6 +677,7 @@ private Color intervalHighlight; private Color currentLineHighlight; private Color foldColor; + private Color selectionAreaBgColor; private FontMetrics fm; @@ -667,6 +698,7 @@ private JEditBuffer buffer; private BufferListener bufferListener; private int minLineNumberDigits; + private int selectionAreaWidth; //}}} //{{{ paintLine() method This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |