Add support for icon attribute in jEdit plugin

diff --git a/build.xml b/build.xml
index 36d8a3874a9c0c7c084b4054cbe7c8ccec465a5a..4fa7b9e1caa4cb821ddbf33288da48a183916548 100644 (file)
--- a/build.xml
+++ b/build.xml
@@ -36,6 +36,7 @@
                                <include name="*.xml"/>
                                <include name="doc/**/*.html"/>
                                <include name="doc/**/*.png"/>
+                               <include name="library/**/*.png"/>
                                <include name="doc/*.html"/>
                        </fileset>
                </jar>

diff --git a/factor/jedit/ListenerAttributeSet.java b/factor/jedit/ListenerAttributeSet.java
index af595ae88e2f982cd830d06601338aa7a97a35ee..e003b4ec7e46c9d8d11c97e06554a01833afbe9c 100644 (file)
--- 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