src/Tools/jEdit/src/rendering.scala
changeset 52471 ff0e0bb81597
parent 52102 59cc8881e911
child 52472 3a43a8b1ecb0
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Thu Jun 27 23:17:26 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Fri Jun 28 14:05:12 2013 +0200
     1.3 @@ -42,9 +42,16 @@
     1.4  
     1.5    /* icons */
     1.6  
     1.7 -  private def load_icon(name: String): Icon =
     1.8 +  def load_icon(name: String): Icon =
     1.9    {
    1.10 -    val icon = GUIUtilities.loadIcon(name)
    1.11 +    val name1 =
    1.12 +      if (name.startsWith("idea-icons/")) {
    1.13 +        val file =
    1.14 +          Isabelle_System.platform_file_url(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar"))
    1.15 +        "jar:" + file + "!/" + name
    1.16 +      }
    1.17 +      else name
    1.18 +    val icon = GUIUtilities.loadIcon(name1)
    1.19      if (icon.getIconWidth < 0 || icon.getIconHeight < 0) error("Bad icon: " + name)
    1.20      else icon
    1.21    }