src/Tools/jEdit/src/jedit_lib.scala
changeset 52873 9e934d4fff00
parent 52478 0a1db0d02628
child 52874 91032244e4ca
--- a/src/Tools/jEdit/src/jedit_lib.scala	Mon Aug 05 21:23:06 2013 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Aug 05 22:54:50 2013 +0200
@@ -10,10 +10,11 @@
 import isabelle._
 
 import java.awt.{Component, Container, Window, GraphicsEnvironment, Point, Rectangle}
+import javax.swing.Icon
 
 import scala.annotation.tailrec
 
-import org.gjt.sp.jedit.{jEdit, Buffer, View}
+import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities}
 import org.gjt.sp.jedit.buffer.JEditBuffer
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter}
 
@@ -222,5 +223,22 @@
       val average = string_width("mix") / (3 * unit)
       def apply(s: String): Double = if (s == "\n") 1.0 else string_width(s) / unit
     }
+
+
+  /* icons */
+
+  def load_icon(name: String): Icon =
+  {
+    val name1 =
+      if (name.startsWith("idea-icons/")) {
+        val file =
+          Isabelle_System.platform_file_url(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar"))
+        "jar:" + file + "!/" + name
+      }
+      else name
+    val icon = GUIUtilities.loadIcon(name1)
+    if (icon.getIconWidth < 0 || icon.getIconHeight < 0) error("Bad icon: " + name)
+    else icon
+  }
 }