diff --git a/build.xml b/build.xml index 36d8a3874a..4fa7b9e1ca 100644 --- a/build.xml +++ b/build.xml @@ -36,6 +36,7 @@ + diff --git a/factor/jedit/ListenerAttributeSet.java b/factor/jedit/ListenerAttributeSet.java index af595ae88e..e003b4ec7e 100644 --- a/factor/jedit/ListenerAttributeSet.java +++ b/factor/jedit/ListenerAttributeSet.java @@ -34,6 +34,7 @@ import factor.Cons; import javax.swing.text.*; import javax.swing.Action; import java.awt.Color; +import org.gjt.sp.jedit.GUIUtilities; public class ListenerAttributeSet extends SimpleAttributeSet { @@ -67,6 +68,9 @@ public class ListenerAttributeSet extends SimpleAttributeSet addAttribute(StyleConstants.FontSize,value); else if("actions".equals(key)) addAttribute(ConsolePane.Actions,createActionsMenu((Cons)value)); + else if("icon".equals(key)) + addAttribute(StyleConstants.IconAttribute, + GUIUtilities.loadIcon((String)value)); } //}}} //{{{ toColor() method