# HG changeset patch
# User wenzelm
# Date 1392913308 -3600
# Node ID 7aea773c55745c8a5efb93ccb9d3be738aa98ddc
# Parent  ce575c2212fca29392abd028305f9dfe3c012953
tuned;

diff -r ce575c2212fc -r 7aea773c5574 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Thu Feb 20 16:56:51 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Thu Feb 20 17:21:48 2014 +0100
@@ -240,10 +240,10 @@
           range, (Protocol.Status.init, 0), overview_elements, _ =>
           {
             case ((status, pri), Text.Info(_, elem)) =>
-              if (elem.name == Markup.WARNING || elem.name == Markup.ERROR)
+              if (Protocol.command_status_markup(elem.name))
+                Some((Protocol.command_status(status, elem.markup), pri))
+              else
                 Some((status, pri max Rendering.message_pri(elem.name)))
-              else
-                Some((Protocol.command_status(status, elem.markup), pri))
           })
       if (results.isEmpty) None
       else {
@@ -345,17 +345,16 @@
   def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
     snapshot.select_markup(range, active_elements, command_state =>
       {
-        case Text.Info(info_range, elem @ Protocol.Dialog(_, serial, _))
-        if !command_state.results.defined(serial) =>
-          Some(Text.Info(snapshot.convert(info_range), elem))
-
         case Text.Info(info_range, elem) =>
-          if (elem.name == Markup.BROWSER ||
-              elem.name == Markup.GRAPHVIEW ||
-              elem.name == Markup.SENDBACK ||
-              elem.name == Markup.SIMP_TRACE)
-            Some(Text.Info(snapshot.convert(info_range), elem))
-          else None
+          if (elem.name == Markup.DIALOG) {
+            elem match {
+              case Protocol.Dialog(_, serial, _)
+              if !command_state.results.defined(serial) =>
+                Some(Text.Info(snapshot.convert(info_range), elem))
+              case _ => None
+            }
+          }
+          else Some(Text.Info(snapshot.convert(info_range), elem))
       }) match { case Text.Info(_, info) :: _ => Some(info) case _ => None }
 
 
@@ -556,21 +555,18 @@
       snapshot.cumulate_markup[Int](range, 0, line_background_elements, _ =>
         {
           case (pri, Text.Info(_, elem)) =>
-            val name = elem.name
-            if (name == Markup.INFORMATION)
+            if (elem.name == Markup.INFORMATION)
               Some(pri max Rendering.information_pri)
-            else if (name == Markup.WRITELN_MESSAGE || name == Markup.TRACING_MESSAGE ||
-                elem.name == Markup.WARNING_MESSAGE || name == Markup.ERROR_MESSAGE)
-              Some(pri max Rendering.message_pri(name))
-            else None
+            else
+              Some(pri max Rendering.message_pri(elem.name))
         })
     val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
 
-    val is_separator = pri > 0 &&
+    val is_separator =
+      pri > 0 &&
       snapshot.cumulate_markup[Boolean](range, false, Set(Markup.SEPARATOR), _ =>
         {
-          case (_, Text.Info(_, elem)) =>
-            if (elem.name == Markup.SEPARATOR) Some(true) else None
+          case _ => Some(true)
         }).exists(_.info)
 
     message_colors.get(pri).map((_, is_separator))
@@ -626,19 +622,11 @@
 
 
   def background2(range: Text.Range): List[Text.Info[Color]] =
-    snapshot.select_markup(range, Set(Markup.TOKEN_RANGE), _ =>
-      {
-        case Text.Info(_, elem) =>
-          if (elem.name == Markup.TOKEN_RANGE) Some(light_color) else None
-      })
+    snapshot.select_markup(range, Set(Markup.TOKEN_RANGE), _ => _ => Some(light_color))
 
 
   def bullet(range: Text.Range): List[Text.Info[Color]] =
-    snapshot.select_markup(range, Set(Markup.BULLET), _ =>
-      {
-        case Text.Info(_, elem) =>
-          if (elem.name == Markup.BULLET) Some(bullet_color) else None
-      })
+    snapshot.select_markup(range, Set(Markup.BULLET), _ => _ => Some(bullet_color))
 
 
   private val foreground_elements =