# HG changeset patch
# User wenzelm
# Date 1418241087 -3600
# Node ID 6959ceb53ac855b87d2231291761feee95c5e11c
# Parent  7b1931111e375c28bcfe4be01a88c438d4ad48bb
more informative gutter content: fall-back on background color, e.g. when line numbers are enabled;
non-transparent information_message_color like other message colors;
removed unused error1_color;

diff -r 7b1931111e37 -r 6959ceb53ac8 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Wed Dec 10 19:26:01 2014 +0100
+++ b/src/Tools/jEdit/etc/options	Wed Dec 10 20:51:27 2014 +0100
@@ -89,9 +89,8 @@
 option information_color : string = "C1DFEEFF"
 option warning_color : string = "FF8C00FF"
 option error_color : string = "B22222FF"
-option error1_color : string = "B2222232"
 option writeln_message_color : string = "F0F0F0FF"
-option information_message_color : string = "C1DFEE32"
+option information_message_color : string = "DCEAF3FF"
 option tracing_message_color : string = "F0F8FFFF"
 option warning_message_color : string = "EEE8AAFF"
 option error_message_color : string = "FFC1C1FF"
diff -r 7b1931111e37 -r 6959ceb53ac8 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Wed Dec 10 19:26:01 2014 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Wed Dec 10 20:51:27 2014 +0100
@@ -128,27 +128,37 @@
         GUI_Thread.assert {}
 
         val gutter = text_area.getGutter
-        val width = GutterOptionPane.getSelectionAreaWidth
+        val sel_width = GutterOptionPane.getSelectionAreaWidth
         val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
         val FOLD_MARKER_SIZE = 12
 
-        if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
-          val buffer = model.buffer
-          JEdit_Lib.buffer_lock(buffer) {
-            val rendering = get_rendering()
+        val buffer = model.buffer
+        JEdit_Lib.buffer_lock(buffer) {
+          val rendering = get_rendering()
 
-            for (i <- 0 until physical_lines.length) {
-              if (physical_lines(i) != -1) {
-                val line_range = Text.Range(start(i), end(i))
+          for (i <- 0 until physical_lines.length) {
+            if (physical_lines(i) != -1) {
+              val line_range = Text.Range(start(i), end(i))
 
-                // gutter icons
-                rendering.gutter_icon(line_range) match {
-                  case Some(icon) =>
-                    val x0 = (FOLD_MARKER_SIZE + width - border_width - icon.getIconWidth) max 10
-                    val y0 = y + i * line_height + (((line_height - icon.getIconHeight) / 2) max 0)
+              rendering.gutter_content(line_range) match {
+                case Some((icon, color)) =>
+                  // icons within selection area
+                  if (!gutter.isExpanded &&
+                      gutter.isSelectionAreaEnabled && sel_width >= 12 && line_height >= 12)
+                  {
+                    val x0 =
+                      (FOLD_MARKER_SIZE + sel_width - border_width - icon.getIconWidth) max 10
+                    val y0 =
+                      y + i * line_height + (((line_height - icon.getIconHeight) / 2) max 0)
                     icon.paintIcon(gutter, gfx, x0, y0)
-                  case None =>
-                }
+                  }
+                  // background
+                  else {
+                    val y0 = y + i * line_height
+                    gfx.setColor(color)
+                    gfx.fillRect(0, y0, gutter.getWidth, line_height)
+                  }
+                case None =>
               }
             }
           }
diff -r 7b1931111e37 -r 6959ceb53ac8 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Wed Dec 10 19:26:01 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Wed Dec 10 20:51:27 2014 +0100
@@ -223,7 +223,6 @@
   val information_color = color_value("information_color")
   val warning_color = color_value("warning_color")
   val error_color = color_value("error_color")
-  val error1_color = color_value("error1_color")
   val writeln_message_color = color_value("writeln_message_color")
   val information_message_color = color_value("information_message_color")
   val tracing_message_color = color_value("tracing_message_color")
@@ -552,13 +551,17 @@
     else if (Protocol.is_information(msg)) Rendering.information_pri
     else 0
 
-  private lazy val gutter_icons = Map(
-    Rendering.information_pri -> JEdit_Lib.load_icon(options.string("gutter_information_icon")),
-    Rendering.warning_pri -> JEdit_Lib.load_icon(options.string("gutter_warning_icon")),
-    Rendering.legacy_pri -> JEdit_Lib.load_icon(options.string("gutter_legacy_icon")),
-    Rendering.error_pri -> JEdit_Lib.load_icon(options.string("gutter_error_icon")))
+  private lazy val gutter_message_content = Map(
+    Rendering.information_pri ->
+      (JEdit_Lib.load_icon(options.string("gutter_information_icon")), information_message_color),
+    Rendering.warning_pri ->
+      (JEdit_Lib.load_icon(options.string("gutter_warning_icon")), warning_message_color),
+    Rendering.legacy_pri ->
+      (JEdit_Lib.load_icon(options.string("gutter_legacy_icon")), warning_message_color),
+    Rendering.error_pri ->
+      (JEdit_Lib.load_icon(options.string("gutter_error_icon")), error_message_color))
 
-  def gutter_icon(range: Text.Range): Option[Icon] =
+  def gutter_content(range: Text.Range): Option[(Icon, Color)] =
   {
     val pris =
       snapshot.cumulate[Int](range, 0, Rendering.gutter_elements, _ =>
@@ -568,7 +571,7 @@
           case _ => None
         }).map(_.info)
 
-    gutter_icons.get((0 /: pris)(_ max _))
+    gutter_message_content.get((0 /: pris)(_ max _))
   }