# HG changeset patch
# User wenzelm
# Date 1448117109 -3600
# Node ID 318f324d41f51c28fec0afca74e5260496470730
# Parent  309c20b21451f45c8f00daf4b4b7d2d870808d3f
less intrusive rendering, notably for State dockable;

diff -r 309c20b21451 -r 318f324d41f5 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Sat Nov 21 14:17:54 2015 +0100
+++ b/src/Tools/jEdit/etc/options	Sat Nov 21 15:45:09 2015 +0100
@@ -91,7 +91,6 @@
 option legacy_color : string = "FF8C00FF"
 option error_color : string = "B22222FF"
 option writeln_message_color : string = "F0F0F0FF"
-option state_message_color : string = "F0E4E4FF"
 option information_message_color : string = "DCEAF3FF"
 option tracing_message_color : string = "F0F8FFFF"
 option warning_message_color : string = "EEE8AAFF"
diff -r 309c20b21451 -r 318f324d41f5 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Sat Nov 21 14:17:54 2015 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Sat Nov 21 15:45:09 2015 +0100
@@ -243,7 +243,6 @@
   val legacy_color = color_value("legacy_color")
   val error_color = color_value("error_color")
   val writeln_message_color = color_value("writeln_message_color")
-  val state_message_color = color_value("state_message_color")
   val information_message_color = color_value("information_message_color")
   val tracing_message_color = color_value("tracing_message_color")
   val warning_message_color = color_value("warning_message_color")
@@ -656,7 +655,6 @@
 
   private lazy val message_colors = Map(
     Rendering.writeln_pri -> writeln_message_color,
-    Rendering.state_pri -> state_message_color,
     Rendering.information_pri -> information_message_color,
     Rendering.tracing_pri -> tracing_message_color,
     Rendering.warning_pri -> warning_message_color,
@@ -672,14 +670,15 @@
         })
     val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
 
-    val is_separator =
-      pri > 0 &&
-      snapshot.cumulate[Boolean](range, false, Rendering.separator_elements, _ =>
-        {
-          case _ => Some(true)
-        }).exists(_.info)
-
-    message_colors.get(pri).map((_, is_separator))
+    message_colors.get(pri).map(message_color =>
+      {
+        val is_separator =
+          snapshot.cumulate[Boolean](range, false, Rendering.separator_elements, _ =>
+            {
+              case _ => Some(true)
+            }).exists(_.info)
+        (message_color, is_separator)
+      })
   }
 
   def output_messages(results: Command.Results): List[XML.Tree] =