--- 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
+ }
}