src/Tools/jEdit/src/jedit/plugin.scala
changeset 39241 e9a442606db3
parent 39167 803431dcc7fb
child 39515 57ceabb0bb8e
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Thu Sep 09 20:09:13 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Thu Sep 09 21:30:33 2010 +0200
@@ -15,12 +15,15 @@
 
 import scala.collection.mutable
 
-import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View}
+import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
+  Buffer, EditPane, ServiceManager, View}
 import org.gjt.sp.jedit.buffer.JEditBuffer
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
 import org.gjt.sp.jedit.msg.{BufferUpdate, EditPaneUpdate, PropertiesChanged}
 import org.gjt.sp.jedit.gui.DockableWindowManager
 
+import org.gjt.sp.util.Log
+
 
 object Isabelle
 {
@@ -106,6 +109,17 @@
   }
 
 
+  /* icons */
+
+  def load_icon(name: String): javax.swing.Icon =
+  {
+    val icon = GUIUtilities.loadIcon(name)
+    if (icon.getIconWidth < 0 || icon.getIconHeight < 0)
+      Log.log(Log.ERROR, icon, "Bad icon: " + name);
+    icon
+  }
+
+
   /* settings */
 
   def default_logic(): String =