src/Tools/jEdit/src/rendering.scala
changeset 52472 3a43a8b1ecb0
parent 52471 ff0e0bb81597
child 52530 99dd8b4ef3fe
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Fri Jun 28 14:05:12 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Fri Jun 28 14:51:19 2013 +0200
     1.3 @@ -56,14 +56,6 @@
     1.4      else icon
     1.5    }
     1.6  
     1.7 -  private val gutter_icons = Map(
     1.8 -    warning_pri -> load_icon("16x16/status/dialog-information.png"),
     1.9 -    legacy_pri -> load_icon("16x16/status/dialog-warning.png"),
    1.10 -    error_pri -> load_icon("16x16/status/dialog-error.png"))
    1.11 -
    1.12 -  val tooltip_close_icon = load_icon("16x16/actions/document-close.png")
    1.13 -  val tooltip_detach_icon = load_icon("16x16/actions/window-new.png")
    1.14 -
    1.15  
    1.16    /* jEdit font */
    1.17  
    1.18 @@ -386,6 +378,14 @@
    1.19    val tooltip_margin: Int = options.int("jedit_tooltip_margin")
    1.20    val tooltip_bounds: Double = (options.real("jedit_tooltip_bounds") max 0.2) min 0.8
    1.21  
    1.22 +  lazy val tooltip_close_icon = Rendering.load_icon(options.string("tooltip_close_icon"))
    1.23 +  lazy val tooltip_detach_icon = Rendering.load_icon(options.string("tooltip_detach_icon"))
    1.24 +
    1.25 +
    1.26 +  private lazy val gutter_icons = Map(
    1.27 +    Rendering.warning_pri -> Rendering.load_icon(options.string("gutter_warning_icon")),
    1.28 +    Rendering.legacy_pri -> Rendering.load_icon(options.string("gutter_legacy_icon")),
    1.29 +    Rendering.error_pri -> Rendering.load_icon(options.string("gutter_error_icon")))
    1.30  
    1.31    def gutter_message(range: Text.Range): Option[Icon] =
    1.32    {
    1.33 @@ -402,7 +402,7 @@
    1.34              pri max Rendering.error_pri
    1.35          })
    1.36      val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
    1.37 -    Rendering.gutter_icons.get(pri)
    1.38 +    gutter_icons.get(pri)
    1.39    }
    1.40  
    1.41