# HG changeset patch
# User wenzelm
# Date 1396383901 -7200
# Node ID 1a9f569b5b7e16760fc419df8f17e7216be795c7
# Parent  a6f8c3566560fd9e8955c7240f4ac19cdc9e037d
some rephrasing to ensure that this becomes cheap "foreach" and not expensive "map" (cf. 0fc032898b05);

diff -r a6f8c3566560 -r 1a9f569b5b7e src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Tue Apr 01 20:22:25 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala	Tue Apr 01 22:25:01 2014 +0200
@@ -114,11 +114,11 @@
     var finished = 0
     var warned = 0
     var failed = 0
-    for {
-      command <- node.commands
-      states = state.command_states(version, command)
-      status = command_status(states.iterator.flatMap(st => st.status.iterator))
-    } {
+    for { command <- node.commands }
+    {
+      val states = state.command_states(version, command)
+      val status = command_status(states.iterator.flatMap(st => st.status.iterator))
+
       if (status.is_running) running += 1
       else if (status.is_finished) {
         val warning = states.exists(st => st.results.entries.exists(p => is_warning(p._2)))