some rephrasing to ensure that this becomes cheap "foreach" and not expensive "map" (cf. 0fc032898b05);
authorwenzelm
Tue, 01 Apr 2014 22:25:01 +0200
changeset 56355 1a9f569b5b7e
parent 56354 a6f8c3566560
child 56356 c3dbaa155ece
some rephrasing to ensure that this becomes cheap "foreach" and not expensive "map" (cf. 0fc032898b05);
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)))