1.1 --- a/src/Tools/jEdit/etc/options	Fri Jun 28 14:05:12 2013 +0200
     1.2 +++ b/src/Tools/jEdit/etc/options	Fri Jun 28 14:51:19 2013 +0200
     1.3 @@ -72,3 +72,22 @@
     1.4  option inner_comment_color : string = "8B0000FF"
     1.5  option dynamic_color : string = "7BA428FF"
     1.6  
     1.7 +
     1.8 +section "Icons"
     1.9 +
    1.10 +(* jEdit/Tango *)
    1.11 +(*
    1.12 +option tooltip_close_icon : string = "16x16/actions/document-close.png"
    1.13 +option tooltip_detach_icon : string = "16x16/actions/window-new.png"
    1.14 +option gutter_warning_icon : string = "16x16/status/dialog-information.png"
    1.15 +option gutter_legacy_icon : string = "16x16/status/dialog-warning.png"
    1.16 +option gutter_error_icon : string = "16x16/status/dialog-error.png"
    1.17 +*)
    1.18 +
    1.19 +(* IntelliJ IDEA *)
    1.20 +option tooltip_close_icon : string = "idea-icons/actions/closeHovered.png"
    1.21 +option tooltip_detach_icon : string = "idea-icons/actions/nextfile.png"
    1.22 +option gutter_warning_icon : string = "idea-icons/runConfigurations/testFailed.png"
    1.23 +option gutter_legacy_icon : string = "idea-icons/general/balloonWarning.png"
    1.24 +option gutter_error_icon : string = "idea-icons/runConfigurations/testError.png"
    1.25 +

     2.1 --- a/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Jun 28 14:05:12 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Fri Jun 28 14:51:19 2013 +0200
     2.3 @@ -142,14 +142,14 @@
     2.4    /* controls */
     2.5  
     2.6    private val close = new Label {
     2.7 -    icon = Rendering.tooltip_close_icon
     2.8 +    icon = current_rendering.tooltip_close_icon
     2.9      tooltip = "Close tooltip window"
    2.10      listenTo(mouse.clicks)
    2.11      reactions += { case _: MouseClicked => window.dismiss }
    2.12    }
    2.13  
    2.14    private val detach = new Label {
    2.15 -    icon = Rendering.tooltip_detach_icon
    2.16 +    icon = current_rendering.tooltip_detach_icon
    2.17      tooltip = "Detach tooltip window"
    2.18      listenTo(mouse.clicks)
    2.19      reactions += {

     3.1 --- a/src/Tools/jEdit/src/rendering.scala	Fri Jun 28 14:05:12 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/rendering.scala	Fri Jun 28 14:51:19 2013 +0200
     3.3 @@ -56,14 +56,6 @@
     3.4      else icon
     3.5    }
     3.6  
     3.7 -  private val gutter_icons = Map(
     3.8 -    warning_pri -> load_icon("16x16/status/dialog-information.png"),
     3.9 -    legacy_pri -> load_icon("16x16/status/dialog-warning.png"),
    3.10 -    error_pri -> load_icon("16x16/status/dialog-error.png"))
    3.11 -
    3.12 -  val tooltip_close_icon = load_icon("16x16/actions/document-close.png")
    3.13 -  val tooltip_detach_icon = load_icon("16x16/actions/window-new.png")
    3.14 -
    3.15  
    3.16    /* jEdit font */
    3.17  
    3.18 @@ -386,6 +378,14 @@
    3.19    val tooltip_margin: Int = options.int("jedit_tooltip_margin")
    3.20    val tooltip_bounds: Double = (options.real("jedit_tooltip_bounds") max 0.2) min 0.8
    3.21  
    3.22 +  lazy val tooltip_close_icon = Rendering.load_icon(options.string("tooltip_close_icon"))
    3.23 +  lazy val tooltip_detach_icon = Rendering.load_icon(options.string("tooltip_detach_icon"))
    3.24 +
    3.25 +
    3.26 +  private lazy val gutter_icons = Map(
    3.27 +    Rendering.warning_pri -> Rendering.load_icon(options.string("gutter_warning_icon")),
    3.28 +    Rendering.legacy_pri -> Rendering.load_icon(options.string("gutter_legacy_icon")),
    3.29 +    Rendering.error_pri -> Rendering.load_icon(options.string("gutter_error_icon")))
    3.30  
    3.31    def gutter_message(range: Text.Range): Option[Icon] =
    3.32    {
    3.33 @@ -402,7 +402,7 @@
    3.34              pri max Rendering.error_pri
    3.35          })
    3.36      val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
    3.37 -    Rendering.gutter_icons.get(pri)
    3.38 +    gutter_icons.get(pri)
    3.39    }
    3.40  
    3.41