support for idea-icons (using ideaIC-129.354/platform/icons/src from IntelliJ IDEA Community Edition 12.1.2);

--- a/Admin/components/components.sha1	Thu Jun 27 23:17:26 2013 +0200
+++ b/Admin/components/components.sha1	Fri Jun 28 14:05:12 2013 +0200
@@ -28,6 +28,7 @@
 8e1d36f5071e3def2cb281f7fefe9f52352cb88f  jedit_build-20120903.tar.gz
 8fa0c67f59beba369ab836562eed4e56382f672a  jedit_build-20121201.tar.gz
 06e9be2627ebb95c45a9bcfa025d2eeef086b408  jedit_build-20130104.tar.gz
+c85c0829b8170f25aa65ec6852f505ce2a50639b  jedit_build-20130628.tar.gz
 8122526f1fc362ddae1a328bdbc2152853186fee  jfreechart-1.0.14.tar.gz
 6c737137cc597fc920943783382e928ea79e3feb  kodkodi-1.2.16.tar.gz
 5f95c96bb99927f3a026050f85bd056f37a9189e  kodkodi-1.5.2.tar.gz

--- a/Admin/components/main	Thu Jun 27 23:17:26 2013 +0200
+++ b/Admin/components/main	Fri Jun 28 14:05:12 2013 +0200
@@ -4,7 +4,7 @@
 exec_process-1.0.3
 Haskabelle-2013
 jdk-7u21
-jedit_build-20130104
+jedit_build-20130628
 jfreechart-1.0.14
 kodkodi-1.5.2
 polyml-5.5.0-3

--- a/src/Tools/jEdit/lib/Tools/jedit	Thu Jun 27 23:17:26 2013 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Fri Jun 28 14:05:12 2013 +0200
@@ -211,6 +211,7 @@
   "$ISABELLE_JEDIT_BUILD_HOME/contrib/SideKick.jar"
   "$ISABELLE_JEDIT_BUILD_HOME/contrib/cobra.jar"
   "$ISABELLE_JEDIT_BUILD_HOME/contrib/js.jar"
+  "$ISABELLE_JEDIT_BUILD_HOME/contrib/idea-icons.jar"
 )
 
 declare -a JFREECHART_JARS=()

--- a/src/Tools/jEdit/src/rendering.scala	Thu Jun 27 23:17:26 2013 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Fri Jun 28 14:05:12 2013 +0200
@@ -42,9 +42,16 @@
 
   /* icons */
 
-  private def load_icon(name: String): Icon =
+  def load_icon(name: String): Icon =
   {
-    val icon = GUIUtilities.loadIcon(name)
+    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
   }