import org.eclipse.jface.preference.IPersistentPreferenceStore;
import org.eclipse.jface.preference.IPreferenceStore;
import org.eclipse.jface.resource.FontDescriptor;
+import org.eclipse.jface.resource.FontRegistry;
import org.eclipse.jface.resource.JFaceResources;
import org.eclipse.jface.resource.LocalResourceManager;
+import org.eclipse.jface.util.IPropertyChangeListener;
+import org.eclipse.jface.util.PropertyChangeEvent;
import org.eclipse.jface.window.DefaultToolTip;
import org.eclipse.jface.window.ToolTip;
import org.eclipse.swt.SWT;
import org.eclipse.swt.events.VerifyListener;
import org.eclipse.swt.graphics.Color;
import org.eclipse.swt.graphics.Font;
+import org.eclipse.swt.graphics.FontData;
import org.eclipse.swt.graphics.GC;
import org.eclipse.swt.graphics.Point;
import org.eclipse.swt.graphics.RGB;
import org.eclipse.swt.widgets.Event;
import org.eclipse.swt.widgets.Listener;
import org.eclipse.swt.widgets.Sash;
+import org.eclipse.ui.PlatformUI;
import org.eclipse.ui.preferences.ScopedPreferenceStore;
import org.simantics.scl.runtime.tuple.Tuple2;
StyledText output;
Sash sash;
+ StyledText deco;
protected StyledText input;
int userInputHeight=0;
protected Color greenColor;
protected Color redColor;
- protected Font textFont;
+
+ FontRegistry fontRegistry;
+ FontDescriptor textFontDescriptor;
+ Font textFont;
ArrayList<String> commandHistory = new ArrayList<String>();
int commandHistoryPos = 0;
return true;
}
- private boolean hasOption(int mask) {
+ protected boolean hasOption(int mask) {
return (options & mask) != 0;
}
resourceManager = new LocalResourceManager(JFaceResources.getResources(), this);
greenColor = resourceManager.createColor(new RGB(0, 128, 0));
redColor = resourceManager.createColor(new RGB(172, 0, 0));
- textFont = resourceManager.createFont( FontDescriptor.createFrom("Courier New", 12, SWT.NONE) );
+
+ // Initialize current text font
+ fontRegistry = PlatformUI.getWorkbench().getThemeManager().getCurrentTheme().getFontRegistry();
+ fontRegistry.addListener(fontRegistryListener);
+ FontDescriptor font = FontDescriptor.createFrom( fontRegistry.getFontData("org.simantics.scl.consolefont") );
+ setTextFont(font);
setLayout(new FormLayout());
readPreferences();
addListener(SWT.Dispose, event -> {
+ if (fontRegistry != null)
+ fontRegistry.removeListener(fontRegistryListener);
try {
writePreferences();
} catch (IOException e) {
}
protected void createInputArea() {
- // "> " Decoration
- StyledText deco = new StyledText(this, SWT.MULTI | SWT.READ_ONLY);
+ deco = new StyledText(this, SWT.MULTI | SWT.READ_ONLY);
deco.setFont(textFont);
deco.setEnabled(false);
GC gc = new GC(deco);
private void asyncSetErrorAnnotations(final String forCommand, final ErrorAnnotation[] annotations) {
if(input.isDisposed())
return;
- input.getDisplay().asyncExec(new Runnable() {
- @Override
- public void run() {
- if(input.isDisposed())
- return;
- if(!input.getText().equals(forCommand))
- return;
- syncSetErrorAnnotations(forCommand, annotations);
- }
+ input.getDisplay().asyncExec(() -> {
+ if(input.isDisposed())
+ return;
+ if(!input.getText().equals(forCommand))
+ return;
+ syncSetErrorAnnotations(forCommand, annotations);
});
}
return output;
}
+ IPropertyChangeListener fontRegistryListener = new IPropertyChangeListener() {
+ @Override
+ public void propertyChange(PropertyChangeEvent event) {
+ setTextFont( FontDescriptor.createFrom((FontData[]) event.getNewValue()) );
+ }
+ };
+
+ private void setTextFont(FontDescriptor font) {
+ FontDescriptor oldFontDesc = textFontDescriptor;
+ textFont = resourceManager.createFont(font);
+ textFontDescriptor = font;
+ applyTextFont(textFont);
+
+ // Only destroy old font after the new font has been set!
+ if (oldFontDesc != null)
+ resourceManager.destroyFont(oldFontDesc);
+ }
+
+ private void applyTextFont(Font font) {
+ if (output != null)
+ output.setFont(font);
+ if (deco != null)
+ deco.setFont(font);
+ if (input != null) {
+ input.setFont(font);
+ adjustInputSize(input.getText());
+ }
+ }
+
}