tuned signature;

--- a/src/Tools/jEdit/src/jedit_lib.scala	Mon Aug 05 21:23:06 2013 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Aug 05 22:54:50 2013 +0200
@@ -10,10 +10,11 @@
 import isabelle._
 
 import java.awt.{Component, Container, Window, GraphicsEnvironment, Point, Rectangle}
+import javax.swing.Icon
 
 import scala.annotation.tailrec
 
-import org.gjt.sp.jedit.{jEdit, Buffer, View}
+import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities}
 import org.gjt.sp.jedit.buffer.JEditBuffer
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter}
 
@@ -222,5 +223,22 @@
       val average = string_width("mix") / (3 * unit)
       def apply(s: String): Double = if (s == "\n") 1.0 else string_width(s) / unit
     }
+
+
+  /* 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
+  }
 }
 

--- 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)