package net.sourceforge.phpdt.sql.editors; import org.eclipse.jface.preference.PreferenceConverter; import org.eclipse.jface.util.IPropertyChangeListener; import org.eclipse.jface.util.PropertyChangeEvent; import org.eclipse.swt.custom.StyledText; import org.eclipse.swt.graphics.Color; import org.eclipse.swt.graphics.Font; import org.eclipse.swt.graphics.FontData; import org.eclipse.swt.widgets.Composite; import org.eclipse.swt.widgets.Display; import org.eclipse.ui.editors.text.TextEditor; import net.sourceforge.phpdt.sql.PHPEclipseSQLPlugin; public class SQLEditor extends TextEditor { SQLConfiguration config; private ColorManager colorManager; /** * An editor capable of editing SQL scripts */ public SQLEditor() { super(); colorManager = new ColorManager(); config = new SQLConfiguration(colorManager); config.loadPrefs(); setPreferenceStore(PHPEclipseSQLPlugin.getDefault().getPreferenceStore()); IPropertyChangeListener preferenceListener = new IPropertyChangeListener() { public void propertyChange(PropertyChangeEvent event) { config.loadPrefs(); config.initializeColors(); getSourceViewer().invalidateTextPresentation(); StyledText widget = getSourceViewer().getTextWidget(); FontData font = PreferenceConverter.getFontData(getPreferenceStore(), "phpeclipse.sql.font"); //$NON-NLS-1$ widget.setFont(new Font(Display.getCurrent(), font)); Color background = colorManager.getColor(SQLColorConstants.BACKGROUND); widget.setBackground(background); } }; getPreferenceStore(). addPropertyChangeListener(preferenceListener); setSourceViewerConfiguration(config); setDocumentProvider(new SQLDocumentProvider()); } public void dispose() { colorManager.dispose(); super.dispose(); } public void createPartControl(Composite arg0) { super.createPartControl(arg0); StyledText widget = getSourceViewer().getTextWidget(); FontData font = PreferenceConverter.getFontData(getPreferenceStore(), "phpeclipse.sql.font"); //$NON-NLS-1$ widget.setFont(new Font(Display.getCurrent(), font)); Color background = colorManager.getColor(SQLColorConstants.BACKGROUND); widget.setBackground(background); } }