equal
deleted
inserted
replaced
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) |