include warning messages in node status;
authorwenzelm
Sun Feb 26 20:05:14 2012 +0100 (2012-02-26 ago)
changeset 46688134982ee4ecb
parent 46687 7e47ae85e161
child 46690 07f9732804ad
include warning messages in node status;
src/Pure/PIDE/protocol.scala
src/Tools/jEdit/src/session_dockable.scala
     1.1 --- a/src/Pure/PIDE/protocol.scala	Sun Feb 26 19:36:35 2012 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Sun Feb 26 20:05:14 2012 +0100
     1.3 @@ -80,9 +80,10 @@
     1.4  
     1.5    /* node status */
     1.6  
     1.7 -  sealed case class Node_Status(unprocessed: Int, running: Int, finished: Int, failed: Int)
     1.8 +  sealed case class Node_Status(
     1.9 +    unprocessed: Int, running: Int, finished: Int, warned: Int, failed: Int)
    1.10    {
    1.11 -    def total: Int = unprocessed + running + finished + failed
    1.12 +    def total: Int = unprocessed + running + finished + warned + failed
    1.13    }
    1.14  
    1.15    def node_status(
    1.16 @@ -91,16 +92,21 @@
    1.17      var unprocessed = 0
    1.18      var running = 0
    1.19      var finished = 0
    1.20 +    var warned = 0
    1.21      var failed = 0
    1.22      node.commands.foreach(command =>
    1.23        {
    1.24 -        val status = command_status(state.command_state(version, command).status)
    1.25 +        val st = state.command_state(version, command)
    1.26 +        val status = command_status(st.status)
    1.27          if (status.is_running) running += 1
    1.28 -        else if (status.is_finished) finished += 1
    1.29 +        else if (status.is_finished) {
    1.30 +          if (st.results.exists(p => is_warning(p._2))) warned += 1
    1.31 +          else finished += 1
    1.32 +        }
    1.33          else if (status.is_failed) failed += 1
    1.34          else unprocessed += 1
    1.35        })
    1.36 -    Node_Status(unprocessed, running, finished, failed)
    1.37 +    Node_Status(unprocessed, running, finished, warned, failed)
    1.38    }
    1.39  
    1.40  
     2.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Sun Feb 26 19:36:35 2012 +0100
     2.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Sun Feb 26 20:05:14 2012 +0100
     2.3 @@ -116,6 +116,7 @@
     2.4              (n, color) <- List(
     2.5                (st.unprocessed, Isabelle_Rendering.unprocessed1_color),
     2.6                (st.running, Isabelle_Rendering.running_color),
     2.7 +              (st.warned, Isabelle_Rendering.warning_color),
     2.8                (st.failed, Isabelle_Rendering.error_color)) }
     2.9            {
    2.10              gfx.setColor(color)