src/Tools/jEdit/src/jedit_lib.scala
changeset 64770 1ddc262514b8
parent 64730 76996d915894
child 64824 330ec9bc4b75
equal deleted inserted replaced
64769:6be5ec46688f 64770:1ddc262514b8
   318 
   318 
   319   def load_icon(name: String): Icon =
   319   def load_icon(name: String): Icon =
   320   {
   320   {
   321     val name1 =
   321     val name1 =
   322       if (name.startsWith("idea-icons/")) {
   322       if (name.startsWith("idea-icons/")) {
   323         val file = Url.platform_file(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar"))
   323         val file = Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar").file.toURI.toASCIIString
   324         "jar:" + file + "!/" + name
   324         "jar:" + file + "!/" + name
   325       }
   325       }
   326       else name
   326       else name
   327     val icon = GUIUtilities.loadIcon(name1)
   327     val icon = GUIUtilities.loadIcon(name1)
   328     if (icon.getIconWidth < 0 || icon.getIconHeight < 0) error("Bad icon: " + name)
   328     if (icon.getIconWidth < 0 || icon.getIconHeight < 0) error("Bad icon: " + name)