From cf2bfad780834ff3803c68b6f54f52c77670f294 Mon Sep 17 00:00:00 2001
From: Slava Pestov <slava@factorcode.org>
Date: Fri, 26 Nov 2004 02:58:58 +0000
Subject: [PATCH] Add support for icon attribute in jEdit plugin

---
 build.xml                              | 1 +
 factor/jedit/ListenerAttributeSet.java | 4 ++++
 2 files changed, 5 insertions(+)

diff --git a/build.xml b/build.xml
index 36d8a3874a..4fa7b9e1ca 100644
--- 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 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