X-Git-Url: https://gerrit.simantics.org/r/gitweb?p=simantics%2Fplatform.git;a=blobdiff_plain;f=bundles%2Forg.simantics.scl.ui%2Fsrc%2Forg%2Fsimantics%2Fscl%2Fui%2Fconsole%2FAbstractCommandConsole.java;h=a293eaee1008c97ddda906211c2be6a240e0d130;hp=a98d65715c7fa89a652ac6a0293667027bfda51a;hb=68d3a3825550e81c7505b9548edd2db2aa7d841a;hpb=d1c23bec0b9900d92fc522429ef5476757a2af93

diff --git a/bundles/org.simantics.scl.ui/src/org/simantics/scl/ui/console/AbstractCommandConsole.java b/bundles/org.simantics.scl.ui/src/org/simantics/scl/ui/console/AbstractCommandConsole.java
index a98d65715..a293eaee1 100644
--- a/bundles/org.simantics.scl.ui/src/org/simantics/scl/ui/console/AbstractCommandConsole.java
+++ b/bundles/org.simantics.scl.ui/src/org/simantics/scl/ui/console/AbstractCommandConsole.java
@@ -12,8 +12,11 @@ import org.eclipse.core.runtime.preferences.InstanceScope;
 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;
@@ -23,6 +26,7 @@ import org.eclipse.swt.events.VerifyEvent;
 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;
@@ -36,6 +40,7 @@ import org.eclipse.swt.widgets.Display;
 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;
 
@@ -63,6 +68,7 @@ public abstract class AbstractCommandConsole extends Composite {
 
     StyledText output;
     Sash sash;
+    StyledText deco;
     protected StyledText input;
     
     int userInputHeight=0;
@@ -70,7 +76,10 @@ public abstract class AbstractCommandConsole extends Composite {
     
     protected Color greenColor;
     protected Color redColor;
-    protected Font textFont;
+
+    FontRegistry fontRegistry;
+    FontDescriptor textFontDescriptor;
+    Font textFont;
 
     ArrayList<String> commandHistory = new ArrayList<String>();
     int commandHistoryPos = 0;
@@ -97,7 +106,7 @@ public abstract class AbstractCommandConsole extends Composite {
         return true;
     }
 
-    private boolean hasOption(int mask) {
+    protected boolean hasOption(int mask) {
         return (options & mask) != 0;
     }
 
@@ -105,7 +114,12 @@ public abstract class AbstractCommandConsole extends Composite {
         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());
 
@@ -152,6 +166,8 @@ public abstract class AbstractCommandConsole extends Composite {
         readPreferences();
 
         addListener(SWT.Dispose, event -> {
+            if (fontRegistry != null)
+                fontRegistry.removeListener(fontRegistryListener);
             try {
                 writePreferences();
             } catch (IOException e) {
@@ -161,8 +177,7 @@ public abstract class AbstractCommandConsole extends Composite {
     }
 
     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);
@@ -513,15 +528,12 @@ public abstract class AbstractCommandConsole extends Composite {
     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);
         });
     }
     
@@ -562,4 +574,33 @@ public abstract class AbstractCommandConsole extends Composite {
         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());
+        }
+    }
+
 }