# HG changeset patch
# User wenzelm
# Date 1392982326 -3600
# Node ID ec4651c697e3f142d1b880e762129627ae4799df
# Parent  561754277494a923170a0c7aa7e41a076c66327c
tuned signature;

diff -r 561754277494 -r ec4651c697e3 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Fri Feb 21 12:07:38 2014 +0100
+++ b/src/Pure/PIDE/protocol.scala	Fri Feb 21 12:32:06 2014 +0100
@@ -63,10 +63,6 @@
     def is_failed: Boolean = failed
   }
 
-  val command_status_markup: Set[String] =
-    Set(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
-      Markup.FINISHED, Markup.FAILED)
-
   def command_status(status: Status, markup: Markup): Status =
     markup match {
       case Markup(Markup.ACCEPTED, _) => status.copy(accepted = true)
@@ -81,6 +77,13 @@
   def command_status(markups: List[Markup]): Status =
     (Status.init /: markups)(command_status(_, _))
 
+  val command_status_elements: Set[String] =
+    Set(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
+      Markup.FINISHED, Markup.FAILED)
+
+  val status_elements: Set[String] =
+    command_status_elements + Markup.WARNING + Markup.ERROR
+
 
   /* command timing */
 
@@ -162,12 +165,12 @@
 
   /* result messages */
 
-  private val clean = Set(Markup.REPORT, Markup.NO_REPORT)
+  private val clean_elements = Set(Markup.REPORT, Markup.NO_REPORT)
 
   def clean_message(body: XML.Body): XML.Body =
     body filter {
-      case XML.Wrapped_Elem(Markup(name, _), _, _) => !clean(name)
-      case XML.Elem(Markup(name, _), _) => !clean(name)
+      case XML.Wrapped_Elem(Markup(name, _), _, _) => !clean_elements(name)
+      case XML.Elem(Markup(name, _), _) => !clean_elements(name)
       case _ => true
     } map {
       case XML.Wrapped_Elem(markup, body, ts) => XML.Wrapped_Elem(markup, body, clean_message(ts))
@@ -272,7 +275,8 @@
 
   /* reported positions */
 
-  private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
+  private val position_elements =
+    Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
 
   def message_positions(
     command_id: Document_ID.Command,
@@ -294,9 +298,9 @@
     def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
       tree match {
         case XML.Wrapped_Elem(Markup(name, props), _, body) =>
-          body.foldLeft(if (include_pos(name)) elem_positions(props, set) else set)(positions)
+          body.foldLeft(if (position_elements(name)) elem_positions(props, set) else set)(positions)
         case XML.Elem(Markup(name, props), body) =>
-          body.foldLeft(if (include_pos(name)) elem_positions(props, set) else set)(positions)
+          body.foldLeft(if (position_elements(name)) elem_positions(props, set) else set)(positions)
         case XML.Text(_) => set
       }
 
diff -r 561754277494 -r ec4651c697e3 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Fri Feb 21 12:07:38 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Fri Feb 21 12:32:06 2014 +0100
@@ -231,19 +231,16 @@
 
   val overview_limit = options.int("jedit_text_overview_limit")
 
-  private val overview_elements =
-    Protocol.command_status_markup + Markup.WARNING + Markup.ERROR
-
   def overview_color(range: Text.Range): Option[Color] =
   {
     if (snapshot.is_outdated) None
     else {
       val results =
         snapshot.cumulate_markup[(Protocol.Status, Int)](
-          range, (Protocol.Status.init, 0), overview_elements, _ =>
+          range, (Protocol.Status.init, 0), Protocol.status_elements, _ =>
           {
             case ((status, pri), Text.Info(_, elem)) =>
-              if (Protocol.command_status_markup(elem.name))
+              if (Protocol.command_status_elements(elem.name))
                 Some((Protocol.command_status(status, elem.markup), pri))
               else
                 Some((status, pri max Rendering.message_pri(elem.name)))
@@ -534,7 +531,8 @@
     Rendering.warning_pri -> warning_color,
     Rendering.error_pri -> error_color)
 
-  private val squiggly_elements = Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
+  private val squiggly_elements =
+    Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
 
   def squiggly_underline(range: Text.Range): List[Text.Info[Color]] =
   {
@@ -597,7 +595,7 @@
   /* text background */
 
   private val background1_elements =
-    Protocol.command_status_markup + Markup.WRITELN_MESSAGE + Markup.TRACING_MESSAGE +
+    Protocol.command_status_elements + Markup.WRITELN_MESSAGE + Markup.TRACING_MESSAGE +
       Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
       active_elements
 
@@ -611,7 +609,7 @@
             range, (Some(Protocol.Status.init), None), background1_elements, command_state =>
             {
               case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
-              if (Protocol.command_status_markup(markup.name)) =>
+              if (Protocol.command_status_elements(markup.name)) =>
                 Some((Some(Protocol.command_status(status, markup)), color))
               case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
                 Some((None, Some(bad_color)))