--- a/src/Pure/PIDE/rendering.scala Sun Mar 05 22:38:19 2017 +0100
+++ b/src/Pure/PIDE/rendering.scala Mon Mar 06 11:38:06 2017 +0100
@@ -33,13 +33,23 @@
val antiquoted = Value("antiquoted")
val foreground = values -- background
- // underline
+ // message underline
val writeln = Value("writeln")
val information = Value("information")
val warning = Value("warning")
val legacy = Value("legacy")
val error = Value("error")
- val underline = values -- background -- foreground
+ val message_underline = values -- background -- foreground
+
+ // message background
+
+ val writeln_message = Value("writeln_message")
+ val information_message = Value("information_message")
+ val tracing_message = Value("tracing_message")
+ val warning_message = Value("warning_message")
+ val legacy_message = Value("legacy_message")
+ val error_message = Value("error_message")
+ val message_background = values -- background -- foreground -- message_underline
}
@@ -76,6 +86,14 @@
legacy_pri -> Color.legacy,
error_pri -> Color.error)
+ val message_background_color = Map(
+ writeln_pri -> Color.writeln_message,
+ information_pri -> Color.information_message,
+ tracing_pri -> Color.tracing_message,
+ warning_pri -> Color.warning_message,
+ legacy_pri -> Color.legacy_message,
+ error_pri -> Color.error_message)
+
/* markup elements */
--- a/src/Tools/jEdit/src/jedit_rendering.scala Sun Mar 05 22:38:19 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Mon Mar 06 11:38:06 2017 +0100
@@ -180,9 +180,7 @@
val tooltip_color = color("tooltip_color")
val warning_color = color("warning_color")
val error_color = color("error_color")
- val writeln_message_color = color("writeln_message_color")
val information_message_color = color("information_message_color")
- val tracing_message_color = color("tracing_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")
@@ -480,15 +478,7 @@
/* message output */
- private lazy val message_colors = Map(
- Rendering.writeln_pri -> writeln_message_color,
- Rendering.information_pri -> information_message_color,
- Rendering.tracing_pri -> tracing_message_color,
- Rendering.warning_pri -> warning_message_color,
- Rendering.legacy_pri -> legacy_message_color,
- Rendering.error_pri -> error_message_color)
-
- def line_background(range: Text.Range): Option[(Color, Boolean)] =
+ def line_background(range: Text.Range): Option[(Rendering.Color.Value, Boolean)] =
{
val results =
snapshot.cumulate[Int](range, 0, JEdit_Rendering.line_background_elements, _ =>
@@ -497,7 +487,7 @@
})
val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
- message_colors.get(pri).map(message_color =>
+ Rendering.message_background_color.get(pri).map(message_color =>
{
val is_separator =
snapshot.cumulate[Boolean](range, false, JEdit_Rendering.separator_elements, _ =>
--- a/src/Tools/jEdit/src/rich_text_area.scala Sun Mar 05 22:38:19 2017 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala Mon Mar 06 11:38:06 2017 +0100
@@ -300,9 +300,9 @@
val line_range = Text.Range(start(i), end(i) min buffer.getLength)
// line background color
- for { (color, separator) <- rendering.line_background(line_range) }
+ for { (c, separator) <- rendering.line_background(line_range) }
{
- gfx.setColor(color)
+ gfx.setColor(rendering.color(c))
val sep = if (separator) 2 min (line_height / 2) else 0
gfx.fillRect(0, y + i * line_height, text_area.getWidth, line_height - sep)
}