# HG changeset patch
# User wenzelm
# Date 1488797174 -3600
# Node ID ce8b8f979afd733cf744e57d08785d83b0e5472c
# Parent  45ccb8ee3d0833c927443991dbd84033c6e4a478
more generic colors;

diff -r 45ccb8ee3d08 -r ce8b8f979afd src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Mon Mar 06 11:45:46 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Mon Mar 06 11:46:14 2017 +0100
@@ -180,10 +180,6 @@
   val tooltip_color = color("tooltip_color")
   val warning_color = color("warning_color")
   val error_color = color("error_color")
-  val information_message_color = color("information_message_color")
-  val warning_message_color = color("warning_message_color")
-  val legacy_message_color = color("legacy_message_color")
-  val error_message_color = color("error_message_color")
   val spell_checker_color = color("spell_checker_color")
   val entity_ref_color = color("entity_ref_color")
   val breakpoint_disabled_color = color("breakpoint_disabled_color")
@@ -448,13 +444,17 @@
 
   private lazy val gutter_message_content = Map(
     Rendering.information_pri ->
-      (JEdit_Lib.load_icon(options.string("gutter_information_icon")), information_message_color),
+      (JEdit_Lib.load_icon(options.string("gutter_information_icon")),
+        color(Rendering.Color.information_message)),
     Rendering.warning_pri ->
-      (JEdit_Lib.load_icon(options.string("gutter_warning_icon")), warning_message_color),
+      (JEdit_Lib.load_icon(options.string("gutter_warning_icon")),
+        color(Rendering.Color.warning_message)),
     Rendering.legacy_pri ->
-      (JEdit_Lib.load_icon(options.string("gutter_legacy_icon")), legacy_message_color),
+      (JEdit_Lib.load_icon(options.string("gutter_legacy_icon")),
+        color(Rendering.Color.legacy_message)),
     Rendering.error_pri ->
-      (JEdit_Lib.load_icon(options.string("gutter_error_icon")), error_message_color))
+      (JEdit_Lib.load_icon(options.string("gutter_error_icon")),
+        color(Rendering.Color.error_message)))
 
   def gutter_content(range: Text.Range): Option[(Icon, Color)] =
   {