# HG changeset patch
# User wenzelm
# Date 1330283114 -3600
# Node ID 134982ee4ecbdad210d29babccdfb77c7eb99aa3
# Parent  7e47ae85e161486949584513c4b99b0f92c74967
include warning messages in node status;

diff -r 7e47ae85e161 -r 134982ee4ecb src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Sun Feb 26 19:36:35 2012 +0100
+++ b/src/Pure/PIDE/protocol.scala	Sun Feb 26 20:05:14 2012 +0100
@@ -80,9 +80,10 @@
 
   /* node status */
 
-  sealed case class Node_Status(unprocessed: Int, running: Int, finished: Int, failed: Int)
+  sealed case class Node_Status(
+    unprocessed: Int, running: Int, finished: Int, warned: Int, failed: Int)
   {
-    def total: Int = unprocessed + running + finished + failed
+    def total: Int = unprocessed + running + finished + warned + failed
   }
 
   def node_status(
@@ -91,16 +92,21 @@
     var unprocessed = 0
     var running = 0
     var finished = 0
+    var warned = 0
     var failed = 0
     node.commands.foreach(command =>
       {
-        val status = command_status(state.command_state(version, command).status)
+        val st = state.command_state(version, command)
+        val status = command_status(st.status)
         if (status.is_running) running += 1
-        else if (status.is_finished) finished += 1
+        else if (status.is_finished) {
+          if (st.results.exists(p => is_warning(p._2))) warned += 1
+          else finished += 1
+        }
         else if (status.is_failed) failed += 1
         else unprocessed += 1
       })
-    Node_Status(unprocessed, running, finished, failed)
+    Node_Status(unprocessed, running, finished, warned, failed)
   }
 
 
diff -r 7e47ae85e161 -r 134982ee4ecb src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Sun Feb 26 19:36:35 2012 +0100
+++ b/src/Tools/jEdit/src/session_dockable.scala	Sun Feb 26 20:05:14 2012 +0100
@@ -116,6 +116,7 @@
             (n, color) <- List(
               (st.unprocessed, Isabelle_Rendering.unprocessed1_color),
               (st.running, Isabelle_Rendering.running_color),
+              (st.warned, Isabelle_Rendering.warning_color),
               (st.failed, Isabelle_Rendering.error_color)) }
           {
             gfx.setColor(color)