steve
/
factor
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Add support for icon attribute in jEdit plugin

cvs
Slava Pestov 2004-11-26 02:58:58 +00:00
parent beeada9220
commit cf2bfad780
2 changed files with 5 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
build.xml
View File

@ -36,6 +36,7 @@
<include name="*.xml"/> <include name="*.xml"/>
<include name="doc/**/*.html"/> <include name="doc/**/*.html"/>
<include name="doc/**/*.png"/> <include name="doc/**/*.png"/>
<include name="library/**/*.png"/>
<include name="doc/*.html"/> <include name="doc/*.html"/>
</fileset> </fileset>
</jar> </jar>

4
factor/jedit/ListenerAttributeSet.java
View File

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