more direct warning within persistent Protocol.Status;
consider Markup.ERROR (e.g. from Output.error_message without exception) as failure;
tuned;

--- a/src/Pure/PIDE/command.scala	Thu Apr 03 21:08:00 2014 +0200
+++ b/src/Pure/PIDE/command.scala	Thu Apr 03 21:55:48 2014 +0200
@@ -109,7 +109,18 @@
     results: Results = Results.empty,
     markups: Markups = Markups.empty)
   {
-    lazy val protocol_status: Protocol.Status = Protocol.Status.make(status.iterator)
+    lazy val protocol_status: Protocol.Status =
+    {
+      val warnings =
+        if (results.iterator.exists(p => Protocol.is_warning(p._2)))
+          List(Markup(Markup.WARNING, Nil))
+        else Nil
+      val errors =
+        if (results.iterator.exists(p => Protocol.is_error(p._2)))
+          List(Markup(Markup.ERROR, Nil))
+        else Nil
+      Protocol.Status.make((warnings ::: errors ::: status).iterator)
+    }
 
     def markup(index: Markup_Index): Markup_Tree = markups(index)
 
@@ -126,7 +137,7 @@
     private def add_markup(status: Boolean, file_name: String, m: Text.Markup): State =
     {
       val markups1 =
-        if (status || Protocol.status_elements(m.info.name))
+        if (status || Protocol.liberal_status_elements(m.info.name))
           markups.add(Markup_Index(true, file_name), m)
         else markups
       copy(markups = markups1.add(Markup_Index(false, file_name), m))

--- a/src/Pure/PIDE/protocol.scala	Thu Apr 03 21:08:00 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala	Thu Apr 03 21:55:48 2014 +0200
@@ -47,6 +47,7 @@
     {
       var touched = false
       var accepted = false
+      var warned = false
       var failed = false
       var forks = 0
       var runs = 0
@@ -57,11 +58,12 @@
           case Markup.JOINED => forks -= 1
           case Markup.RUNNING => touched = true; runs += 1
           case Markup.FINISHED => runs -= 1
-          case Markup.FAILED => failed = true
+          case Markup.WARNING => warned = true
+          case Markup.FAILED | Markup.ERROR => failed = true
           case _ =>
         }
       }
-      Status(touched, accepted, failed, forks, runs)
+      Status(touched, accepted, warned, failed, forks, runs)
     }
 
     val empty = make(Iterator.empty)
@@ -77,26 +79,33 @@
   sealed case class Status(
     private val touched: Boolean,
     private val accepted: Boolean,
+    private val warned: Boolean,
     private val failed: Boolean,
     forks: Int,
     runs: Int)
   {
     def + (that: Status): Status =
-      Status(touched || that.touched, accepted || that.accepted, failed || that.failed,
-        forks + that.forks, runs + that.runs)
+      Status(
+        touched || that.touched,
+        accepted || that.accepted,
+        warned || that.warned,
+        failed || that.failed,
+        forks + that.forks,
+        runs + that.runs)
 
     def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0))
     def is_running: Boolean = runs != 0
     def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0
+    def is_warned: Boolean = is_finished && warned
     def is_failed: Boolean = failed
   }
 
-  val command_status_elements =
+  val proper_status_elements =
     Document.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
       Markup.FINISHED, Markup.FAILED)
 
-  val status_elements =
-    command_status_elements + Markup.WARNING + Markup.ERROR
+  val liberal_status_elements =
+    proper_status_elements + Markup.WARNING + Markup.ERROR
 
 
   /* command timing */
@@ -136,10 +145,8 @@
       val status = Status.merge(states.iterator.map(_.protocol_status))
 
       if (status.is_running) running += 1
-      else if (status.is_finished) {
-        val warning = states.exists(st => st.results.iterator.exists(p => is_warning(p._2)))
-        if (warning) warned += 1 else finished += 1
-      }
+      else if (status.is_warned) warned += 1
+      else if (status.is_finished) finished += 1
       else if (status.is_failed) failed += 1
       else unprocessed += 1
     }

--- a/src/Tools/jEdit/src/rendering.scala	Thu Apr 03 21:08:00 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Thu Apr 03 21:55:48 2014 +0200
@@ -182,7 +182,7 @@
     Document.Elements(Markup.SEPARATOR)
 
   private val background_elements =
-    Protocol.command_status_elements + Markup.WRITELN_MESSAGE +
+    Protocol.proper_status_elements + Markup.WRITELN_MESSAGE +
       Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
       Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
       active_elements
@@ -292,26 +292,18 @@
     if (snapshot.is_outdated) None
     else {
       val results =
-        snapshot.cumulate[(List[Markup], Int)](
-          range, (Nil, 0), Protocol.status_elements, _ =>
+        snapshot.cumulate[List[Markup]](range, Nil, Protocol.liberal_status_elements, _ =>
           {
-            case ((status, pri), Text.Info(_, elem)) =>
-              if (Protocol.command_status_elements(elem.name))
-                Some((elem.markup :: status), pri)
-              else
-                Some((status, pri max Rendering.message_pri(elem.name)))
+            case (status, Text.Info(_, elem)) => Some(elem.markup :: status)
           }, status = true)
       if (results.isEmpty) None
       else {
-        val status =
-          Protocol.Status.make(results.iterator.flatMap(info => info.info._1.iterator))
-        val pri = (0 /: results.iterator.map(info => info.info._2))(_ max _)
+        val status = Protocol.Status.make(results.iterator.flatMap(_.info))
 
         if (status.is_running) Some(running_color)
-        else if (pri == Rendering.warning_pri) Some(warning_color)
-        else if (pri == Rendering.error_pri) Some(error_color)
+        else if (status.is_warned) Some(warning_color)
+        else if (status.is_failed) Some(error_color)
         else if (status.is_unprocessed) Some(unprocessed_color)
-        else if (status.is_failed) Some(error_color)
         else None
       }
     }
@@ -606,7 +598,7 @@
             command_states =>
               {
                 case (((status, color), Text.Info(_, XML.Elem(markup, _))))
-                if !status.isEmpty && Protocol.command_status_elements(markup.name) =>
+                if !status.isEmpty && Protocol.proper_status_elements(markup.name) =>
                   Some((markup :: status, color))
                 case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
                   Some((Nil, Some(bad_color)))