src/Tools/jEdit/src/rendering.scala

       else name
     val icon = GUIUtilities.loadIcon(name1)
     if (icon.getIconWidth < 0 || icon.getIconHeight < 0) error("Bad icon: " + name)
     else icon
   }
-
-  private val gutter_icons = Map(
-    warning_pri -> load_icon("16x16/status/dialog-information.png"),
-    legacy_pri -> load_icon("16x16/status/dialog-warning.png"),
-    error_pri -> load_icon("16x16/status/dialog-error.png"))
-
-  val tooltip_close_icon = load_icon("16x16/actions/document-close.png")
-  val tooltip_detach_icon = load_icon("16x16/actions/window-new.png")
 
 
   /* jEdit font */
 
   def font_family(): String = jEdit.getProperty("view.font")

   }
 
   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"))
+
+
+  private lazy val gutter_icons = Map(
+    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")))
 
   def gutter_message(range: Text.Range): Option[Icon] =
   {
     val results =
       snapshot.cumulate_markup[Int](range, 0, Some(Set(Markup.WARNING, Markup.ERROR)), _ =>

             }
           case (pri, Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _))) =>
             pri max Rendering.error_pri
         })
     val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
-    Rendering.gutter_icons.get(pri)
+    gutter_icons.get(pri)
   }
 
 
   private val squiggly_colors = Map(
     Rendering.writeln_pri -> writeln_color,