# HG changeset patch
# User wenzelm
# Date 1372423879 -7200
# Node ID 3a43a8b1ecb0212f80af1c479b880d34b89b09d4
# Parent  ff0e0bb8159755f6735557d9cfe6301ef0c34eb5
load icons via options -- prefer IntelliJ IDEA for now;

diff -r ff0e0bb81597 -r 3a43a8b1ecb0 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Fri Jun 28 14:05:12 2013 +0200
+++ b/src/Tools/jEdit/etc/options	Fri Jun 28 14:51:19 2013 +0200
@@ -72,3 +72,22 @@
 option inner_comment_color : string = "8B0000FF"
 option dynamic_color : string = "7BA428FF"
 
+
+section "Icons"
+
+(* jEdit/Tango *)
+(*
+option tooltip_close_icon : string = "16x16/actions/document-close.png"
+option tooltip_detach_icon : string = "16x16/actions/window-new.png"
+option gutter_warning_icon : string = "16x16/status/dialog-information.png"
+option gutter_legacy_icon : string = "16x16/status/dialog-warning.png"
+option gutter_error_icon : string = "16x16/status/dialog-error.png"
+*)
+
+(* IntelliJ IDEA *)
+option tooltip_close_icon : string = "idea-icons/actions/closeHovered.png"
+option tooltip_detach_icon : string = "idea-icons/actions/nextfile.png"
+option gutter_warning_icon : string = "idea-icons/runConfigurations/testFailed.png"
+option gutter_legacy_icon : string = "idea-icons/general/balloonWarning.png"
+option gutter_error_icon : string = "idea-icons/runConfigurations/testError.png"
+
diff -r ff0e0bb81597 -r 3a43a8b1ecb0 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Jun 28 14:05:12 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Jun 28 14:51:19 2013 +0200
@@ -142,14 +142,14 @@
   /* controls */
 
   private val close = new Label {
-    icon = Rendering.tooltip_close_icon
+    icon = current_rendering.tooltip_close_icon
     tooltip = "Close tooltip window"
     listenTo(mouse.clicks)
     reactions += { case _: MouseClicked => window.dismiss }
   }
 
   private val detach = new Label {
-    icon = Rendering.tooltip_detach_icon
+    icon = current_rendering.tooltip_detach_icon
     tooltip = "Detach tooltip window"
     listenTo(mouse.clicks)
     reactions += {
diff -r ff0e0bb81597 -r 3a43a8b1ecb0 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Fri Jun 28 14:05:12 2013 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Fri Jun 28 14:51:19 2013 +0200
@@ -56,14 +56,6 @@
     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 */
 
@@ -386,6 +378,14 @@
   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] =
   {
@@ -402,7 +402,7 @@
             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)
   }