some rephrasing to ensure that this becomes cheap "foreach" and not expensive "map" (cf. 0fc032898b05);
authorwenzelm
Tue Apr 01 22:25:01 2014 +0200 (2014-04-01)
changeset 563551a9f569b5b7e
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
     1.1 --- a/src/Pure/PIDE/protocol.scala	Tue Apr 01 20:22:25 2014 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Apr 01 22:25:01 2014 +0200
     1.3 @@ -114,11 +114,11 @@
     1.4      var finished = 0
     1.5      var warned = 0
     1.6      var failed = 0
     1.7 -    for {
     1.8 -      command <- node.commands
     1.9 -      states = state.command_states(version, command)
    1.10 -      status = command_status(states.iterator.flatMap(st => st.status.iterator))
    1.11 -    } {
    1.12 +    for { command <- node.commands }
    1.13 +    {
    1.14 +      val states = state.command_states(version, command)
    1.15 +      val status = command_status(states.iterator.flatMap(st => st.status.iterator))
    1.16 +
    1.17        if (status.is_running) running += 1
    1.18        else if (status.is_finished) {
    1.19          val warning = states.exists(st => st.results.entries.exists(p => is_warning(p._2)))