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;
--- 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"
--- 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 =>
}
}
}
--- 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 _))
}