src/Tools/jEdit/src/rendering.scala

--- a/src/Tools/jEdit/src/rendering.scala	Mon Aug 05 21:23:06 2013 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Mon Aug 05 22:54:50 2013 +0200
@@ -14,7 +14,7 @@
 import javax.swing.Icon
 
 import org.gjt.sp.jedit.syntax.{Token => JEditToken}
-import org.gjt.sp.jedit.{jEdit, GUIUtilities}
+import org.gjt.sp.jedit.jEdit
 
 import scala.collection.immutable.SortedMap
 
@@ -41,23 +41,6 @@
     Markup.ERROR -> error_pri, Markup.ERROR_MESSAGE -> error_pri)
 
 
-  /* 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
-  }
-
-
   /* jEdit font */
 
   def font_family(): String = jEdit.getProperty("view.font")
@@ -381,15 +364,15 @@
   val tooltip_margin: Int = options.int("jedit_tooltip_margin")
   val tooltip_bounds: Double = (options.real("jedit_tooltip_bounds") max 0.2) min 0.8
 
-  lazy val tooltip_close_icon = Rendering.load_icon(options.string("tooltip_close_icon"))
-  lazy val tooltip_detach_icon = Rendering.load_icon(options.string("tooltip_detach_icon"))
+  lazy val tooltip_close_icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon"))
+  lazy val tooltip_detach_icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))
 
 
   private lazy val gutter_icons = Map(
-    Rendering.information_pri -> Rendering.load_icon(options.string("gutter_information_icon")),
-    Rendering.warning_pri -> Rendering.load_icon(options.string("gutter_warning_icon")),
-    Rendering.legacy_pri -> Rendering.load_icon(options.string("gutter_legacy_icon")),
-    Rendering.error_pri -> Rendering.load_icon(options.string("gutter_error_icon")))
+    Rendering.information_pri -> JEdit_Lib.load_icon(options.string("gutter_information_icon")),
+    Rendering.warning_pri -> JEdit_Lib.load_icon(options.string("gutter_warning_icon")),
+    Rendering.legacy_pri -> JEdit_Lib.load_icon(options.string("gutter_legacy_icon")),
+    Rendering.error_pri -> JEdit_Lib.load_icon(options.string("gutter_error_icon")))
 
   private val gutter_elements = Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)